Overview and analysis of the SAT Challenge 2012 solver competition

被引：24

作者：

Balint, Adrian ^{[1
]}

Belov, Anton ^{[2
]}

Jarvisalo, Matti ^{[3
,4
]}

Sinz, Carsten ^{[5
]}

机构：

[1] Univ Ulm, Inst Theoret Comp Sci, D-89069 Ulm, Germany

[2] Univ Coll Dublin, Complex & Adapt Syst Lab, Dublin, Ireland

[3] Univ Helsinki, HITT, FIN-00014 Helsinki, Finland

[4] Univ Helsinki, Dept Comp Sci, FIN-00014 Helsinki, Finland

[5] Karlsruhe Inst Technol, Inst Theoret Informat, D-76021 Karlsruhe, Germany

来源：

ARTIFICIAL INTELLIGENCE | 2015年 / 223卷

基金：

芬兰科学院;

关键词：

Boolean satisfiability; SAT solvers; Competitions; Solver ranking; Empirical analysis; ALGORITHM; COMPLEXITY; SETS;

D O I：

10.1016/j.artint.2015.01.002

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Programs for the Boolean satisfiability problem (SAT), i.e., SAT solvers, are nowadays used as core decision procedures for a wide range of combinatorial problems. Advances in SAT solving during the last 10-15 years have been spurred by yearly solver competitions. In this article, we report on the main SAT solver competition held in 2012, SAT Challenge 2012. Besides providing an overview of how SAT Challenge 2012 was organized, we present an in-depth analysis of key aspects of the results obtained during the competition. (C) 2015 Elsevier B.V. All rights reserved.

引用

页码：120 / 155

页数：36

共 86 条

[1] BOINC: A system for public-resource computing and storage [J].

Anderson, DP .

FIFTH IEEE/ACM INTERNATIONAL WORKSHOP ON GRID COMPUTING, PROCEEDINGS, 2004, :4-10

[2]

[Anonymous], SAT COMPETITION 2011

[3]

[Anonymous], 2004, LECT NOTES COMPUT SC, DOI DOI 10.1007/11527695_

[4]

[Anonymous], GNOVELTY

[5]

[Anonymous], J AUTOM REASON

[6]

[Anonymous], P AAAI

[7]

[Anonymous], CoRR

[8]

[Anonymous], DEP COMPUTER SCI SER

[9]

[Anonymous], P 6 IJCAR ATP SYST C

[10]

[Anonymous], ARXIV12063111 CORR

← 1 2 3 4 5 6 7 8 9 →