## Abstract

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 language | English |
---|---|

Title of host publication | Theory and Applications of Satisfiability Testing – SAT 2016 |

Subtitle of host publication | 19th International Conference Bordeaux, France, July 5–8, 2016 Proceedings |

Editors | Nadia Creignou, Daniel Le Berre |

Place of Publication | Cham Switzerland |

Publisher | Springer |

Pages | 342-360 |

Number of pages | 19 |

ISBN (Electronic) | 9783319409702 |

ISBN (Print) | 9783319409696 |

DOIs | |

Publication status | Published - 2016 |

Externally published | Yes |

Event | International Conference on Theory and Applications of Satisfiability Testing 2016 - Bordeaux, France Duration: 5 Jul 2016 → 8 Jul 2016 Conference number: 19th https://sat2016.labri.fr/ |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 9710 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | International Conference on Theory and Applications of Satisfiability Testing 2016 |
---|---|

Abbreviated title | SAT 2016 |

Country/Territory | France |

City | Bordeaux |

Period | 5/07/16 → 8/07/16 |

Internet address |

## Keywords

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