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:
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.
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.]
This release uses unsatisfiable cores to boost the first phase of CAMUS as published in SAT-2009:
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: