NP-completeness of small conflict set generation for congruence closure

Andreas Fellner; Pascal Fontaine; Bruno Woltzenlogel Paleo

doi:10.1007/s10703-017-0283-x

NP-completeness of small conflict set generation for congruence closure

Andreas Fellner^*, Pascal Fontaine, Bruno Woltzenlogel Paleo

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

2 Citations (Scopus)

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.

Original language	English
Pages (from-to)	533-544
Number of pages	12
Journal	Formal Methods in System Design
Volume	51
Issue number	3
DOIs	https://doi.org/10.1007/s10703-017-0283-x
Publication status	Published - 1 Dec 2017

Access to Document

10.1007/s10703-017-0283-x

Cite this

@article{8c571b30b12e4d1d83076b0cc7cbcec8,

title = "NP-completeness of small conflict set generation for congruence closure",

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.",

keywords = "Complexity, Congruence closure, Decision procedures, Satisfiability modulo theories",

author = "Andreas Fellner and Pascal Fontaine and Paleo, {Bruno Woltzenlogel}",

note = "Publisher Copyright: {\textcopyright} 2017, The Author(s).",

year = "2017",

month = dec,

day = "1",

doi = "10.1007/s10703-017-0283-x",

language = "English",

volume = "51",

pages = "533--544",

journal = "Formal Methods in System Design",

issn = "0925-9856",

publisher = "Springer Netherlands",

number = "3",

}

TY - JOUR

T1 - NP-completeness of small conflict set generation for congruence closure

AU - Fellner, Andreas

AU - Fontaine, Pascal

AU - Paleo, Bruno Woltzenlogel

PY - 2017/12/1

Y1 - 2017/12/1

N2 - 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.

AB - 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.

KW - Complexity

KW - Congruence closure

KW - Decision procedures

KW - Satisfiability modulo theories

UR - http://www.scopus.com/inward/record.url?scp=85021096697&partnerID=8YFLogxK

U2 - 10.1007/s10703-017-0283-x

DO - 10.1007/s10703-017-0283-x

M3 - Article

SN - 0925-9856

VL - 51

SP - 533

EP - 544

JO - Formal Methods in System Design

JF - Formal Methods in System Design

IS - 3

ER -

NP-completeness of small conflict set generation for congruence closure

Abstract

Access to Document

Other files and links

Fingerprint

Cite this