Abstract
In this paper we describe a significant improvement to the justificationbased local search algorithm for circuit satisfiability proposed by Järvisalo et al [7]. By carefully combining local search with Boolean Constraint Propagation we achieve multiple orders of magnitude reduction in run-time on industrial and structured benchmark circuits, and, in some cases, performance comparable with complete SAT solvers.
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.
References
Belov, A., Stachniak, Z.: Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 258–264. Springer, Heidelberg (2009)
Belov, A.: Stochastic Local Search for Non-Clausal and Circuit Satisfiability. In: preparation PhD Thesis, York University, Toronto, Canada (2010)
Crawford, J.M., Kearns, M.J., Shapire, R.E.: The Minimal Disagreement Parity Problem as Hard Satisfiability Problem. Tech. report CIRL and ATT Bell Labs (1994)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Hirsch, E.A., Kojevnikov, A.: UnitWalk: A New SAT Solver that Uses Local Search Guided by Unit Clause Elimination. Annals of Mathematics and Artificial Intelligence (2005)
Hoos, H.H., Stutzle, T.: Local Search Algorithms for SAT: An Empirical Evaluation. J. of Automated Reasoning (2000)
Järvisalo, M., Junttila, T., Niemelä, I.: Justification-Based Non-Clausal Local Search for SAT. In: Proc. of ECAI 2008 (2008)
Junttila, T.: The BC Package and a File Format for Constrained Boolean Circuits, http://www.tcs.hut.fi/~tjunttil/bcsat/
Kuehlmann, A., Ganai, M., Paruthi, V.: Circuit-based Boolean Reasoning. In: Proc. of DAC 2001 (2001)
Pham, D.N., Thornton, J., Sattar, A.: Building Structure into Local Search for SAT. In: Proc. of IJCAI 2007 (2007)
Velev, M.N., http://www.ece.cmu.edu/~mvelev
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Belov, A., Stachniak, Z. (2010). Improved Local Search for Circuit Satisfiability. In: Strichman, O., Szeider, S. (eds) Theory and Applications of Satisfiability Testing – SAT 2010. SAT 2010. Lecture Notes in Computer Science, vol 6175. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14186-7_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-14186-7_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14185-0
Online ISBN: 978-3-642-14186-7
eBook Packages: Computer ScienceComputer Science (R0)