NP-completeness of small conflict set generation for congruence closure (bibtex)
by Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo
Abstract:
The efficiency of satisfiability modulo theories (SMT) solvers is dependent on the capability of theory reasoners to provide small conflict sets, i.e. small unsatisfiable subsets from unsatisfiable sets of literals. Decision procedures for uninterpreted symbols (i.e. congruence closure algorithms) date back from the very early days of SMT. Nevertheless, to the best of our knowledge, the complexity of generating smallest conflict sets for sets of literals with uninterpreted symbols and equalities had not yet been determined, although the corresponding decision problem was believed to be NP-complete. We provide here an NP-completeness proof, using a simple reduction from SAT.
Reference:
NP-completeness of small conflict set generation for congruence closureAndreas Fellner, Pascal Fontaine, Bruno Woltzenlogel PaleoFormal Methods in System Design, 2017.
Bibtex Entry:
@Article{Fellner2017,
  author   = {Fellner, Andreas and Fontaine, Pascal and Paleo, Bruno Woltzenlogel},
  title    = {NP-completeness of small conflict set generation for congruence closure},
  journal  = {Formal Methods in System Design},
  year     = {2017},
  issn     = {1572-8102},
  abstract = {The efficiency of satisfiability modulo theories (SMT) solvers is dependent on the capability of theory reasoners to provide small conflict sets, i.e. small unsatisfiable subsets from unsatisfiable sets of literals. Decision procedures for uninterpreted symbols (i.e. congruence closure algorithms) date back from the very early days of SMT. Nevertheless, to the best of our knowledge, the complexity of generating smallest conflict sets for sets of literals with uninterpreted symbols and equalities had not yet been determined, although the corresponding decision problem was believed to be NP-complete. We provide here an NP-completeness proof, using a simple reduction from SAT.},
  doi      = {10.1007/s10703-017-0283-x},
  url      = {http://dx.doi.org/10.1007/s10703-017-0283-x},
}
Powered by bibtexbrowser