cnf-ssa:                         ykt, avg 930707

This directory contains the selected formulas from those generated by Nemesis.
Nemesis is a test-pattern generation program described by
Tracy Larrabee in:

  "Test Pattern Generation for Realistic Bridging Faults in CMOS ICs,"
  with Joe Ferguson, Proceedings of the International Testing Conference,
  Nashville, TN, October 1991.
  Also available as Technical Report UCSC-CRL-91-30,
  Computer Research Laboratory, University of California, Santa Cruz.

  "Test Pattern Generation Using Boolean Satisfiability",
  IEEE Transactions on Computer-Aided Design, 11(1):6-22, January 1992.

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.

We select 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.

We apply further deterministic polynomial time tests 
on the formulas generated by Nemesis to eliminate those that can
be easily processed.  The details of this screening will be described
elsewhere, but it eliminates both satisfiable and unsatisfiable
formulas.  For example, a formula that is unsatisfiable based on
the Krom clauses alone will be 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 contributed in the Cnfparse directory
under UCSC.  

Formula    #fmlas   #fmls  #fmls   #fmlas  #fmlas        comments
subdirs    producd  unsat  solved  solved  selected
           by       Krom   subseq  subseq
           Nemesis  part   by      by 
                           3clng   maxsat
---------------------------------------------------------------------
tdl432.ssa     16      8       1       0     < 7>     
tdl1355.ssa     8      0       8       0     < 0>
tdl2670.ssa   141     27      43      59     <12>
tdl6288.ssa    51     48       0       0     < 3>   over 10000 vars
tdl7552.ssa   163     30      25      28     <80>

Formulas are in Dimacs Challenge cnf format.  A separate directory,
Cnfparse, has a parser and example programs using the parser.

Contributed by Yumi Tsuji and Allen Van Gelder,
University of California, Santa Cruz.  tsuji@cs.ucsc.edu, avg@cs.ucsc.edu