MCS extraction with sublinear oracle queries

Carlos Mencía, Alexey Ignatiev, Alessandro Previti, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

18 Citations (Scopus)


Given an inconsistent set of constraints, an often studied problem is to compute an irreducible subset of the constraints which, if relaxed, enable the remaining constraints to be consistent. In the case of unsatisfiable propositional formulas in conjunctive normal form, such irreducible sets of constraints are referred to as Minimal Correction Subsets (MCSes). MCSes find a growing number of applications, including the approximation of maximum satisfiability and as an intermediate step in the enumeration of minimal unsatisfiability. A number of efficient algorithms have been proposed in recent years, which exploit a wide range of insights into the MCS extraction problem. One open question is to find the best worst-case number of calls to a SAT oracle, when the calls to the oracle are kept simple, and given reasonable definitions of simple SAT oracle calls. This paper develops novel algorithms for computing MCSes which, in specific settings, are guaranteed to require asymptotically fewer than linear calls to a SAT oracle, where the oracle calls can be viewed as simple. The experimental results, obtained on existing problem instances, demonstrate that the new algorithms contribute to improving the state of the art.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2016
Subtitle of host publication19th International Conference Bordeaux, France, July 5–8, 2016 Proceedings
EditorsNadia Creignou, Daniel Le Berre
Place of PublicationCham Switzerland
Number of pages19
ISBN (Electronic)9783319409702
ISBN (Print)9783319409696
Publication statusPublished - 2016
Externally publishedYes
EventInternational Conference on Theory and Applications of Satisfiability Testing 2016 - Bordeaux, France
Duration: 5 Jul 20168 Jul 2016
Conference number: 19th

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2016
Abbreviated titleSAT 2016
Internet address


  • Conjunctive Normal Form
  • Cardinality Constraint
  • Conjunctive Normal Form Formula
  • Oracle Query
  • Oracle Call

Cite this