next up previous
Next: Solvers ranking Up: First stage results Previous: Handmade

Random

Results of all solvers on all random benchmarks:

solver #series #benchs Remark
amvo 0 0  
berkmin561 10 54  
berkmin62 9 51  
bmsat 6 43 Hors concours
compsat 17 96 Incorrect
farseer 1 6  
forklift 11 53  
funex 5 37  
jerusat1a 6 46  
jerusat1b 7 43  
jerusat1c 6 40  
jquest2 4 23  
kcnfs 25 163  
limmat 5 24  
lsat 10 52  
marchsp 18 131  
marchtt 18 128  
marchxq 16 119 Incorrect
oepir 5 39  
oksolver 16 96 Hors concours, SAT2002 winner
opensat 3 13  
qingting 9 73  
satnik 13 64  
sato 9 54  
saturn 14 127  
satzilla2 22 172 Hors concours
satzilla 19 121  
satzoo0 10 49  
satzoo1 11 67  
siege 6 44 Hors concours
tts 0 0 Hors concours
unitwalk 15 139  
xqingting 4 27  
zchaff 10 53  

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

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

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

benchmark solved by
random/simon/sat02-random/glassybp-v399-s382874052.cnf(1677) kcnfs(25)
random/simon/sat02-random/glassybp-v399-s499089820.cnf(1678) kcnfs(25) marchsp(16) marchtt(17)
random/simon/sat02-random/glassyb-v399-s500582891.cnf(1679) kcnfs(25) satzilla(29) satzilla2(32)
random/simon/sat02-random/glassyb-v399-s732524269.cnf(1680) kcnfs(25) marchsp(16) marchtt(17) satzilla(29) satzilla2(32)
random/simon/sat02-random/hgen2-v400-s161064952.cnf(1681)  
random/simon/sat02-random/hgen2-v450-s41511877.cnf(1682)  
random/simon/sat02-random/hgen2-v500-s1216665065.cnf(1683)  
random/simon/sat02-random/hgen3-v300-s1766565160.cnf(1684) kcnfs(25)
random/simon/sat02-random/hgen3-v300-s1817652174.cnf(1685) kcnfs(25)
random/simon/sat02-random/hgen3-v300-s229883414.cnf(1686) kcnfs(25)
random/simon/sat02-random/hgen3-v350-s1711636364.cnf(1687)  
random/simon/sat02-random/hgen3-v350-s524562458.cnf(1688)  
random/simon/sat02-random/hgen3-v400-s344840348.cnf(1689)  
random/simon/sat02-random/hgen3-v400-s553296708.cnf(1690)  
random/simon/sat02-random/hgen3-v450-s432353833.cnf(1691)  
random/simon/sat02-random/hgen3-v500-s1349121860.cnf(1692)  
random/simon/sat02-random/hgen3-v500-s1803930514.cnf(1693)  
random/simon/sat02-random/hgen3-v500-s1920280160.cnf(1694) saturn(27) unitwalk(26)
random/simon/sat02-random/hgen3-v550-s1180212793.cnf(1695) unitwalk(26)
random/simon/sat02-random/hgen3-v550-s1969596846.cnf(1696)  
random/simon/sat02-random/hgen3-v550-s918732479.cnf(1697) saturn(27) unitwalk(26)
random/simon/sat02-random/okgen-c1700-v400-s2038016593-2038016593.cnf(1698) kcnfs(25) marchsp(16) marchtt(17)
random/simon/sat02-random/okgen-c1890-v450-s1673494695-1673494695.cnf(1699) kcnfs(25)
random/simon/sat02-random/okgen-c1912-v450-s1189481636-1189481636.cnf(1700) kcnfs(25) satzilla(29) satzilla2(32)
random/simon/sat02-random/okgen-c1912-v450-s243113776-243113776.cnf(1701) kcnfs(25) satzilla(29) satzilla2(32)
random/simon/sat02-random/okgen-c1935-v450-s1097304465-1097304465.cnf(1702) kcnfs(25)
random/simon/sat02-random/okgen-c1935-v450-s1697757218-1697757218.cnf(1703) kcnfs(25)
random/simon/sat02-random/okgen-c1935-v450-s569787048-569787048.cnf(1704) kcnfs(25)
random/simon/sat02-random/okgen-c2025-v450-s1380514806-1380514806.cnf(1705) compsat(7) kcnfs(25) marchsp(16) marchtt(17) satzilla(29) satzilla2(32)
random/simon/sat02-random/okgen-c2025-v450-s35766214-35766214.cnf(1706) kcnfs(25) marchsp(16) marchtt(17) satzilla(29) satzilla2(32)
random/simon/sat02-random/okgen-c2025-v450-s7443027-7443027.cnf(1707) kcnfs(25)
random/simon/sat02-random/unif-c1700-v400-s734590802.cnf(1708) kcnfs(25) marchsp(16) marchtt(17) satzilla(29) satzilla2(32)
random/simon/sat02-random/unif-c1890-v450-s1615727951.cnf(1709) kcnfs(25)
random/simon/sat02-random/unif-c1912-v450-s1305257180.cnf(1710) kcnfs(25) marchxq(18) qingting(20) saturn(27) satzilla(29) satzilla2(32) unitwalk(26)
random/simon/sat02-random/unif-c1912-v450-s669590537.cnf(1711) kcnfs(25) satzilla(29) satzilla2(32)
random/simon/sat02-random/unif-c1935-v450-s164592491.cnf(1712) kcnfs(25) marchtt(17) saturn(27) satzilla(29) satzilla2(32) unitwalk(26)
random/simon/sat02-random/unif-c1935-v450-s402823357.cnf(1713) kcnfs(25) marchsp(16) marchtt(17) saturn(27) satzilla(29) satzilla2(32) unitwalk(26)
random/simon/sat02-random/unif-c1935-v450-s529333649.cnf(1714) kcnfs(25)
random/simon/sat02-random/unif-c2025-v450-s1561158813.cnf(1715) kcnfs(25) marchsp(16) marchtt(17) satzilla(29) satzilla2(32)
random/simon/sat02-random/unif-c2025-v450-s2044100906.cnf(1716) compsat(7) kcnfs(25) marchsp(16) marchtt(17) satzilla(29) satzilla2(32)
random/simon/sat02-random/unif-c2025-v450-s605642359.cnf(1717) kcnfs(25) marchsp(16) marchtt(17) satzilla(29) satzilla2(32)

next up previous
Next: Solvers ranking Up: First stage results Previous: Handmade
LE BERRE Daniel 2003-05-02