## Abstract

Minimal explanations of infeasibility are of great interest in many domains. In propositional logic, these are referred to as Minimal Unsatisfiable Subsets (MUSes). An unsatisfiable formula can have multiple MUSes, some of which provide more insights than others. Different criteria can be considered in order to identify a good minimal explanation. Among these, the size of an MUS is arguably one of the most intuitive. Moreover, computing the smallest MUS (SMUS) finds several practical applications that include validating the quality of the MUSes computed by MUS extractors and finding equivalent subformulae of smallest size, among others. This paper develops a novel algorithm for computing a smallest MUS, and we show that it outperforms all the previous alternatives pushing the state of the art in SMUS solving. Although described in the context of propositional logic, the presented technique can also be applied to other constraint systems.

Original language | English |
---|---|

Title of host publication | Principles and Practice of Constraint Programming |

Subtitle of host publication | 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings |

Editors | Gilles Pesant |

Place of Publication | Cham Switzerland |

Publisher | Springer |

Pages | 173-182 |

Number of pages | 10 |

ISBN (Electronic) | 9783319232195 |

ISBN (Print) | 9783319232188 |

DOIs | |

Publication status | Published - 2015 |

Externally published | Yes |

Event | International Conference on Principles and Practice of Constraint Programming 2015 - Cork, Ireland Duration: 31 Aug 2015 → 4 Sep 2015 Conference number: 21st https://web.archive.org/web/20150810094235/http://booleconferences.ucc.ie/cp2015 |

### Publication series

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

Publisher | Springer |

Volume | 9255 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | International Conference on Principles and Practice of Constraint Programming 2015 |
---|---|

Abbreviated title | CP 2015 |

Country | Ireland |

City | Cork |

Period | 31/08/15 → 4/09/15 |

Internet address |

## Keywords

- Propositional Logic
- Conjunctive Normal Form
- Propositional Formula
- Conjunctive Normal Form Formula
- Minimal Explanation