On-the-fly resolve trace minimization

ABSTRACT

The ability of modern SAT solvers to produce proofs of un-satisfiability for Boolean formulas has become a powerful tool for EDA applications. Proofs are generated from a resolve trace that captures information about the creation of all conflict clauses. Due to their sizes, resolve traces are kept in files. The sizes of these files makes the use of proofs of un-satisfiability impractical for industrial tools. Although only a small part of the resolve trace is eventually used, until now it was not known how to filter out unnecessary information.

We propose a simple algorithm for on-the-fly resolve trace minimization in which we identify clauses that are guaranteed not to take part in the proof of unsatisfiability, and delete all of their associated information. This algorithm dramatically decreases the size of the resolve trace, to the point where it can be stored in the main memory. Our experiments reveal that the minimized trace is typically 3 to 6 times smaller. This makes the use of proofs of unsatisfiability and the computation of unsat cores more practical and will enable future applications to take advantage of it.

REFERENCES

• 1: IBM Formal Verification Benchmarks Library.
• 2: IBM RuleBase Parallel Edition. 2004.
• 3: R. J. Jr. Bayardo and R. C. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In IICAI, 1997.
• 4: D. Le Berre and L. Simon. SAT competition. 2005.
• 5: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 6: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 7: N. Een and N. Sorensson. An Extensible SAT-solver. In SAT, 2003.
• 8: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 9: K. L. McMillan. Interpolation and SAT-Based Model Checking. In CAV, 2003.
• 10: K. L. McMillan and N. Amla. Automatic Abstraction without Counterexamples. In TACAS, 2003.
• 11: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 12: Ofer Shtrichman, Pruning Techniques for the SAT-Based Bounded Model Checking Problem, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.58-70, September 04-07, 2001
• 13: Chao Wang , HoonSang Jin , Gary D. Hachtel , Fabio Somenzi, Refining the SAT decision ordering for bounded model checking, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996713]
• 14: Jesse Whittemore , Joonyoung Kim , Karem Sakallah, SATIRE: a new incremental satisfiability engine, Proceedings of the 38th conference on Design automation, p.542-545, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379019]
• 15: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 16: L. Zhang and S. Malik. Extracting small unsatisfiable cores from unsatisfiable Boolean formulas. In SAT, 2003.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Verification

Keywords:
SAT solvers, SAT-based verification, unsatisfiable core