Abstract
Automated reasoning tasks in many real-world domains involve analysis of redundancies in unsatisfiable instances of SAT. In CNF-based instances, some of the redundancies can be captured by computing a minimally unsatisfiable subset of clauses (MUS). However, the notion of MUS does not apply directly to non-clausal instances of SAT, particularly those that are represented as Boolean circuits. In this paper we identify certain types of redundancies in unsatisfiable Boolean circuits, and propose a number of algorithms to compute minimally unsatisfiable, that is, irredundant, subcircuits. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Belov, A., & Marques-Silva, J. (2011). Minimally unsatisfiable Boolean circuits. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6695 LNCS, pp. 145–158). https://doi.org/10.1007/978-3-642-21581-0_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
