Mark Liffiton

mliffito -at- domain

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).

Latest Release: MARCO 2.0 [.tar.gz archive]

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]

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.

Parallelizing Partial MUS Enumeration
Wenting Zhao and Mark H. Liffiton
in Proc. 28th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2016), [to appear], November 2016.
Fast, Flexible MUS Enumeration
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:

Enumerating Infeasibility: Finding Multiple MUSes Quickly
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:

Partial MUS Enumeration
Alessandro Previti and Joao Marques-Silva
in Proc. 27th Conference on Artificial Intelligence (AAAI-13), 818-825, July 2013.
[PDF available on their site]