NP-completeness of small conflict set generation for congruence closure

DOI10.1007/s10703-017-0283-xzbMath1377.68090OpenAlexW2693644836WikidataQ59521641 ScholiaQ59521641MaRDI QIDQ1688538

Pascal Fontaine, Bruno Woltzenlogel Paleo, Andreas Fellner

Publication date: 8 January 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-017-0283-x

zbMATH Keywords

complexitysatisfiability modulo theoriesdecision procedurescongruence closure

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

NP-completeness of small conflict set generation for congruence closure

Uses Software

• Skeptik

Cites Work

• Unnamed Item
• Fast congruence closure and extensions
• NP-completeness of small conflict set generation for congruence closure
• Fast Decision Procedures Based on Congruence Closure
• Variations on the Common Subexpression Problem
• Term Rewriting and Applications