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.
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.
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.
Runtime, memory usage, and output counts for varying time limits comparing three variants of MARCO and two previously published algorithms (CAMUS and DAA).
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.
MARCO was first presented in CPAIOR 2013:
Previti and Marques-Silva's eMUS was presented in AAAI 2013: