SAT中的 width-based algorithm

• Knot Pipatsrisawat, Adnan Darwiche:
  Width-Based Restart Policies for Clause-Learning Satisfiability Solvers. SAT 2009: 341-355
  
  

@inproceedings{DBLP:conf/sat/PipatsrisawatD09,
  author       = {Knot Pipatsrisawat and
                  Adnan Darwiche},
  editor       = {Oliver Kullmann},
  title        = {Width-Based Restart Policies for Clause-Learning Satisfiability Solvers},
  booktitle    = {Theory and Applications of Satisfiability Testing - {SAT} 2009, 12th
                  International Conference, {SAT} 2009, Swansea, UK, June 30 - July
                  3, 2009. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5584},
  pages        = {341--355},
  publisher    = {Springer},
  year         = {2009},
  url          = {https://doi.org/10.1007/978-3-642-02777-2\_32},
  doi          = {10.1007/978-3-642-02777-2\_32},
  timestamp    = {Tue, 14 May 2019 10:00:41 +0200},
  biburl       = {https://dblp.org/rec/conf/sat/PipatsrisawatD09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

1. width-based algorithm

Galil [12] proposed a SAT algorithm which runs in time exponential in the width of the CNF formula. This algorithm, which was later reformulated in [13] and [9], works by deriving all resolvents of size ≤ k, for increasing k. Since there are only O(nk) clauses of size ≤ k,wheren is the total number of variables, this algorithm works well on formulas with bounded or small widths. Moreover, it was shown in [9] that this algorithm runs in time that is at most quasi-polynomial in the size of the smallest tree-like refutation proof (i.e., optimal DPLL). Nevertheless, one drawback which limits the practicality of this approach is the amount of memory it requires. Even though the space complexity of the algorithm is only exponential in the width of the proof, in practice, this could be a serious limiting factor–especially when compared to the clause-learning descendants of DPLL, which perform resolution in a more directed way and keep only a fraction of the resolvents in the knowledge base. The restart policies that we propose in this work can be thought of as a way to efficiently combine the benefits of both approaches. In other words, our approach canbeviewedasawayofusingthelowmemory requirement of modern clause learning SAT algorithms to loosely imitate the above width-based algorithm.

References

1. Gomes, C.P., Selman, B., Crato, N.: Heavy-tailed distributions in combinatorial search. In: Principles and Practice of Constraint Programming, pp. 121–135 (1997)

2. Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Proc. of DAC 2001, pp. 530–535 (2001)

3. E´ en, N., S¨orensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

4. Goldberg, E., Novikov, Y.: Berkmin: A fast and robust sat-solver. In: DATE 2002, pp. 142–149 (2002)

5. Huang, J.: The effect of restarts on the efficiency of clause learning. In: Proc. of IJCAI 2007, pp. 2318–2323 (2007)

6. Biere, A.: Adaptive restart strategies for conflict driven sat solvers. In: Kleine B¨ uning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 28–33. Springer, Heidelberg (2008)

7. Ryvchin, V., Strichman, O.: Local restarts. In: Kleine B¨ uning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 271–276. Springer, Heidelberg (2008)

8. Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. JAIR 22, 319–351 (2004)

9. Ben-Sasson, E., Wigderson, A.: Short proofs are narrow—resolution made simple. J. ACM 48(2), 149–169 (2001)

10. Ryan, L.: Efficient Algorithms for Clause-Learning SAT Solvers. Master’s thesis, Simon Fraser University (2004)

11. Zhang, L., Malik, S.: Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE 2003, pp. 880–885 (2003)

12. Galil, Z.: On resolution with clauses of bounded size. SIAM Journal on Comput ing 6(3), 444–459 (1977)

13. Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: Annual IEEE Symposium on Foundations of Computer Science, p. 274 (1996)

14. Mahajan, Y.S., Fu, Z., Malik, S.: Zchaff2004: An efficient sat solver. In: Proc. of SAT 2005, pp. 360–375 (2005)

15. Nadel, A., Gordon, M., Patti, A., Hanna, Z.: Eureka-2006 sat solver Solver descrip tion for SAT-Race 2006 (2006)

16. Biere, A.: Picosat essentials. JSAT, 75–97 (2008)

17. Huang, J.: A case for simple SAT solvers. In: Bessi`ere, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 839–846. Springer, Heidelberg (2007)

18. Pipatsrisawat, K., Darwiche, A.: Rsat 2.0: Sat solver description. Technical Re port D–153, Automated Reasoning Group, Computer Science Department, UCLA (2007)

19. S¨orensson, N., E´ en, N.: Minisat 2.1 and minisat++ 1.0–sat race 2008 editions (2008

20. Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near optimal separation of tree like and general resolution. Combinatorica 24(4), 585–603 (2004) 21. Babi´ c, D., Hu, A.J.: Structural Abstraction of Software Verification Conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 371–383. Springer, Heidelberg (2007)

22. Babi´ c, D., Hu, A.J.: Calysto: Scalable and Precise Extended Static Checking. In: Proc. of ICSE 2008, pp. 211–220 (2008)

23. Hertel, A., Urquhart, A.: Comments on eccc report tr06-133: The resolution width problem is exptime-complete. Technical Report TR09-003, ECCC (2009)

24. Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for sat isfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007)

25. Dechter, R.: Enhancement schemes for constraint processing: backjumping, learn ing, and cutset decomposition. Artif. Intell. 41(3), 273–312 (1990)

26. Bayardo, R.J., Miranker, D.P.: A complexity analysis of space-bounded learning algorithms for the constraint satisfaction problem. In: AAAI 1996, pp. 298–304 (1996)

27. Bayardo, R.J.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proc. of AAAI 1997, Providence, Rhode Island, pp. 203–208 (1997)

28. Nadel, A.: Backtrack search algorithms for propositional logic satisfiability: Review and innovations. Master’s thesis, The Hebrew University (2002

2.   Existing and Width-Based Restart Policies

Width-Based Restart Policies for Clause-Learning Satisfiability Solvers. SAT 2009: 341-355