clasp: A conflict-driven answer set solver

被引：157

作者：

Gebser, Martin ^{[1
]}

Kaufmann, Benjamin ^{[1
]}

Neumann, Andre ^{[1
]}

Schaub, Torsten ^{[1
]}

机构：

[1] Univ Potsdam, Inst Informat, August-Bebel-Str 89, D-14482 Potsdam, Germany

来源：

LOGIC PROGRAMMING AND NONMONOTONIC REASONING, PROCEEDINGS | 2007年 / 4483卷

关键词：

D O I：

10.1007/978-3-540-72200-7_23

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We describe the conflict-driven answer set solver clasp, which is based on concepts from constraint processing (CSP) and satisfiability checking (SAT). We detail its system architecture and major features, and provide a systematic empirical evaluation of its features.

引用

页码：260 / +

页数：2

共 18 条

[1]

Anger C., 2006, P INT WORKSH NONM RE, P58

[2]

Baral C., 2003, Knowledge Representation, Reasoning and Declarative Problem Solving

[3] An extensible SAT-solver [J].

Eén, N ;

Sörensson, N .

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 :502-518

[4]

Freeman J. W., 1995, Improvements to Propositional Satisfiability Search Algorithms

[5]

GEBSER M, CONFLICT DRIVEN ANSW

[6]

GEBSER M, CONFLICT DRIVEN ANSW, P386

[7] BerkMin: a fast and robust SAT-solver [J].

Goldberg, E ;

Novikov, Y .

DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, 2002 PROCEEDINGS, 2002, :142-149

[8]

HUANG J, EFFECT RESTARTS EFFI, P2318

[9] The DLV system for knowledge representation and reasoning [J].

Leone, Nicola ;

Pfeifer, Gerald ;

Faber, Wolfgang ;

Eiter, Thomas ;

Gottlob, Georg ;

Perri, Simona ;

Scarcello, Francesco .

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2006, 7 (03) :499-562

[10] OPTIMAL SPEEDUP OF LAS-VEGAS ALGORITHMS [J].

LUBY, M ;

SINCLAIR, A ;

ZUCKERMAN, D .

INFORMATION PROCESSING LETTERS, 1993, 47 (04) :173-180

← 1 2 →