Results

This page presents the results of the five tracks of the SAT Challenge 2012. In each track each solver had to tackle 600 SAT instances. Below, you can find the awarded solvers and the complete final rankings for each track.

Awarded Solvers

Main Track: Application SAT+UNSAT

  • Best Single-Engine Solver in the Application Track:
    glucose
    by Gilles Audemard and Laurent Simon
  • Best Interacting Multi-Engine Approach in the Application Track:
    Industrial Satisfiability Solver (ISS)
    by Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, and Meinolf Sellmann
  • Best Portfolio Approach in the Application Track:
    SATzilla 2012 APP
    by Lin Xu, Frank Hutter, Jonathan Shen, Holger H. Hoos, and Kevin Leyton-Brown

Main Track: Hard Combinatorial SAT+UNSAT

  • Best Single-Engine Solver in the Hard Combinatorial Track:
    clasp-crafted
    by Benjamin Kaufmann, Torsten Schaub, and Marius Schneider
  • Best Interacting Multi-Engine Approach in the Hard Combinatorial Track:
    interactSAT_c
    by Jingchao Chen
  • Best Portfolio Approach in the Hard Combinatorial Track:
    SATzilla 2012 COMB
    by Lin Xu, Frank Hutter, Jonathan Shen, Holger H. Hoos, and Kevin Leyton-Brown

Main Track: Random SAT

  • Best Solver in the Sequential Random SAT Track:
    CCASat
    by Shaowei Cai, Chuan Luo, and Kaile Su

Parallel Track: Application SAT+UNSAT

  • Best Solver in the Parallel Track:
    pfolioUZK
    by Andreas Wotzlaw, Alexander van der Grinten, Ewald Speckenmeyer, and Stefan Porschen

Sequential Portfolio Track

  • Best Solver in the Sequential Portfolio Track:
    SATzilla 2012 ALL
    by Lin Xu, Frank Hutter, Jonathan Shen, Holger H. Hoos, and Kevin Leyton-Brown

Complete Rankings

The color coding in the tables is as follows:

  • Green for Single-Engine Solvers
  • Blue for Interacting Multi-Engine Solvers
  • Orange for Parallel Solvers
  • Pink for Portfolio Solvers
  • Grey for the Virtual Best Solver (VBS)

