Abstract
Blocked clause elimination is a powerful technique in SAT solving. In recent work, it has been shown that it is possible to decompose any propositional formula into two subsets (blocked sets) such that both can be solved by blocked clause elimination. We extend this work in several ways. First, we prove new theoretical properties of blocked sets. We then present additional and improved ways to efficiently solve blocked sets. Further, we propose novel decomposition algorithms for faster decomposition or which produce blocked sets with desirable attributes. We use decompositions to reencode CNF formulas and to obtain circuits, such as AIGs, which can then be simplified by algorithms from circuit synthesis and encoded back to CNF. Our experiments demonstrate that these techniques can increase the performance of the SAT solver Lingeling on hard to solve application benchmarks.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355–370. Springer, Heidelberg (2012)
Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96–97, 149–176 (1999)
Järvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010)
Järvisalo, M., Biere, A., Heule, M.J.H.: Simulating circuit-level simplifications on cnf. Journal of Automated Reasoning 49(4), 583–619 (2012)
Heule, M.J.H., Biere, A.: Blocked clause decomposition. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 423–438. Springer, Heidelberg (2013)
Parkes, A.J.: Clustering at the phase transition. In: Proc. of the 14th Nat. Conf. on AI, pp. 340–345. AAAI Press / The MIT Press (1997)
Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. In: Balint, A., Belov, M.J.H., Heule, M. (eds.) Proceedings of SAT Competition 2013. Department of Computer Science Series of Publications B, vol. B-2013-1, pp. 51–52. University of Helsinki (2013)
Mishchenko, A., Chatterjee, S., Brayton, R.K.: DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In: Sentovich, E. (ed.) Proceedings of the 43rd Design Automation Conference (DAC 2006), pp. 532–535. ACM (2006)
Brayton, R., Mishchenko, A.: Abc: An academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 21(12) (2002)
Balint, A., Schöning, U.: Choosing probability distributions for stochastic local search and the role of make versus break. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 16–29. Springer, Heidelberg (2012)
Balint, A., Fröhlich, A.: Improving stochastic local search for sat with a new probability distribution. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 10–15. Springer, Heidelberg (2010)
Li, C., Fan, Y.: Cca2013. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Balyo, T., Fröhlich, A., Heule, M.J.H., Biere, A. (2014). Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask). In: Sinz, C., Egly, U. (eds) Theory and Applications of Satisfiability Testing – SAT 2014. SAT 2014. Lecture Notes in Computer Science, vol 8561. Springer, Cham. https://doi.org/10.1007/978-3-319-09284-3_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-09284-3_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09283-6
Online ISBN: 978-3-319-09284-3
eBook Packages: Computer ScienceComputer Science (R0)