Mark Liffiton

mliffito -at- domain

CAMUS

Compute All Minimal Unsatisfiable Subsets
[pronounced "ka-moo" after the French writer]

CAMUS is a set of algorithms for finding all minimal correction sets (MCSes) and minimal unsatisfiable subsets (MUSes) of overconstrained/infeasible constraint systems. The algorithms are not at all domain-specific; they are applicable to any type of constraint system. The best reference for CAMUS is our paper in the Journal of Automated Reasoning:

Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints
Mark H. Liffiton and Karem A. Sakallah
Journal of Automated Reasoning, 40(1):1-33, January 2008.
(The original publication is available at www.springerlink.com here.)

I have developed implementations of CAMUS for Boolean Satisfiability (SAT), Disjunctive Temporal Problems (DTPs - work done with Michael Moffitt), and Satisfiability Modulo Theories (SMT). The SMT implementation is built on top of YICES, and though SMT subsumes both Boolean SAT and DTPs, those two implementations perform better on their specific constraint theories than the SMT version.

The SMT implementation has been integrated into Reveal, a Verilog model equivalence checker for hardware verification developed by Zaher Andraus. I am always looking for further constraint types and applications for CAMUS.

Download

The implementation of CAMUS for Boolean SAT instances is available as source code under the University of Michigan's license. [Please note that this implementation of CAMUS is built on a now-very-old, outdated version of MiniSAT (v1.12b). An implementation of the algorithm with a modern SAT solver would likely perform much better.]

Latest Release: CAMUS 1.0.6 [.tar.gz archive]

This release includes the option to boost the first phase of CAMUS using unsatisfiable cores as published in SAT-2009:

Generalizing Core-Guided Max-SAT
Mark H. Liffiton and Karem A. Sakallah
Proc. 12th Conf. on Theory and App. of Satisfiability Testing (SAT-2009), 481-494, June 2009.

Results

The following tables list experimental results for our implementation of CAMUS for Boolean satisfiability. They contain more detailed data than included in my papers (limited by space constraints). In addition to data on the performance of CAMUS, these results contain characteristics of the resulting MUSes (number and size, mainly), which may be of interest to other researchers.

In the implementation used here, the first phase of CAMUS is built on MiniSAT version 1.12b. The entire implementation is written in C++, compiled for the x86-64 instruction set by the g++ compiler with the -O3 optimization flag. All experiments were run in Linux on 3.0GHz Intel Core 2 Duo with 3GB of RAM.

Select a benchmark family for details and results: