# Instances from circuit fault analysis

The following description is based on the description given by Allen van Gelder and Yumi Tsuji. The original description can be found here.
The instances given here are selected formulas from those generated by Nemesis. Nemesis is a test-pattern generation program described in [LF91,Lar92].
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.
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.
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.
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.
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 here.
Formulas are in DIMACS Challenge cnf format. A separate directory, Cnfparse, has a parser and example programs using the parser.

#### Benchmark instances

There are four benchmark instances which test for bridge faults and eight instances which test for single-at-stuck 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.

#### Instances hardness

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 ssa7552-038.cnf being the hardest.
Of the unsatisfiable instances only instances ssa2670-130.cnf and ssa2670-141.cnf 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 ssa6288-047.cnf, the largest of these instances, even in the preprocessing steps of SATZ.

instance | vars | clauses | satisfiable?
bf0432-007.cnf | 1040 | 3668 | no
bf1355-075.cnf | 2180 | 6778 | no
bf1355-638.cnf | 2177 | 4768 | no
bf2670-001.cnf | 1393 | 3434 | no
ssa0432-003.cnf | 435 | 1027 | no
ssa2670-130.cnf | 1359 | 3321 | no
ssa2670-141.cnf | 986 | 2315 | no
ssa6288-047.cnf | 10410 | 34238 | no
ssa7552-038.cnf | 1501 | 3575 | yes
ssa7552-158.cnf | 1363 | 3034 | yes
ssa7552-159.cnf | 1363 | 3032 | yes
ssa7552-160.cnf | 1391 | 3126 | yes

Table 1: Instances from circuit fault analysis.
More instances are available from the DIMACS ftp-site in this directory.

[LF91] | F.J. Ferguson and T. Larrabee. Test Pattern Generation for Realistic Bridging Faults in CMOS ICS. Proceedings of the International Testing Conference, pages 492-499, 1991. Also available as Technical Report UCSC-CRL-91-30, Computer Research Laboratory, University of California, Santa Cruz.
[Lar92] | T. Larrabee. Test Pattern Generation Using Boolean Satisfiability. IEEE Transactions on Computer-Aided Design, 11(1):6-22, January 1992.