SAT Race 2015

被引：26

作者：

Balyo, Tomas ^{[1
]}

Biere, Armin ^{[2
]}

Iser, Markus ^{[1
]}

Sinz, Carsten ^{[1
]}

机构：

[1] Karlsruhe Inst Technol, Dept Informat, Bldg 50-34,Fasanengarten 5, D-76131 Karlsruhe, Germany

[2] Johannes Kepler Univ Linz, Fac Engn & Nat Sci, Altenbergerstr 69, A-4040 Linz, Austria

来源：

ARTIFICIAL INTELLIGENCE | 2016年 / 241卷

关键词：

SAT; Competition; SAT-Race;

D O I：

10.1016/j.artint.2016.08.007

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Boolean satisfiability (SAT) solving is one of the most competitive research areas of theoretical computer science. The performance of state-of-the-art SAT solvers has been continuously improving in the last decades and has reached a level where SAT solvers can be employed to solve real world problems in fields such as hardware and software verification, automated planning and many others. One of the important driving forces of this progress are the yearly organized (since 2002) SAT competitions. In this paper we describe the 2015 SAT Race that featured the traditional sequential and parallel tracks (with 64 core computers) and introduced the Incremental Library Track, which is particularly interesting for developers of SAT based applications. We describe the 2015 SAT Race and provide a detailed analysis of its results. (C) 2016 Elsevier B.V. All rights reserved.

引用

页码：45 / 65

页数：21

共 38 条

[21] Recognition of Nested Gates in CNF Formulas [J].

Iser, Markus ;

Manthey, Norbert ;

Sinz, Carsten .

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015, 2015, 9340 :255-271

[22]

Jarvisalo Matti, 2012, Automated Reasoning. Proceedings 6th International Joint Conference, IJCAR 2012, P355, DOI 10.1007/978-3-642-31365-3_28

[23]

Jarvisalo M., 2011, SAT 2011 COMPETITION

[24]

Järvisalo M, 2012, AI MAG, V33, P89

[25]

Jarvisalo M, 2010, LECT NOTES COMPUT SC, V6015, P129, DOI 10.1007/978-3-642-12002-2_10

[26]

Katsirelos G., 2013, 27 AAAI C ART INT, V27, P481

[27]

KAUTZ H, 1992, ECAI 92 - 10TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE : PROCEEDINGS, P359

[28] Robust Boolean reasoning for equivalence checking and functional property verification [J].

Kuehlmann, A ;

Paruthi, V ;

Krohm, F ;

Ganai, MK .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2002, 21 (12) :1377-1394

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

LUBY, M ;

SINCLAIR, A ;

ZUCKERMAN, D .

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

[30]

Manthey N., 2014, P JOINT AUTOMATED RE, P26

← 1 2 3 4 →