Abstract
Restarts are a pivotal aspect of conflict-driven clause-learning (CDCL) SAT solvers, yet it remains unclear when they are favorable in practice, and whether they offer additional power in theory. In this paper, we consider the power of restarts through the lens of backdoors. Extending the notion of learning-sensitive (LS) backdoors, we define a new parameter called learning-sensitive with restarts (LSR) backdoors. Broadly speaking, we show that LSR backdoors are a powerful parametric lens through which to understand the impact of restarts on SAT solver performance, and specifically on the kinds of proofs constructed by SAT solvers. First, we prove that when backjumping is disallowed, LSR backdoors can be exponentially smaller than LS backdoors. Second, we demonstrate that the size of LSR backdoors are dependent on the learning scheme used during search. Finally, we present new algorithms to compute upper-bounds on LSR backdoors that intrinsically rely upon restarts, and can be computed with a single run of a CDCL SAT solver. We empirically demonstrate that this can often produce much smaller backdoors than previous approaches to computing LS backdoors. We conclude with empirical results on industrial benchmarks which demonstrate that rapid restart policies tend to produce more “local” proofs than other heuristics, in terms of the number of unique variables found in learned clauses of the proof.
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
References
Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. 40, 353–373 (2011)
Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22, 319–351 (2004)
Beame, P., Kautz, H., Sabharwal, A.: Understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22, 319–351 (2014)
Beame, P., Sabharwal, A.: Non-restarting sat solvers with simple preprocessing can efficiently simulate resolution. In: AAAI Conference on Artificial Intelligence, pp. 2608–2615. AAAI Press (2014)
Biere, A., Fröhlich, A.: Evaluating CDCL restart schemes. In: Pragmatics of SAT Workshop (2015)
Biere, A., Heule, M., van Maaren, H.: Handbook of satisfiability, vol. 185. IOS Press (2009)
Buss, S.R., Hoffmann, J., Johannsen, J.: Resolution trees with lemmas: resolution refinements that characterize DLL algorithms with clause learning. arXiv preprint arXiv:0811.1075 (2008)
Dilkina, B., Gomes, C.P., Malitsky, Y., Sabharwal, A., Sellmann, M.: Backdoors to combinatorial optimization: feasibility and optimality. In: van Hoeve, W.-J., Hooker, J.N. (eds.) CPAIOR 2009. LNCS, vol. 5547, pp. 56–70. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-01929-6_6
Dilkina, B., Gomes, C.P., Sabharwal, A.: Backdoors in the context of learning. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 73–79. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_9
Dilkina, B., Gomes, C.P., Sabharwal, A.: Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search. Ann. Math. Artif. Intell. 70(4), 399–431 (2014). https://doi.org/10.1007/s10472-014-9407-9
Ganian, R., Ramanujan, M.S., Szeider, S.: Backdoor treewidth for SAT. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 20–37. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_2
Godefroid, P., Levin, M.Y., Molnar, D.A., et al.: Automated whitebox fuzz testing. In: Network and Distributed System Security Symposium, pp. 151–166. Internet Society (2008)
Haim, S., Heule, M.: Towards ultra rapid restarts. arXiv preprint arXiv:1402.4413 (2014)
Hertel, P., Bacchus, F., Pitassi, T., Van Gelder, A.: Clause learning can effectively p-simulate general propositional resolution. In: AAAI Conference on Artificial Intelligence, pp. 283–290. AAAI Press (2008)
Huang, J.: The effect of restarts on the efficiency of clause learning. In: International Joint Conference on Artificial Intelligence, pp. 2318–2323. AAAI Press (2007)
Kilby, P., Slaney, J., Thiébaux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: AAAI Conference on Artificial Intelligence, pp. 1368–1373. AAAI Press (2005)
Li, Z., van Beek, P.: Finding small backdoors in SAT instances. In: Butz, C., Lingras, P. (eds.) AI 2011. LNCS (LNAI), vol. 6657, pp. 269–280. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21043-3_33
Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123–140. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_9
Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of las vegas algorithms. Inf. Process. Lett. 47(4), 173–180 (1993)
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: Design Automation Conference, pp. 530–535. ACM (2001)
Nadel, A., Ryvchin, V.: Chronological backtracking. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 111–121. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_7
Pipatsrisawat, K., Darwiche, A.: A new clause learning scheme for efficient unsatisfiability proofs. In: AAAI Conference on Artificial Intelligence, pp. 1481–1484 (2008)
Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers with restarts. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 654–668. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04244-7_51
Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175, 512–525 (2011). https://doi.org/10.1016/j.artint.2010.002
Ruan, Y., Kautz, H., Horvitz, E.: The backdoor key: a path to understanding problem hardness. In: AAAI Conference on Artificial Intelligence, pp. 124–130. AAAI Press (2004)
Samer, M., Szeider, S.: Backdoor trees. In: AAAI Conference on Artificial Intelligence, pp. 363–368. AAAI Press (2008)
Gelder, A.: Pool resolution and its relation to regular resolution and DPLL with clause learning. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 580–594. Springer, Heidelberg (2005). https://doi.org/10.1007/11591191_40
Williams, R., Gomes, C., Selman, B.: On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 222–230. Springer (2003). https://doi.org/10.1.1.128.5725
Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, pp. 279–285. IEEE Press (2001)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Zulkoski, E. et al. (2018). Learning-Sensitive Backdoors with Restarts. In: Hooker, J. (eds) Principles and Practice of Constraint Programming. CP 2018. Lecture Notes in Computer Science(), vol 11008. Springer, Cham. https://doi.org/10.1007/978-3-319-98334-9_30
Download citation
DOI: https://doi.org/10.1007/978-3-319-98334-9_30
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98333-2
Online ISBN: 978-3-319-98334-9
eBook Packages: Computer ScienceComputer Science (R0)