SAT Competition 2017

Results

The slides used at the 2017 SAT Conference.

The Proceedings of the SAT Competition 2017: Solver and Benchmark Descriptions is now available.

Parallel Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT SolvedSolver NameNote
1229297.26237113124syrup24
1242909.39236127109cbpenelopehors concours*
1266163.50239110129plingeling
1290273.04231122109ccspenelopehors concours*
1334230.98227112115syrup48
1361020.21228127101scalope36hors concours*
1368420.42223114109painless
1474168.4621612591scalope48hors concours*
1562606.67208103105abcdsatdisqualified+
1564363.1120998111treengeling
1808778.801739776ddc-submit

Detailed results and benchmarks avaliable here.

* These solvers produced incorrect answers during the initial execution of the parallel track. The incorrect answers originated from a combination of writing non-unique files to the same network directory and solving benchmarks concurrently. After analyzing the results, the organizers fixed the solvers, all penelope hacks, by changing the code to store files locally. We label them "hors concours" due to requiring a fix by the organizers.

+ This solver produced incorrect answers.

Main Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT SolvedSolver Name
1610934.19936208102106Maple_LCM_Dist,default
1640696.51549206100106Maple_LCM,default
1654244.8346620496108MapleLRB_LCMoccRestart,default
1676517.6480019894104MapleLRB_LCM,default
1780711.473961889395MapleCOMSPS_LRB_VSIDS_2_drup,LRB_VSIDS_2_drup
1798300.375161888999COMiniSatPS_Pulsar_drup,drup
1805445.413971859689MapleCOMSPS_LRB_VSIDS_drup,LRB_VSIDS_drup
1825427.45627818583102cadical-sc17-proof,default
1866002.0463561799089MapleCOMSPS_CHB_VSIDS_drup,CHB_VSIDS_drup
1890486.9363841798099tch_glucose3,default
1893632.7003891808595glucose-4.1,default
1898402.2289971799782cadical-sc17-agile-proof,default
1909310.2727281768690GHackCOMSPS_drup,ghack_drup
1917700.0820771798297bs_glucose,default
1958463.8925021747797glu_vc,default
2051828.5105091618279tch_glucose2,default
2057715.1847481627290tch_glucose1,default
2059608.4479121607090glucose-3.0+width,default
2071505.7533711627290Riss7,BVE_DRAT
2124070.489601546688lingeling-bbe,default
2152106.9359351507575Riss7,noPP_DRAT
2176799.168991477374satUZK-seq,sge
2187064.4792171467373abcdsat_r17,default
2210323.173251447074satUZK-seq,ge
2370968.146641227250candy,rsilv
2379124.153181217249candy,rsili
2379582.073941257550satUZK-seq,sme
2384006.569471247351satUZK-seq,me
2414486.856001187048Candy,default

Detailed results and benchmarks avaliable here.

NoLimit Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT SolvedSolver Name
1758011.4630619187104COMiniSatPS_Pulsar_no_drup,11842,no_drup
1758801.497091919398MapleCOMSPS_LRB_VSIDS_2_no_drup,11844,LRB_VSIDS_2_no_drup
1789914.811431879196MapleCOMSPS_LRB_VSIDS_no_drup,11845,LRB_VSIDS_no_drup
1841142.36658418382101cadical-sc17-noproof,11736,default
1866617.38521818281101tch_glucose3,11501,default
1886016.050011788494MapleCOMSPS_CHB_VSIDS_no_drup,11843,CHB_VSIDS_no_drup
1896019.7487281828498bs_glucose,11498,default
1906346.2166211778592GHackCOMSPS_no_drup,11562,ghack_no_drup
1908135.6315331789583cadical-sc17-agile,11808,default
1937649.4194351777899glu_vc,11430,default
1953137.91877317272100abcdSAT_n17,11383,default
2018319.2053671637192Riss7,11379,default
2034518.521361677394lingeling-bbe,11703,default
2038502.1421271667393tch_glucose1,11499,default
2057599.7505071608278tch_glucose2,11500,default
2081416.4983271597188Riss7,11379,BVE
2110551.0143221556788abcdsat_r17,11464,default
2156688.1260751497475Riss7,11379,noPP

Detailed results and benchmarks avaliable here.

Random Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT SolvedSolver Name
1794277.029489441241240yalsat,12214,default
1894840.68412781131130tch_glucose3,11502,default
2075884.232601497970Score2SAT,11458,default

Detailed results and benchmarks avaliable here.

Agile Track

Full Ranking: (click on the table header to sort by another column)

ScoreTotal SolvedSAT SolvedUNSAT SolvedSolver Name
240983.1480253332879372350cadical-agile,12575,default
248613.0495320031297042425cadical-noproof,12576,default
257997.9300521331628252337glu_vc,11429,default
263772.2120812231007702330glucose-4.1,11823,default
265194.3828713330677352332bs_glucose,11488,default
267793.4365839230587202338tch_glucose1,11489,default
268285.4391992630577242333tch_glucose3,11491,default
276918.6771893529866652321abcdsat_a17,11401,default
278807.1986316629686552313abcdsat_r17,11463,default
283825.425995230417932248Candy,11816,default
285859.4303624028485672281Riss7,11381,noPP_DRAT
291201.3594595829986912307Riss7,11381,BVE_DRAT
297109.9336012528375652272tch_glucose2,11490,default
353870.8292409423951392256lingeling-bbe,12577,default
599642.3715939303yalsat-03s,12578,default

Detailed results and benchmarks avaliable here.

Incremental Track

Number of solved instances and rank per application:

Solver Name >abcdSATGlucoseRiss
Application vSolvedRankSolvedRankSolvedRank
Essential variables422.451.403.
Longest Simple Path951.822.03.
Partial MaxSAT571.562.553.
Pidgeon Hole Principle123.151.151.
Automated Planning631.22.03.
ijtihad - QBF Solver482.13.561.
cbmc - program verification603.612.631.
satpin - axiom pinpointing382.03.401.
Average Rank1.8752.02.0

Detailed results and benchmarks avaliable here.