Abstract
We describe a new decision-making procedure for resolution-based SAT-solvers called Decision Making with a Reference Point (DMRP). In DMRP, a complete assignment called a reference point is maintained. DMRP is aimed at finding a change of the reference point under which the number of clauses falsified by the modified point is smaller than for the original one. DMRP makes it possible for a DPLL-like algorithm to perform a ”local search strategy”. We describe a SAT-algorithm with conflict clause learning that uses DMRP. Experimental results show that even a straightforward and unoptimized implementation of this algorithm is competitive with SAT-solvers like BerkMin and Minisat on practical formulas. Interestingly, DMRP is beneficial not only for satisfiable but also for unsatisfiable formulas.
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
Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking (a book chapter). In: Zelkovitz, M. (ed.) Advances in computers, vol. 58, Elsevier, Amsterdam (2003)
Davis, M., Longemann, G., Loveland, D.: A Machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)
Een, N., Sorensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 503–518. Springer, Heidelberg (2004)
Fang, H., Ruml, W.: Complete Local Search for Propositional Satisfiability. In: Proc. of 19th National Conference on Artificial Intelligence, pp. 161–166 (2004)
Gelder, A.V.: Autarky pruning in propositional model elimination reduces failure redundancy. J. of Autom. Reasoning 23(2), 137–193 (1999)
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., Novikov, Y.: BerkMin: a Fast and Robust SAT-Solver. In: DATE 2002, Paris, pp. 142–149 (2002)
Gomes, C.P., Selman, B., Kautz, H.: Boosting Combinatorial Search Through Randomization. In: Proc. AAAI 1998 (1998)
Habet, D., Li, C.M., Devendeville, L., Vasquez, M.: A hybrid approach for SAT. In: Int. Conf. on Principles and Practice of Constraint Programming, pp. 172–184 (2002)
Hirsch, E.A., Kojevnikov, A.: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. Annals of Math. and Artif. Intell. 43(1-4), 91–111 (2005)
Hoos, H., Stutzle, T.: Stochastic Local Search: Foundations and Applications. Morgan Kaufmann, San Francisco (CA) (2004)
Katz, J., Hanna, Z., Dershowitz, N.: Space-efficient Bounded Model Checking. In: DATE 2005, pp. 686–687 (2005)
Kullmann, O.: Investigations on autark assignments. Discrete Applied Mathematics 107, 99–137 (2000)
Li, C.M.: A constrained-based approach to narrow search trees for satisfiability. Information processing letters 71, 75–80 (1999)
Mazure, B., Sais, L., Gregoire, R.: Boosting complete techniques thanks to local search methods. Annals of Math. and Artif. Intell. 22, 319–331 (1998)
Monien, B., Speckenmeyer, E.: Solving satisfiability in less than \(\mathit{2^n}\) steps. Discrete Applied Mathematics 10, 287–295 (1985)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001 (2001)
Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. STTT 7(2), 16–173 (2005)
Prestwich, S.: Local search and backtracking vs. non-systematic backtracking. In: AAAI Fall Symposium on Using Uncertainty Within Computation, North Falmouth, Cape Cod, MA, November 2-4, 2001, pp. 109–115 (2001)
Selman, B., Levesque, H., Mitchell, D.: A New Method for Solving Hard Satisfiability Problems. In: AAAI 1992, pp. 440–446 (1992)
Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: AAAI 1994, Seattle, pp. 337–343 (1994)
Silva, J.P.M., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions of Computers 48, 506–521 (1999)
Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. In: ICCAD 2001 (2001)
Zhang, H.: SATO: An efficient propositional prover. In: International Conference on Automated Deduction, July 1997, pp. 272–275 (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goldberg, E. (2008). A Decision-Making Procedure for Resolution-Based SAT-Solvers. In: Kleine Büning, H., Zhao, X. (eds) Theory and Applications of Satisfiability Testing – SAT 2008. SAT 2008. Lecture Notes in Computer Science, vol 4996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79719-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-79719-7_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79718-0
Online ISBN: 978-3-540-79719-7
eBook Packages: Computer ScienceComputer Science (R0)