Fast, flexible MUS enumeration
Session date: 2 October 2023
Session host: Konstantin Sidorov
Summary:
In this session, I will review the MARCO (Ma</string>pping Regions of Constraints) algorithm for enumerating all MUSes of a given constraint system (i.e., constraint subsets that are minimally infeasible). In particular, MARCO is constraint-agnostic: it requires an oracle that outputs SAT/UNSAT given a constraint set but does not require any further insight into the constraint structure.