next up previous
Next: Random Up: First stage results Previous: Industrial

Handmade

Results of all solvers on all handmade benchmarks:

solver #series #benchs Remark
amvo 1 10  
berkmin561 16 65  
berkmin62 16 60 SAT2002 winner
bmsat 15 53 Hors concours
compsat 26 134 Incorrect
farseer 6 14  
forklift 17 63  
funex 15 53  
jerusat1a 20 82  
jerusat1b 22 81  
jerusat1c 19 63  
jquest2 16 57  
kcnfs 16 51  
limmat 14 52  
lsat 15 128  
marchsp 19 84  
marchtt 18 83  
marchxq 17 79 Incorrect
oepir 17 64  
opensat 8 25  
qingting 3 12  
satnik 20 88  
sato 15 52  
saturn 7 29  
satzilla2 21 90 Hors concours
satzilla 21 89  
satzoo0 18 82  
satzoo1 21 102  
siege 22 97 Hors concours
tts 10 68 Hors concours
unitwalk 5 20  
xqingting 10 38  
zchaff 17 67 SAT2002 winner

Figure 3: Number of instances solved vs. CPU time for complete solvers on all handmade benchmarks
\begin{figure}\centerline{\epsfig{figure=Complete-HandMade-color.eps,width=18cm}}\end{figure}

Figure 4: Number of instances solved vs. CPU time for all solvers on SAT handmade benchmarks
\begin{figure}\centerline{\epsfig{figure=Uncomplete-HandMade-color.eps,width=18cm}}\end{figure}

Detailled results on handmade SAT2002 challenging benchmarks (i.e. not solved during the first stage of the SAT2002 competition):

benchmark solved by
handmade/simon/sat02/ezfact256_1.cnf(1515)  
handmade/simon/sat02/ezfact64_10.cnf(1516)  
handmade/simon/sat02/ezfact64_1.cnf(1517) compsat(7) satzoo1(31)
handmade/simon/sat02/ezfact64_2.cnf(1518) compsat(7) oepir(12)
handmade/simon/sat02/ezfact64_3.cnf(1519) compsat(7)
handmade/simon/sat02/ezfact64_4.cnf(1520)  
handmade/simon/sat02/ezfact64_5.cnf(1521)  
handmade/simon/sat02/ezfact64_6.cnf(1522)  
handmade/simon/sat02/ezfact64_7.cnf(1523) compsat(7)
handmade/simon/sat02/ezfact64_8.cnf(1524) compsat(7)
handmade/simon/sat02/ezfact64_9.cnf(1525)  
handmade/simon/sat02/hanoi6.cnf(1526) forklift(3) siege(30)
handmade/simon/sat02/lisa21_99_a.cnf(1527) bmsat(19) compsat(7) jerusat1b(10) jerusat1c(11) lsat(23) marchsp(16) marchtt(17) marchxq(18) satnik(15) satzilla(29) satzilla2(32) siege(30)
handmade/simon/sat02/Mat26.cnf(1528) compsat(7)
handmade/simon/sat02/Mat317.cnf(1529)  
handmade/simon/sat02/Mat323.cnf(1530)  
handmade/simon/sat02/par32-1-c.cnf(1531) lsat(23)
handmade/simon/sat02/par32-1.cnf(1532) lsat(23)
handmade/simon/sat02/par32-2-c.cnf(1533) lsat(23)
handmade/simon/sat02/par32-2.cnf(1534) lsat(23)
handmade/simon/sat02/par32-3-c.cnf(1535)  
handmade/simon/sat02/par32-3.cnf(1536) lsat(23)
handmade/simon/sat02/par32-4-c.cnf(1537) lsat(23)
handmade/simon/sat02/par32-4.cnf(1538) lsat(23)
handmade/simon/sat02/par32-5-c.cnf(1539) lsat(23)
handmade/simon/sat02/par32-5.cnf(1540) lsat(23)
handmade/simon/sat02/pyhala-braun-sat-40-4-03.cnf(1541) compsat(7) satzilla(29) satzilla2(32) zchaff(4)
handmade/simon/sat02/pyhala-braun-sat-40-4-04.cnf(1542) satzoo1(31) siege(30)
handmade/simon/sat02/pyhala-braun-unsat-35-4-03.cnf(1543) compsat(7) kcnfs(25) satnik(15) satzilla(29)
handmade/simon/sat02/pyhala-braun-unsat-35-4-04.cnf(1544) compsat(7) kcnfs(25) satnik(15) satzilla(29)
handmade/simon/sat02/pyhala-braun-unsat-40-4-01.cnf(1545)  
handmade/simon/sat02/pyhala-braun-unsat-40-4-02.cnf(1546)  
handmade/simon/sat02/pyhala-braun-unsat-40-4-03.cnf(1547) compsat(7)
handmade/simon/sat02/pyhala-braun-unsat-40-4-04.cnf(1548)  
handmade/simon/sat02/rope_2500.cnf(1549) siege(30)
handmade/simon/sat02/rope_5000.cnf(1550)  
handmade/simon/sat02/rope_7500.cnf(1551)  
handmade/simon/sat02/urquhart3_25bis.cnf(1552) berkmin62(1) compsat(7) jerusat1a(9) jerusat1b(10) lsat(23) marchsp(16) marchtt(17) marchxq(18) satnik(15) satzilla(29) satzilla2(32) satzoo0(5) satzoo1(31) siege(30) tts(33)
handmade/simon/sat02/urquhart3_25.cnf(1553) compsat(7) lsat(23) marchsp(16) marchtt(17) marchxq(18) satzilla(29) satzilla2(32) tts(33)
handmade/simon/sat02/urquhart4_25bis.cnf(1554) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/urquhart4_25.cnf(1555) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/Urquhart-s3-b3.cnf(1556) compsat(7) jerusat1a(9) jerusat1b(10) jerusat1c(11) lsat(23) satnik(15) sato(28) satzilla(29) satzilla2(32) satzoo0(5) satzoo1(31) siege(30) tts(33) zchaff(4)
handmade/simon/sat02/Urquhart-s3-b4.cnf(1557) compsat(7) lsat(23) satzilla(29) satzilla2(32) satzoo1(31) siege(30) tts(33)
handmade/simon/sat02/Urquhart-s3-b6.cnf(1558) compsat(7) lsat(23) tts(33)
handmade/simon/sat02/Urquhart-s4-b1.cnf(1560) compsat(7) lsat(23) satzilla(29) satzilla2(32) tts(33)
handmade/simon/sat02/Urquhart-s4-b2.cnf(1561) compsat(7) lsat(23) tts(33)
handmade/simon/sat02/Urquhart-s4-b3.cnf(1562) compsat(7) lsat(23) tts(33)
handmade/simon/sat02/Urquhart-s5-b1.cnf(1570) lsat(23) tts(33)
handmade/simon/sat02/Urquhart-s5-b2.cnf(1571) lsat(23)
handmade/simon/sat02/Urquhart-s5-b3.cnf(1572) lsat(23)
handmade/simon/sat02/x1.1_128.cnf(1579) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1_128.cnf(1580) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1.1_40.cnf(1581) compsat(7) jerusat1a(9) lsat(23) marchsp(16) marchtt(17) marchxq(18) satnik(15) satzilla(29) satzilla2(32) satzoo1(31) siege(30) tts(33)
handmade/simon/sat02/x1.1_44.cnf(1582) compsat(7) lsat(23) marchsp(16) marchtt(17) marchxq(18) satzilla(29) satzilla2(32)
handmade/simon/sat02/x1.1_48.cnf(1583) compsat(7) lsat(23) marchsp(16) marchtt(17) marchxq(18) satzilla(29) satzilla2(32) satzoo1(31) siege(30) tts(33)
handmade/simon/sat02/x1.1_56.cnf(1584) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1.1_64.cnf(1585) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1.1_72.cnf(1586) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1.1_80.cnf(1587) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1.1_96.cnf(1588) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1_36.cnf(1589) compsat(7) jerusat1a(9) lsat(23) marchsp(16) marchtt(17) marchxq(18) satnik(15) satzilla(29) satzilla2(32) satzoo0(5) satzoo1(31) siege(30) tts(33)
handmade/simon/sat02/x1_40.cnf(1590) compsat(7) lsat(23) marchsp(16) marchtt(17) marchxq(18) satzilla(29) satzilla2(32) satzoo1(31) siege(30) tts(33)
handmade/simon/sat02/x1_44.cnf(1591) compsat(7) lsat(23) marchsp(16) marchtt(17) marchxq(18) satzilla(29) satzilla2(32) tts(33)
handmade/simon/sat02/x1_48.cnf(1592) compsat(7) jerusat1b(10) lsat(23) marchsp(16) marchtt(17) marchxq(18) satnik(15) satzilla(29) satzilla2(32) satzoo1(31) siege(30) tts(33)
handmade/simon/sat02/x1_56.cnf(1593) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1_64.cnf(1594) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1_72.cnf(1595) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1_80.cnf(1596) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x1_96.cnf(1597) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x2_128.cnf(1598) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x2_40.cnf(1599) compsat(7) lsat(23) marchsp(16) marchtt(17) marchxq(18) satzilla(29) satzilla2(32) satzoo1(31) siege(30) tts(33)
handmade/simon/sat02/x2_44.cnf(1600) compsat(7) lsat(23) marchsp(16) marchtt(17) marchxq(18) satzilla(29) satzilla2(32) siege(30)
handmade/simon/sat02/x2_48.cnf(1601) compsat(7) lsat(23) marchsp(16) marchtt(17) marchxq(18) satzilla(29) satzilla2(32) tts(33)
handmade/simon/sat02/x2_56.cnf(1602) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x2_64.cnf(1603) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x2_72.cnf(1604) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x2_80.cnf(1605) lsat(23) marchsp(16) marchtt(17) marchxq(18)
handmade/simon/sat02/x2_96.cnf(1606) lsat(23) marchsp(16) marchtt(17) marchxq(18)

next up previous
Next: Random Up: First stage results Previous: Industrial
LE BERRE Daniel 2003-05-02