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.