NPE-1.0 in CNF Format
==========================================================================

Author:      Miroslav N. Velev
             mvelev@ece.cmu.edu
             http://www.ece.cmu.edu/~mvelev

Date:        March 23, 2002


Description
----------------------------
6 CNF formulas generated in microprocessor formal verification without
exploiting the property of Positive Equality.

3 of the formulas, *bug*.cnf, should be satisfiable, while the 
other 3 formulas should be unsatisfiable.


Conditions of Availability
----------------------------
1. Email Miroslav (mvelev@ece.cmu.edu) about any papers that you publish
   and that use these benchmarks.

2. In any publication that uses this benchmark suite, reference the paper 
   that describes how the benchmarks were generated:

   M.N. Velev, and R.E. Bryant, "Effective Use of Boolean Satisfiability 
   Procedures in the Formal Verification of Superscalar and 
   VLIW Microprocessors," 38th Design Automation Conference (DAC '01), 
   June 2001, pp. 226-231.


Note
----------------------------
The two biggest benchmarks are approximately 327 MB when uncompressed with 'gunzip',
and have close to 900,000 CNF variables and 15 million clauses.