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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Biere, A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation 4, 75–97 (2008)
Desrosiers, C., Galinier, P., Hertz, A., Paroz, S.: Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems. J. Comb. Optim. 18(2), 124–150 (2009)
Grégoire, É., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of Boolean clauses. In: Int’l. Conf. on Tools with Artificial Intelligence, pp. 74–83 (2008)
Jain, H., Clarke, E.M.: Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts. In: Proc. of the 46th Annual Design Automation Conference, pp. 563–568 (2009)
Järvisalo, M., Le Berre, D., Roussel, O.: Rules of the 2011 SAT Competition (2011), http://www.satcompetition.org/2011/
Kleine Büuning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, ch. 11, pp. 339–401. IOS Press, Amsterdam (2009)
Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7, 59–64 (2010)
Marques-Silva, J.: Minimal unsatisfiability: Models, algorithms and applications. In: Int’l Symposium on Multiple-Valued Logic, pp. 9–14 (2010)
Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 156–170. Springer, Heidelberg (2011)
Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Formal Methods in Computer- Aided Design (2010)
Schuppan, V.: Towards a notion of unsatisfiable cores for LTL. In: Fundamentals of Software Engineering. In: Third IPM Int’l Conference, pp. 129–145 (2010)
Tseitin, G.S.: On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic, Part II, pp. 115–125 (1968)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Belov, A., Marques-Silva, J. (2011). Minimally Unsatisfiable Boolean Circuits. In: Sakallah, K.A., Simon, L. (eds) Theory and Applications of Satisfiability Testing - SAT 2011. SAT 2011. Lecture Notes in Computer Science, vol 6695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21581-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-21581-0_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21580-3
Online ISBN: 978-3-642-21581-0
eBook Packages: Computer ScienceComputer Science (R0)