Abstract
As SAT becomes more popular due to its ability to handle large real-world problems, progress in efficiency appears to have slowed down over the past few years. On the other hand, we now have access to many sophisticated implementations of SAT solvers, sometimes boasting large amounts of code. Although low-level optimizations can help, we argue that the SAT algorithm itself offers opportunities for more significant improvements. Specifically, we start with a no-frills solver implemented in less than 550 lines of code, and show that by focusing on the central aspects of the solver, higher performance can be achieved over some best existing solvers on a large set of benchmarks. This provides motivation for further research into these more important aspects of SAT algorithms, which we hope will lead to future significant advances in SAT.
National ICT Australia is funded by the Australian Government’s Backing Australia’s Ability initiative, in part through the Australian Research Council.
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
Beame, P., Kautz, H., Sabharwal, A.: Understanding the power of clause learning. In: IJCAI, pp. 1194–1201 (2003)
Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. JAIR 22, 319–351 (2004)
Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)
Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: DATE, pp. 142–149 (2002)
Huang, J.: The effect of restarts on the efficiency of clause learning. In: IJCAI, pp. 2318–2323 (2007)
Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: IJCAI, pp. 366–371 (1997)
Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Information Processing Letters 47(4), 173–180 (1993)
Lynce, I., Silva, J.P.M.: Complete unrestricted backtracking algorithms for satisfiability. In: SAT (2002)
Marques-Silva, J., Sakallah, K.: GRASP—A new search algorithm for satisfiability. In: ICCAD, pp. 220–227 (1996)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC, pp. 530–535 (2001)
Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: SAT, pp. 294–299 (2007)
Pipatsrisawat, T., Darwiche, A.: SAT solver description: Rsat. In: SAT-Race (2006)
Sinz, C.: SAT Race (2006), http://fmv.jku.at/sat-race-2006
Zarpas, E.: Benchmarking SAT solvers for bounded model checking. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 340–354. Springer, Heidelberg (2005)
Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: ICCAD, pp. 279–285 (2001)
Zhang., L.: On subsumption removal and on-the-fly CNF simplification. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 482–489. Springer, Heidelberg (2005)
Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE, pp. 10880–10885 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huang, J. (2007). A Case for Simple SAT Solvers. In: Bessière, C. (eds) Principles and Practice of Constraint Programming – CP 2007. CP 2007. Lecture Notes in Computer Science, vol 4741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74970-7_62
Download citation
DOI: https://doi.org/10.1007/978-3-540-74970-7_62
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74969-1
Online ISBN: 978-3-540-74970-7
eBook Packages: Computer ScienceComputer Science (R0)