The columns denote, from left to right, the rank in the track (Rank), the rank in the track with respect to the type of solver (RiG, Rank-in-Group), the solver name (Solver), the number of solved instances (#solved), the percentage of solved instances (%solved), the cumulative run-time on all solved instances (cum. run-time) and the median run-time (counting time-outs as 900 seconds).

The given run-times are in seconds and denote wall-clock time for the Parallel Track and CPU time for all other tracks.

Detailed results (runtimes for each solver on each instance, statistical evaluation) are available within the EDACC system.

Main Track: Application SAT+UNSAT

Rank RiG Solver #solved %solved cum. run-time median run-time
Virtual Best Solver (VBS)
56894.75652830.3
11
SATzilla2012 APP
53188.585194114.0
22
SATzilla2012 ALL
51585.886638122.2
31
Industrial SAT Solver
49983.293705160.2
lingeling (SAT Competition 2011 Bronze)
48881.384715135.3
42
interactSAT
48080.087676152.5
51
glucose
47579.271501114.4
62
SINN
47278.786302146.4
73
ZENN
46878.074019124.7
84
Lingeling
46777.891973185.5
95
linge_dyphase
45876.390192204.4
106
simpsat
45375.595737222.0
117
glue_dyphase
45275.367412126.4
glueminisat (SAT Competition 2011 Silver)
45275.368818145.7
123
CCCneq
45275.394956224.7
glucose (SAT Competition 2011 Gold)
45175.266076120.6
138
TENN
45175.282154173.1
144
CCCeq
44674.391896230.9
CryptoMiniSat (REFERENCE)
44273.795035240.6
153
ppfolio2012
42370.597819293.0
164
pfolioUZK
40467.398418348.6
minisat (REFERENCE)
39966.565633189.5
179
relback
39365.575842285.6
1810
Glucose++
38964.875377300.4
1911
satUZKs
38764.570910263.7
2012
caglue
38764.578154323.6
2113
contrasat12
38363.863645243.6
2214
satUZK
37963.268621282.3
2315
relback_m
35859.765364397.3
2416
riss
35158.567549434.3
255
Clingeling
27846.376576900.0
2617
Sat4j
24941.561334900.0
276
Flegel
23138.540190900.0
2818
march
376.29689900.0

Main Track: Hard Combinatorial SAT+UNSAT

Rank RiG Solver #solved %solved cum. run-time median run-time
Virtual Best Solver (VBS)
52988.2248481.3
11
SATzilla2012 COMB
47679.33810845.4
22
SATzilla2012 ALL
47378.84176545.2
33
ppfolio2012
42270.33578450.5
41
interactSAT_c
41769.54031356.6
54
pfolioUZK
40166.83418777.7
65
aspeed-crafted
37061.749239269.3
71
clasp-crafted
36761.249317277.0
MPhaseSAT (SAT Competititon 2011) (REFERENCE)
36160.235006172.6
86
claspfolio-crafted
35258.742522296.7
clasp (SAT Competition 2011 #1 Non-portfolio) (REFERENCE)
34757.841038322.2
92
Lingeling
33355.527313291.0
102
CCCneq
32954.836311454.6
113
CCCeq
32954.836943494.3
124
Flegel
32654.342999596.2
135
Clingeling
32654.347136599.8
glucose (SAT Competition 2011 #3 Non-portfolio) (REFERENCE)
32253.734546515.4
143
ZENN
31452.327878490.8
154
simpsat
31452.330999582.3
165
relback
31452.332182642.5
176
SINN
31352.233730647.6
187
caglue
31151.830109647.1
CryptoMiniSat (REFERENCE)
30751.232414682.9
198
satUZKs
30651.040401801.5
209
contrasat12
30651.040540778.0
2110
lingeling
30550.829095801.4
2211
relback_m
30450.736940806.0
minisat (REFERENCE)
30450.739055843.9
2312
satUZK
30050.035028869.6
2413
TENN
28747.826183900.0
2514
linge_dyphase
27946.529183900.0
2615
riss
27345.531599900.0
2716
Sat4j
27145.226382900.0
2817
sattime2012
24340.530541900.0
2918
sattime2011
23839.728198900.0
3019
gNovelty+PCL
23138.512791900.0
3120
Sparrow2011
21736.219972900.0
3221
march
21736.221817900.0
3322
BossLS
19031.715034900.0
3423
CCASat
18430.79052900.0
3524
sparrow2011-PCL
15025.015330900.0
EagleUP (SAT Competition 2011) (REFERENCE)
345.7997900.0

Main Track: Random SAT

Rank RiG Solver #solved %solved cum. run-time median run-time
Virtual Best Solver (VBS)
55893.07284139.2
11
CCASat
42370.576206218.8
21
SATzilla2012 RAND
32153.580796714.4
32
SATzilla2012 ALL
30651.083273845.6
Sparrow2011 (SAT Competition 2011 Gold) (REFERENCE)
30350.576396876.1
EagleUP (SAT Competition 2011 Bronze) (REFERENCE)
28347.283787900.0
42
sattime2012
26944.880345900.0
53
ppfolio2012
25342.270903900.0
sattime2011 (SAT Competition 2011 Silver) (REFERENCE)
23639.367237900.0
64
pfolioUZK
23038.355584900.0
73
ssa
15025.035316900.0
84
gNovelty+PCL
12320.540240900.0
95
BossLS
10317.218934900.0
106
sparrow2011-PCL
8113.522788900.0

Parallel Track: Application SAT+UNSAT

Rank Solver #solved %solved cum. run-time median run-time
Virtual Best Solver (VBS)
57696.03967019.6
1
pfolioUZK
53188.57239069.1
2
PeneLoPe
53088.36296754.4
3
ppfolio2012
52587.57883391.4
4
Cellulose
52186.85370542.0
5
ppfolio
50984.87540091.3
6
Sucrose
50383.87612080.7
7
ParaCIRMiniSAT
49682.76349786.7
8
clasp
49081.76242477.8
9
Glycogen
48981.57624197.1
10
ZENNfork
48580.87380889.1
11
CryptoMiniSat
48280.390543166.4
12
Plingeling
46777.887632169.2
13
CCCneq
46777.887970159.5
14
CCCeq
46677.792724167.1
15
SATX10
46477.373527124.3
16
Treengeling
45776.282929180.2
17
Minifork
42871.355864106.5
18
claspmt (REFERENCE)
36260.356435352.3
19
splitter
27345.535325900.0

Sequential Portfolio Track

Rank Solver #solved %solved cum. run-time median run-time
Virtual Best Solver (VBS)
48480.76480565.5
1
SATzilla2012 ALL
43372.268033139.9
2
ppfolio2012
37061.765598376.0
3
pfolioUZK
36260.369485391.6