Abstract
Many state-of-the-art SAT solvers use the VSIDS heuristic to make branching decisions based on the activity of variables or literals. In combination with rapid restarts and phase saving this yields a powerful decision heuristic in practice. However, there are approaches that motivate more in-depth reasoning to guide the search of the SAT solver. But more reasoning often requires more information and comes along with more complex data structures. This may sometimes even cause strong concepts to be inapplicable in practice.
In this paper we present a suitable data structure for the DMRP approach to overcome the problem above. Moreover, we show how DMRP can be combined with CDCL solving to be competitive to state-of-the-art solvers and to even improve on some families of industrial instances.
This work was supported by DFG-SPP 1307, project “Structure-based Algorithm Engineering for SAT-Solving”.
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
Bacchus, F.: Exploring the computational tradeoff of more reasoning and less searching. In: SAT 2002, pp. 7–16 (2002)
Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 28–33. Springer, Heidelberg (2008)
Biere, A.: Picosat essentials. JSAT 4, 75–97 (2008)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. ACM Commun. 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
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)
Fukunaga, A.S.: Efficient Implementations of SAT Local Search. In: SAT (2004)
Goldberg, E.: Determinization of resolution by an algorithm operating on complete assignments. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 90–95. Springer, Heidelberg (2006)
Goldberg, E.: A decision-making procedure for resolution-based SAT-solvers. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 119–132. Springer, Heidelberg (2008)
Ivancic, F., Yang, Z., Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. Theoretical Computer Science 404(3) (2008)
Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proceedings of the Tenth European Conference on Artificial Intelligence ECAI 1992, pp. 359–363 (1992)
Kottler, S.: Solver descriptions for the SAT competition (2009), satcompetition.org
Küchlin, W., Sinz, C.: Proving consistency assertions for automotive product data management. J. Automated Reasoning 24(1-2), 145–163 (2000)
Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of las vegas algorithms. In: ISTCS, pp. 128–133 (1993)
Lynce, I., Marques-Silva, J.: SAT in bioinformatics: Making the case with haplotype inference. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 136–141. Springer, Heidelberg (2006)
Marques-Silva, J.P.: Practical Applications of Boolean Satisfiability. In: Workshop on Discrete Event Systems, WODES 2008 (2008)
Marques-Silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC (2001)
Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007)
Selman, B., Levesque, H., Mitchell, D.: A new method for solving hard satisfiability problems. In: Tenth National Conference on Artificial Intelligence (1992)
Velev, M.N.: Using rewriting rules and positive equality to formally verify wide-issue out-of-order microprocessors with a reorder buffer. In: DATE 2002 (2002)
Zheng, L., Stuckey, P.J.: Improving SAT using 2SAT. In: Proceedings of the 25th Australasian Computer Science Conference, pp. 331–340. E (2002)
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
Kottler, S. (2010). SAT Solving with Reference Points. 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_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-14186-7_13
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)