MARCO§
Mapping Regions of Constraint sets
[named after the Venetian explorer Marco Polo]
MARCO is an algorithm for enumerating minimal unsatisfiable subsets (MUSes) and minimal correction sets (MCSes) of unsatisfiable/infeasible constraint sets. The algorithm is not at all domain-specific; it is applicable to any type of constraint system. Compared to CAMUS, which also enumerates MUSes and MCSes, MARCO produces MUSes earlier in its execution and more steadily. On many instances, the first phase of CAMUS cannot complete within any reasonable time limit (due to the general intractability of the problem it is solving) and produces no results, while MARCO can output multiple MUSes on the same instance.
Independently, Alessandro Previti and Joao Marques-Silva developed a very similar algorithm they named eMUS, with an earlier implementation available on their site. The MARCO implementation here incorporates our later joint work.
For a quick, visual overview of the algorithm, see our interactive algorithm visualization.
Download§
This Python implementation of MARCO accepts both Boolean SAT (in CNF and group-oriented GCNF formats) and SAT Modulo Theories (SMT) instances. It uses the MUSer2 MUS extraction tool for SAT instances, and it can use Z3 for SMT instances, if available. From version 2.0, it includes the MARCOs parallel implementation as well (accessible via command line flags), and v3.0 runs in parallel by default.
Latest release, code on Github: liffiton/MARCO (releases)
Please see the included README file for further details, and let me know if you have any questions or run into issues. I'd also appreciate a quick note about your use of MARCO if you apply it or extend it in some way.
I am always looking for further constraint types and applications for MARCO, and I'm happy to provide assistance in determining how best to apply it to any particular problem. There are several experimental features that may prove useful in any given context.
Experimental Data§
Runtime, memory usage, and output counts for varying time limits comparing three variants of MARCO and two previously published algorithms (CAMUS and DAA).
enumeration_results_201312.ods [OpenDocument Spreadsheet w/ formatting]
enumeration_results_201312.csv [raw CSV]
- Instances: 300 CNF instances used in the MUS track of the 2011 SAT Competition — download [600MB .tar file]
- Hardware: Amazon Elastic Compute Cloud cc2.8xlarge instances (thanks to an AWS in Education Grant award)
- CPU: 2 x 8-core 2.60GHz Intel Xeon E5-2670
- Memory: 60.5 GiB
- 16 parallel instances per node (one per physical core)
- Time limit: 3600 seconds (output counts also reported for 10, 60, and 600 seconds)
- Memory limit: 3000 MB (per instance)
References§
The ICTAI paper presents the parallel implementation ("MARCOs"), while the Constraints journal paper provides the most complete reference for this work. We have also created an interactive algorithm visualization for MARCO that complements the papers.
Wenting Zhao and Mark H. Liffiton
in Proc. 28th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2016), November 2016.
Mark H. Liffiton, Alessandro Previti, Ammar Malik, and João Marques-Silva
Constraints, 21(2):223-250, 2016.
[Springer's published version is available here.]
MARCO was first presented in CPAIOR 2013:
Mark H. Liffiton and Ammar Malik
in Proc. 10th International Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) techniques in Constraint Programming (CPAIOR-2013), 160-175, May 2013.
Previti and Marques-Silva's eMUS was presented in AAAI 2013:
Alessandro Previti and Joao Marques-Silva
in Proc. 27th Conference on Artificial Intelligence (AAAI-13), 818-825, July 2013.
[PDF available on their site]