ersatz-0.2: data/dimacs/bf/descr.html
<html><head><title>SATLIB - Benchmark Problems</title></head><body alink="#ff0000" bgcolor="white" link="#0000ff" text="black" vlink="#551a8b">
<br>
<h1>Instances from circuit fault analysis</h1>
<br>
The following description is based on the description given by <a href="http://www.cse.ucsc.edu/personnel/faculty/avg.html">Allen van
Gelder</a> and <a href="mailto:tsuji@cse.ucsc.edu">Yumi
Tsuji</a>. The original description can be found <a href="ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/contributed/UCSC/instances/cnf-ssa/README">here</a>.<br><br>
The instances given here are selected formulas from those generated by
Nemesis. Nemesis is a test-pattern generation program described in
[LF91,Lar92].<br><br>
These formulas are in CNF, and contain clauses of lengths 1-6.
Usually, more than half the clauses are Krom-clauses (2-clauses), so
the number of clauses is not as formidable as it first appears.<br><br>
The given instances include only a subset of the formulas generated by
Nemesis because there are a large number of them, which could cause
disk space problems. Also, the large majority are objectively very
easy, and would not provide significant tests of algorithms.<br><br>
Nemesis applys random (but repeatable) simulation process to the
circuits to identify some detectable faults, then
generates cnf formulas only for those that were not found to be
detectable by this simulation.<br><br>
Further deterministic polynomial time tests on the formulas generated
by Nemesis were done to eliminate those that can be easily processed.
This screening eliminates both satisfiable and unsatisfiable formulas.
For example, a formula that is unsatisfiable based on the Krom clauses
alone is screened out.<br><br>
Each selected formula is "squeezed" (Nemesis generates formula that
has many gaps in the variable id's; so we rename the variables to make
them consecutive without gaps while maintaining the relative order).
The program "cnfsqueeze" is available <a href="ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/contributed/UCSC/instances">here</a>.
<br><br>
Formulas are in DIMACS Challenge cnf format. A separate directory,
Cnfparse, has a parser and example programs using the parser.<br><br>
<h4>Benchmark instances</h4>
There are four benchmark instances which test for <i>bridge faults</i>
and eight instances which test for <i>single-at-stuck</i> faults. The
instances are of rather large size (most of them have more than 1000
variables). Yet, it should be noted that the instances contain unit
clauses and, hence, can still be simplified by unit propagation. The
instances are described in Table 1.<br><br>
<h4>Instances hardness</h4>
Most of these instances are, despite their size, quite easily
solved. For example, all the satisfiable instances are solved with at
most backtrack by SATZ (version41). Also, WalkSAT, a stochastic local
search algorithm, quite easily solves these instances (for example,
using the option -noise 70 100 these instance are solved, on average,
in approx.\ 20.000 to 60.000 variable flips, with
<i>ssa7552-038.cnf</i> being the hardest.<br><br>
Of the unsatisfiable instances only instances <i>ssa2670-130.cnf</i>
and <i>ssa2670-141.cnf</i> may be considered as hard, at least when
compared to the other unsatisfiable instances. For example, on the
first instance SATZ (version41) takes 17632 Backtracks, on the second
one 131352 Backtracks. Yet, with polynomial preprocessing techniques
(using the binary failed literal option in Jimmy Crawford's compact)
this latter instance becomes very easy for SATZ. The other instances
are all solved within at most 216 backtracks, instance
<i>ssa6288-047.cnf</i>, the largest of these instances, even in the
preprocessing steps of SATZ.
<!--The four satisfiable instances are easily solved by local search as
well as complete algorithms. For example, WalkSAT solves the four
instances with reasonable noise settings (for example, using the
option -noise 70 100) on average in roughly 20.000 to 60.000,
depending on the instance.
-->
<br><br>
<table border="1">
<tbody><tr>
<td align="center"><b>instance </b></td>
<td align="center"><b>vars </b></td>
<td align="center"><b>clauses </b></td>
<td align="center"><b>satisfiable? </b></td>
</tr>
<tr>
<td align="right">bf0432-007.cnf </td>
<td align="right">1040 </td>
<td align="right">3668 </td>
<td align="right">no </td>
</tr>
<tr>
<td align="right">bf1355-075.cnf </td>
<td align="right">2180 </td>
<td align="right">6778 </td>
<td align="right">no </td>
</tr>
<tr>
<td align="right">bf1355-638.cnf </td>
<td align="right">2177 </td>
<td align="right">4768 </td>
<td align="right">no </td>
</tr>
<tr>
<td align="right">bf2670-001.cnf </td>
<td align="right">1393 </td>
<td align="right">3434 </td>
<td align="right">no </td>
</tr>
<tr>
<td align="right">ssa0432-003.cnf </td>
<td align="right">435 </td>
<td align="right">1027 </td>
<td align="right">no </td>
</tr>
<tr>
<td align="right">ssa2670-130.cnf </td>
<td align="right">1359 </td>
<td align="right">3321 </td>
<td align="right">no </td>
</tr>
<tr>
<td align="right">ssa2670-141.cnf </td>
<td align="right">986 </td>
<td align="right">2315 </td>
<td align="right">no </td>
</tr>
<tr>
<td align="right">ssa6288-047.cnf </td>
<td align="right">10410 </td>
<td align="right">34238 </td>
<td align="right">no </td>
</tr>
<tr>
<td align="right">ssa7552-038.cnf</td>
<td align="right">1501 </td>
<td align="right">3575 </td>
<td align="right">yes </td>
</tr>
<tr>
<td align="right">ssa7552-158.cnf</td>
<td align="right">1363 </td>
<td align="right">3034 </td>
<td align="right">yes </td>
</tr>
<tr>
<td align="right">ssa7552-159.cnf</td>
<td align="right">1363 </td>
<td align="right">3032 </td>
<td align="right">yes </td>
</tr>
<tr nosave="">
<td align="right">ssa7552-160.cnf</td>
<td align="right">1391 </td>
<td align="right">3126 </td>
<td nosave="" align="right">yes </td>
</tr>
</tbody></table><br>
<b>Table 1:</b> Instances from circuit fault analysis.
<br>
<br>
More instances are available from the DIMACS ftp-site in this <a href="ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/contributed/UCSC/instances/">directory</a>.<br><br>
<table>
<tbody><tr>
<td valign="top"><small>[LF91] </small></td><td><small> <i><a href="http://www.cse.ucsc.edu/%7Efjf/">F.J. Ferguson</a> and <a href="http://www.cse.ucsc.edu/%7Elarrabee/">T. Larrabee</a>.</i>
<strong>Test Pattern Generation for Realistic Bridging Faults in CMOS
ICS.</strong> <cite>Proceedings of the International Testing
Conference,</cite> pages 492-499, 1991. <br> Also available as
Technical Report UCSC-CRL-91-30, Computer Research Laboratory,
University of California, Santa Cruz.</small><br>
</td></tr><tr>
<td valign="top"><small>[Lar92]
</small></td><td><small> <i><a href="http://www.cse.ucsc.edu/%7Elarrabee/">T. Larrabee</a>.</i>
<strong>Test Pattern Generation Using Boolean Satisfiability.</strong>
<cite>IEEE Transactions on Computer-Aided Design,</cite> 11(1):6-22, January 1992.
</small><br>
</td></tr></tbody></table>
<br>
</body></html>