\documentstyle[12pt,supertab]{article}
\begin{document}
\tablefirsthead{\hline\multicolumn{5}{|c|}{DIMACS SAT
BENCHMARKS}\\\hline File&Code&Variables&Clauses&Satisfiable?\\\hline}
\tablehead{\hline\multicolumn{5}{|c|}{DIMACS SAT
BENCHMARKS (cont.)}\\\hline File&Code&Variables&Clauses&Satisfiable?\\\hline}
\tabletail{\hline\multicolumn{5}{|r|}{\it Continued on next
page}\\\hline}
\tablelasttail{\hline}
\begin{supertabular}{|lc|rr|c|}
ii16a1.cnf&(Re)&1650 &19368 &Yes\\
ii16a2.cnf&(Re)&1602 &23281 &Yes\\
ii16b1.cnf&(Re)&1728 &24792 &Yes\\
ii16b2.cnf&(Re)&1076 &16121 &Yes\\
ii16c1.cnf&(Re)&1580 &16467 &Yes\\
ii16c2.cnf&(Re)&924 &13803 &Yes\\
ii16d1.cnf&(Re)&1230 &15901 &Yes\\
ii16d2.cnf&(Re)&836 &12461 &Yes\\
ii16e1.cnf&(Re)&1245 &14766 &Yes\\
ii16e2.cnf&(Re)&532 &7825 &Yes\\
ii32a1.cnf&(Re)&459 &9212 &Yes\\
ii32b1.cnf&(Re)&228 &1374 &Yes\\
ii32b2.cnf&(Re)&261 &2558 &Yes\\
ii32b3.cnf&(Re)&348 &5734 &Yes\\
ii32b4.cnf&(Re)&381 &9618 &Yes\\
ii32c1.cnf&(Re)&225 &1280 &Yes\\
ii32c2.cnf&(Re)&249 &2182 &Yes\\
ii32c3.cnf&(Re)&279 &3272 &Yes\\
ii32c4.cnf&(Re)&759 &20862 &Yes\\
ii32d1.cnf&(Re)&332 &2703 &Yes\\
ii32d2.cnf&(Re)&404 &5153 &Yes\\
ii32d3.cnf&(Re)&824 &19478 &Yes\\
ii32e1.cnf&(Re)&222 &1186 &Yes\\
ii32e2.cnf&(Re)&267 &2746 &Yes\\
ii32e3.cnf&(Re)&330 &5020 &Yes\\
ii32e4.cnf&(Re)&387 &7106 &Yes\\
ii32e5.cnf&(Re)&522 &11636 &Yes\\
ii8a1.cnf&(Re)&66 &186 &Yes\\
ii8a2.cnf&(Re)&180 &800 &Yes\\
ii8a3.cnf&(Re)&264 &1552 &Yes\\
ii8a4.cnf&(Re)&396 &2798 &Yes\\
ii8b1.cnf&(Re)&336 &2068 &Yes\\
ii8b2.cnf&(Re)&576 &4088 &Yes\\
ii8b3.cnf&(Re)&816 &6108 &Yes\\
ii8b4.cnf&(Re)&1068 &8214 &Yes\\
ii8c1.cnf&(Re)&510 &3065 &Yes\\
ii8c2.cnf&(Re)&950 &6689 &Yes\\
ii8d1.cnf&(Re)&530 &3207 &Yes\\
ii8d2.cnf&(Re)&930 &6547 &Yes\\
ii8e1.cnf&(Re)&520 &3136 &Yes\\
ii8e2.cnf&(Re)&870 &6121 &Yes\\
bf0432-007.cnf&(BF)&1040&3668&\\ 
bf1355-075.cnf&(BF)& 2180&6778&\\
bf1355-638.cnf&(BF)& 2177&4768&No\\
bf2670-001.cnf&(BF)& 1393&3434&\\
ssa0432-003.cnf&(SSA)&435&1027&No\\   
ssa2670-130.cnf&(SSA)&1359&3321&\\    
ssa2670-141.cnf&(SSA)&986&2315&No\\   
ssa6288-047.cnf&(SSA)&10410&34238&No\\
ssa7552-038.cnf&(SSA)&1501&3575&\\
ssa7552-158.cnf&(SSA)&1363&3034&Yes\\
ssa7552-159.cnf&(SSA)&1363&3032&Yes\\
ssa7552-160.cnf&(SSA)&1391&3126&Yes\\
dubois100.cnf&(Dub)&300&800&No\\
dubois20.cnf&(Dub)&60&160&No\\
dubois21.cnf&(Dub)&63&168&No\\
dubois22.cnf&(Dub)&66&176&No\\
dubois23.cnf&(Dub)&69&184&No\\
dubois24.cnf&(Dub)&72&192&No\\
dubois25.cnf&(Dub)&75&200&No\\
dubois26.cnf&(Dub)&78&208&No\\
dubois27.cnf&(Dub)&81&216&No\\
dubois28.cnf&(Dub)&84&224&No\\
dubois29.cnf&(Dub)&87&232&No\\
dubois30.cnf&(Dub)&90&240&No\\
dubois50.cnf&(Dub)&150&400&No\\
par16-1-c.cnf&(Par)&317 &1264 &Yes\\
par16-1.cnf&(Par)&1015 &3310 &Yes\\ 
par16-2-c.cnf&(Par)&349 &1392 &Yes\\
par16-2.cnf&(Par)&1015 &3374 &Yes\\ 
par16-3-c.cnf&(Par)&334 &1332 &Yes\\
par16-3.cnf&(Par)&1015 &3344 &Yes\\ 
par16-4-c.cnf&(Par)&324 &1292 &Yes\\
par16-4.cnf&(Par)&1015 &3324 &Yes\\ 
par16-5-c.cnf&(Par)&341 &1360 &Yes\\
par16-5.cnf&(Par)&1015 &3358 &Yes\\ 
par32-1-c.cnf&(Par)&1315 &5254 &Yes\\
par32-1.cnf&(Par)&3176 &10277 &Yes\\ 
par32-2-c.cnf&(Par)&1303 &5206 &Yes\\
par32-2.cnf&(Par)&3176 &10253 &Yes\\ 
par32-3-c.cnf&(Par)&1325 &5294 &Yes\\
par32-3.cnf&(Par)&3176 &10297 &Yes\\ 
par32-4-c.cnf&(Par)&1333 &5326 &Yes\\
par32-4.cnf&(Par)&3176 &10313 &Yes\\ 
par32-5-c.cnf&(Par)&1339 &5350 &Yes\\
par32-5.cnf&(Par)&3176 &10325 &Yes\\ 
par8-1-c.cnf&(Par)&64 &254 &Yes\\
par8-1.cnf&(Par)&350 &1149 &Yes\\  
par8-2-c.cnf&(Par)&68 &270 &Yes\\
par8-2.cnf&(Par)&350 &1157 &Yes\\  
par8-3-c.cnf&(Par)&75 &298 &Yes\\
par8-3.cnf&(Par)&350 &1171 &Yes\\  
par8-4-c.cnf&(Par)&67 &266 &Yes\\
par8-4.cnf&(Par)&350 &1155 &Yes\\  
par8-5-c.cnf&(Par)&75 &298 &Yes\\
par8-5.cnf&(Par)&350 &1171 &Yes\\
f600,cnf&(LRan)&600&2550&Yes\\
f1000.cnf&(LRan)&1000 &4250 &Yes\\
f2000.cnf&(LRan)&2000 &8500 &Yes\\
g125.17.cnf&(GC)&2125 &66272 & Yes\\
g125.18.cnf&(GC)&2250 &70163 & Yes\\
g250.15.cnf&(GC)&3750&233965&Yes\\
g250.29.cnf&(GC)&7250&454622&Yes\\
hanoi4.cnf&(Han)&718 &4934 &Yes\\
hanoi5.cnf&(Han)&1931 &14468 &Yes\\
pret150\_25.cnf&(Pret)&150&400 & No\\
pret150\_40.cnf&(Pret)&150&400 & No\\
pret150\_60.cnf&(Pret)&150&400 & No\\
pret150\_75.cnf&(Pret)&150&400 & No\\
pret60\_25.cnf&(Pret)&60&160 & No\\
pret60\_40.cnf&(Pret)&60&160 & No\\
pret60\_60.cnf&(Pret)&60&160 & No\\
pret60\_75.cnf&(Pret)&60&160 & No\\
hole10.cnf&(Hole)&110&561&No\\
hole6.cnf&(Hole)&42&133&No\\
hole7.cnf&(Hole)&56&204&No\\
hole8.cnf&(Hole)&72&297&No\\
hole9.cnf&(Hole)&90&415&No\\
jnh201.cnf&(JNH)&100&800&Yes\\
jnh202.cnf&(JNH)&100&800&No\\
jnh203.cnf&(JNH)&100&800&No\\
jnh204.cnf&(JNH)&100&800&Yes\\
jnh205.cnf&(JNH)&100&800&Yes\\
jnh206.cnf&(JNH)&100&800&No\\
jnh207.cnf&(JNH)&100&800&Yes\\
jnh208.cnf&(JNH)&100&800&No\\
jnh209.cnf&(JNH)&100&800&Yes\\
jnh210.cnf&(JNH)&100&800&Yes\\
jnh211.cnf&(JNH)&100&800&No\\
jnh212.cnf&(JNH)&100&800&Yes\\
jnh213.cnf&(JNH)&100&800&Yes\\
jnh214.cnf&(JNH)&100&800&No\\
jnh215.cnf&(JNH)&100&800&No\\
jnh216.cnf&(JNH)&100&800&No\\
jnh217.cnf&(JNH)&100&800&Yes\\
jnh218.cnf&(JNH)&100&800&Yes\\
jnh219.cnf&(JNH)&100&800&No\\
jnh220.cnf&(JNH)&100&800&Yes\\
jnh301.cnf&(JNH)&100&900&Yes\\
jnh302.cnf&(JNH)&100&900&No\\
jnh303.cnf&(JNH)&100&900&No\\
jnh304.cnf&(JNH)&100&900&No\\
jnh305.cnf&(JNH)&100&900&No\\
jnh306.cnf&(JNH)&100&900&No\\
jnh307.cnf&(JNH)&100&900&No\\
jnh308.cnf&(JNH)&100&900&No\\
jnh309.cnf&(JNH)&100&900&No\\
jnh310.cnf&(JNH)&100&900&No\\
jnh1.cnf&(JNH)&100&850&Yes\\
jnh2.cnf&(JNH)&100&850&No\\
jnh3.cnf&(JNH)&100&850&No\\
jnh4.cnf&(JNH)&100&850&No\\
jnh5.cnf&(JNH)&100&850&No\\
jnh6.cnf&(JNH)&100&850&No\\
jnh7.cnf&(JNH)&100&850&Yes\\
jnh8.cnf&(JNH)&100&850&No\\
jnh9.cnf&(JNH)&100&850&No\\
jnh10.cnf&(JNH)&100&850&No\\
jnh11.cnf&(JNH)&100&850&No\\
jnh12.cnf&(JNH)&100&850&Yes\\
jnh13.cnf&(JNH)&100&850&No\\
jnh14.cnf&(JNH)&100&850&No\\
jnh15.cnf&(JNH)&100&850&No\\
jnh16.cnf&(JNH)&100&850&No\\
jnh17.cnf&(JNH)&100&850&Yes\\
jnh18.cnf&(JNH)&100&850&No\\
jnh19.cnf&(JNH)&100&850&No\\
jnh20.cnf&(JNH)&100&850&No\\
aim-100-1\_6-no-1.cnf&(AIM)&100&160   &No\\ 
aim-100-1\_6-no-2.cnf&(AIM)&100&160 &No\\ 
aim-100-1\_6-no-3.cnf&(AIM)&100&160 &No\\ 
aim-100-1\_6-no-4.cnf&(AIM)&100&160&No\\ 
aim-100-1\_6-yes1-1.cnf&(AIM)&100&160&Yes\\
aim-100-1\_6-yes1-2.cnf&(AIM)&100&160&Yes\\
aim-100-1\_6-yes1-3.cnf&(AIM)&100&160&Yes\\
aim-100-1\_6-yes1-4.cnf&(AIM)&100&160&Yes\\
aim-100-2\_0-no-1.cnf&(AIM)&100&200&No\\ 
aim-100-2\_0-no-2.cnf&(AIM)&100&200 &No\\ 
aim-100-2\_0-no-3.cnf&(AIM)&100&200   &No\\ 
aim-100-2\_0-no-4.cnf&(AIM)&100&200   &No\\ 
aim-100-2\_0-yes1-1.cnf&(AIM)&100&200   &Yes\\
aim-100-2\_0-yes1-2.cnf&(AIM)&100&200   &Yes\\
aim-100-2\_0-yes1-3.cnf&(AIM)&100&200   &Yes\\
aim-100-2\_0-yes1-4.cnf&(AIM)&100&200   &Yes\\
aim-100-3\_4-yes1-1.cnf&(AIM)&100&340   &Yes\\
aim-100-3\_4-yes1-2.cnf&(AIM)&100&340   &Yes\\
aim-100-3\_4-yes1-3.cnf&(AIM)&100&340   &Yes\\
aim-100-3\_4-yes1-4.cnf&(AIM)&100&340   &Yes\\
aim-100-6\_0-yes1-1.cnf&(AIM)&100&600   &Yes\\
aim-100-6\_0-yes1-2.cnf&(AIM)&100&600   &Yes\\
aim-100-6\_0-yes1-3.cnf&(AIM)&100&600   &Yes\\
aim-100-6\_0-yes1-4.cnf&(AIM)&100&600   &Yes\\
aim-200-1\_6-no-1.cnf&(AIM)&200&320   &No\\ 
aim-200-1\_6-no-2.cnf&(AIM)&200&320   &No\\ 
aim-200-1\_6-no-3.cnf&(AIM)&200&320   &No\\ 
aim-200-1\_6-no-4.cnf&(AIM)&200&320   &No\\ 
aim-200-1\_6-yes1-1.cnf&(AIM)&200&320   &Yes\\
aim-200-1\_6-yes1-2.cnf&(AIM)&200&320   &Yes\\
aim-200-1\_6-yes1-3.cnf&(AIM)&200&320   &Yes\\
aim-200-1\_6-yes1-4.cnf&(AIM)&200&320   &Yes\\
aim-200-2\_0-no-1.cnf&(AIM)&200&400   &No\\ 
aim-200-2\_0-no-2.cnf&(AIM)&200&400   &No\\ 
aim-200-2\_0-no-3.cnf&(AIM)&200&400   &No\\ 
aim-200-2\_0-no-4.cnf&(AIM)&200&400   &No\\ 
aim-200-2\_0-yes1-1.cnf&(AIM)&200&400   &Yes\\
aim-200-2\_0-yes1-2.cnf&(AIM)&200&400   &Yes\\
aim-200-2\_0-yes1-3.cnf&(AIM)&200&400   &Yes\\
aim-200-2\_0-yes1-4.cnf&(AIM)&200&400   &Yes\\
aim-200-3\_4-yes1-1.cnf&(AIM)&200&680   &Yes\\
aim-200-3\_4-yes1-2.cnf&(AIM)&200&680   &Yes\\
aim-200-3\_4-yes1-3.cnf&(AIM)&200&680   &Yes\\
aim-200-3\_4-yes1-4.cnf&(AIM)&200&680   &Yes\\
aim-200-6\_0-yes1-1.cnf&(AIM)&200&1200   &Yes\\
aim-200-6\_0-yes1-2.cnf&(AIM)&200&1200   &Yes\\
aim-200-6\_0-yes1-3.cnf&(AIM)&200&1200   &Yes\\
aim-200-6\_0-yes1-4.cnf&(AIM)&200&1200   &Yes\\
aim-50-1\_6-no-1.cnf&(AIM)&50&80   &No\\  
aim-50-1\_6-no-2.cnf&(AIM)&50&80   &No\\  
aim-50-1\_6-no-3.cnf&(AIM)&50&80   &No\\  
aim-50-1\_6-no-4.cnf&(AIM)&50&80  &No\\  
aim-50-1\_6-yes1-1.cnf&(AIM)&50&80   &Yes\\
aim-50-1\_6-yes1-2.cnf&(AIM)&50&80   &Yes\\
aim-50-1\_6-yes1-3.cnf&(AIM)&50&80   &Yes\\
aim-50-1\_6-yes1-4.cnf&(AIM)&50&80   &Yes\\
aim-50-2\_0-no-1.cnf&(AIM)&50&100   &No\\  
aim-50-2\_0-no-2.cnf&(AIM)&50&100   &No\\  
aim-50-2\_0-no-3.cnf&(AIM)&50&100   &No\\  
aim-50-2\_0-no-4.cnf&(AIM)&50&100   &No\\  
aim-50-2\_0-yes1-1.cnf&(AIM)&50&100   &Yes\\
aim-50-2\_0-yes1-2.cnf&(AIM)&50&100   &Yes\\
aim-50-2\_0-yes1-3.cnf&(AIM)&50&100   &Yes\\
aim-50-2\_0-yes1-4.cnf&(AIM)&50&100   &Yes\\
aim-50-3\_4-yes1-1.cnf&(AIM)&50&170   &Yes\\
aim-50-3\_4-yes1-2.cnf&(AIM)&50&170   &Yes\\
aim-50-3\_4-yes1-3.cnf&(AIM)&50&170   &Yes\\
aim-50-3\_4-yes1-4.cnf&(AIM)&50&170   &Yes\\
aim-50-6\_0-yes1-1.cnf&(AIM)&50&300   &Yes\\
aim-50-6\_0-yes1-2.cnf&(AIM)&50&300   &Yes\\
aim-50-6\_0-yes1-3.cnf&(AIM)&50&300   &Yes\\
aim-50-6\_0-yes1-4.cnf&(AIM)&50&300   &Yes\\
\end{supertabular}

\bigskip
{\bf NOTES:}

(FAW) denotes problems that are part of the collection of problems
assembled by F.J. Radermacher and J. Mayer at the Forschungsinstitut
f\"ur anwndungsorientierte Wissensverarbeitung in Ulm Germany.
\begin{description}

\item[Re] From Mauricio Resende {\tt mgcr@research.att.com}. From ``A
continuous approach to inductive inference'', by Kamath, Karmarkar,
Ramakrishanan, and Resende (Mathematical Programming 57: 215--238
(1992)).

\item[SSA] (From Allen Van Gelder {\tt avg@cs.ucsd.edu} and Yumi Tsuji
  {\tt tsuji@cse.ucsc.edu}) Instances from circuit fault analysis:
checking for cicuit ``single--stuck--at'' fault.  For more instances,
see the sat/contributed/UCSC/instances directory.

\item[BF] (From Allen Van Gelder {\tt avg@cs.ucsd.edu} and Yumi Tsuji
  {\tt tsuji@cse.ucsc.edu}) Instances from circuit fault analysis:
  checking for cicuit ``bridge--fault''. For more
instances, see the sat/contributed/UCSC/instances directory.

\item[Dub] (From Olivier Dubois {\tt dubois@laforia.ibp.fr}  Instances
from the gensathard.c code.  For generator see the
sat/contributed/dubois directory.

\item[Par] (From James Crawford {\tt jc@research.att.com}) Instances
that arise from a problem in learning the parity function.  For more
details, see the README in the sat/contributed/crawford directory.

\item[LRan] (From Bart Selman {\tt selman@research.att.com}) Large
random satisfiable instances. See also the README.cnf in
sat/contributed/selman. 

\item[GC] (From Bart Selman {\tt selman@research.att.com}) The boolean
satisfiability form of a hard graph coloring problem.  See also the
README.cnf in sat/contributed/selman.

\item[Hanoi] (From Bart Selman {\tt selman@research.att.com}) An
encoding of the Towers of Hanoi problem.  Contact {\tt
kautz@research.att.com} for more information and similar instances.
See also the README.cnf file in sat/contributed/selman.

\item[Pret] (From Daniele Pretolani {\tt daniele@crt.umontreal.ca}) An
encoding of two--coloring a graph, along with a parity constraint to
force nonsatisfiablity.  Generator is in sat/contributed/pretolani.

\item[JNH] (From John Hooker {\tt jh38+@andrew.cmu.edu}) (FAW) A set of
random instances generated to be difficult by rejecting unit clauses
and setting the density to a hard value.

\item[Hole] (From John Hooker {\tt jh38+@andrew.cmu.edu}) (FAW)
Instance of the pigeon hole problem.  holen asks if it is possible to
place n+1 pigeons in n holes without two pigeons being in the same
hole.

\item[AIM] (From Eiji Miyano {\tt miyano@csce.kyushu-u.ac.jp})
Artificially generated 3--sat instances.  All the ``yes'' instances
have exactly one satisfying assignment.  For generators and further
information, see sat/contributed/iwama.


\end{description}

\end{document}