Abstract
HypBinRes, a particular form of hyper-resolution, was first employed in the SAT solver 2cls+eq. In 2cls+eq, HypBinRes and equality reduction are used at every node of a DPLL search tree, pruning much of the search tree. This allowed 2cls+eq to display the best all-around performance in the 2002 SAT solver competition. In particular, it was the only solver to qualify for the second round of the competition in all three benchmark categories. In this paper we investigate the use of HypBinRes and equality reduction in a preprocessor that can be used to simplify a CNF formula prior to SAT solving. We present empirical evidence demonstrating that such a preprocessor can be extremely effective on large structured problems, making some previously unsolvable problems solvable. The preprocessor is also able to solve a number of non-trivial instances by itself. Since the preprocessor does not have to worry about undoing changes on backtrack, nor about keeping track of reasons for intelligent backtracking, we are able to develop a new algorithm for applying HypBinRes that can be orders of magnitude more efficient than the algorithm employed inside of 2cls+eq. The net result is a technique that improves our ability to solve hard problems SAT problems.
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
Bacchus, F.: Enhancing davis putnam with extended binary clause reasoning. In: Proceedings of the AAAI National Conference, pp. 613–619 (2002)
Bacchus, F.: Exploring the computational tradeoff of more reasoning and less searching. In: Fifth International Symposium on Theory and Applications of Satisfiability Testing, SAT 2002, pp. 7–16 (2002), Available from www.cs.toronto.edu/~fbacchus/2clseq.html
Van Gelder, A., Tsuji, Y.K.: Satisfiability testing with more reasoning and less guessing. In: Johnson, D., Trick, M. (eds.) Cliques, Coloring and Satisfiability. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 559–586. American Mathematical Society, Providence (1996)
Simon, L., Berre, D.L., Hirsch, E.A.: The sat2002 competition. Technical report (2002), www.satlive.org , available on line at www.satlive.org/SATCompetition/
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proc. of the Design Automation Conference, DAC (2001)
Lynce, I., Marques-Silva, J.P.: The puzzling role of simplification in propositional satisfiability. In: EPIA 2001 Workshop on Constraint Satisfaction and Operational Research Techniques for Problem Solving (EPIA-CSOR) (2001), available on line at sat.inesc.pt/~jpms/research/publications.html
Aspvall, B., Plass, M., Tarjan, R.: A linear-time algorithms for testing the truth of certain quantified boolean formulas. Information Processing Letters 8, 121–123 (1979)
Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. In: Proceedings of the International Joint Conference on Artifical Intelligence (IJCAI), pp. 515–522 (2001)
Morrisette, T.: Incremental reasoning in less time and space (2002) (submitted manuscript), available from the author e-mail threesat2000@yahoo.com
Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT 2002 (2002), on line pre-prints available at gauss.ececs.uc.edu/Conferences/SAT2002/sat2002list.html
Tarjan, R.: Depth first search and linear graph algorithms. SIAM Journal on Computing 1, 146–160 (1972)
Crawford, J.M., Auton, L.D.: Experimental results on the crossover point in random 3-sat. Artificial Intelligence 81, 31–57 (1996)
Li, C.M.: Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the International Joint Conference on Artifical Intelligence (IJCAI), pp. 366–371 (1997)
Berre, D.L.: Exploiting the real power of unit propagation lookahead. In: LICS Workshop on Theory and Applications of Satisfiablity Testing (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bacchus, F., Winter, J. (2004). Effective Preprocessing with Hyper-Resolution and Equality Reduction. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-24605-3_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20851-8
Online ISBN: 978-3-540-24605-3
eBook Packages: Springer Book Archive