Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization

James Bailey, Peter J. Stuckey

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

124 Citations (Scopus)

Abstract

An unsatisfiable set of constraints is minimal if all its (strict) subsets are satisfiable. The task of type error diagnosis requires finding all minimal unsatisfiable subsets of a given set of constraints (representing an error), in order to generate the best explanation of the error. Similarly circuit error diagnosis requires finding all minimal unsatisfiable subsets in order to make minimal diagnoses. In this paper we present a new approach for efficiently determining all minimal unsatisfiable sets for any kind of constraints. Our approach makes use of the duality that exists between minimal unsatisfiable constraint sets and maximal satisfiable constraint sets. We show how to incrementally compute both these sets, using the fact that the complements of the maximal satisfiable constraint sets are the hitting sets of the minimal unsatisfiable constraint sets. We experimentally compare our technique to the best known method on a number of large type problems and show that considerable improvements in running time are obtained.

Original languageEnglish
Title of host publicationPractical Aspects of Declarative Languages
Subtitle of host publication7th International Symposium, PADL 2005 Long Beach, CA, USA, January 10-11, 2005 Proceedings
EditorsManuel Hermenegildo, Daniel Cabeza
Place of PublicationBerlin Germany
PublisherSpringer
Pages174-186
Number of pages13
ISBN (Print)3540243623
DOIs
Publication statusPublished - 1 Sep 2005
Externally publishedYes
Event7th International Symposium on Practical Aspects of Declarative Languages, PADL 2005 - Long Beach, United States of America
Duration: 10 Jan 200511 Jan 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume3350
ISSN (Print)0302-9743

Conference

Conference7th International Symposium on Practical Aspects of Declarative Languages, PADL 2005
CountryUnited States of America
CityLong Beach
Period10/01/0511/01/05

Keywords

  • Constraint solving
  • Hitting sets
  • Hypergraph transversals
  • Minimal unsatisfiable sets

Cite this