Heuristic-based backtracking relaxation for propositional satisfiability. (English) Zbl 1109.68099
Summary: In recent years backtrack search algorithms for propositional satisfiability (SAT) have been the subject of dramatic improvements. These improvements allowed SAT solvers to successfully solve instances with thousands or tens of thousands of variables. However, many new challenging problem instances are still too hard for current SAT solvers. As a result, further improvements to SAT technology are expected to have key consequences in solving hard real-world instances. This paper introduces a new idea: choosing the backtrack variable using a heuristic approach with the goal of diversifying the regions of the space that are explored during the search. The proposed heuristics are inspired by the heuristics proposed in recent years for the decision branching step of SAT solvers, namely, VSIDS and its improvements. Completeness conditions are established, which guarantee completeness for the new algorithm, as well as for any other incomplete backtracking algorithm. Experimental results on hundreds of instances derived from real-world problems show that the new technique is able to speed SAT solvers, while aborting fewer instances. These results clearly motivate the integration of heuristic backtracking in SAT solvers.
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
| 68P10 | Searching and sorting |
| 68W05 | Nonnumerical algorithms |
Keywords:
backtrack search algorithmsSoftware:
BerkMinReferences:
| [1] | Baptista, L. and Marques-Silva, J. P.: Using randomization and learning to solve real-world instances of satisfiablility, in R. Dechter (ed.), Proceedings of the International Conference of Principles and Practice of Constraint Programming, Vol. 1894 of Lecture Notes in Computer Science, 2000, pp. 489–494. · Zbl 1044.68736 |
| [2] | Bayardo Jr., R. and Scharg, R.: Using CSP look-back techniques to solve real-world SAT instances, in Proceedings of the National Conference on Artificial Intelligence, 1997, pp.203–208. |
| [3] | Bhalla, A., Lynce, I., de Sousa, J. and Marques-Silva, J.: Heuristic backtracking algorithms for SAT, in Proceedings of the International Workshop of Microprocessor Test and Verification, 2003, pp. 69–74. · Zbl 1205.68370 |
| [4] | Bhalla, A., Lynce, J., de Sousa, J. and Marques-Silva, J. P.: Heuristic-based backtracking for propositional satisfiability, in F. Moura-Pires and S. Abreu (eds.), Proceedings of the Portuguese Conference on Artificial Intelligence, Vol., 1894 of Lecture Notes in Artificial Intelligence, 2003, pp. 116–130. · Zbl 1205.68370 |
| [5] | Davis, M., Logemann, G. and Loveland, D.: A machine program for theorem proving, Commun. Assoc. Comput. Mach. 5 (1962), 394–397. · Zbl 0217.54002 |
| [6] | Davis, M. and Putnam, H.: A computing procedure for quantification theory, J. Assoc. Comput. Mach. 7 (1960), 201–215. · Zbl 0212.34203 |
| [7] | Freuder, E. C., Dechter, R., Ginsberg, M. L., Selman, B. and Tsang, E.: Systematic versus stochastic constraint satisfaction, in Proceedings of the International Joint Conference on Artificial Intelligence, 1995, pp. 2027–2032. |
| [8] | Gaschnig, J.: Performance Measurement and Analysis of Certain Search Algorithms, PhD thesis, Carnegie-Mellon University, Pittsburgh, PA. |
| [9] | Ginsberg, M. L.: Dynamic backtracking, J. Artif. Intell. Res. 1 (1993), 25–46. · Zbl 0900.68179 |
| [10] | Ginsberg, M. L. and McAllester, D.: GSAT and dynamic backtracking, in Proceedings of the International Conference of Principles of Knowledge and Reasoning, 1994, pp. 226–237. |
| [11] | Goldberg, E. and Nonikov, Y.: BerkMin: A Fast and Robust SAT-Solver, in Proceedings of the Design and Test in Europe Conference, 2002, pp. 142–149. |
| [12] | Games, C. P., Selman, B. and Kautz, H.: Boosting combination search through randomization, in Proceedings of the National Conference on Artificial Intelligence, 1998, pp. 431–437. |
| [13] | Hirsch, E. A. and Kojevnikov, A.: Solving Boolean satisfiability using local search guided by unit clause elimination, in Proceedings of the International Conference on Principles and Practice of Constraint Programming, 2001, pp. 605–609. · Zbl 1067.68643 |
| [14] | Jussien, N. and Lhomme, O.: Local search with constraint propagation and conflict-based heuristics, in Proceedings of the National Conference on Artificial Intelligence, 2000, pp.169–174. · Zbl 1015.68056 |
| [15] | Lynce, I., Baptista, L. and Marques-Silva, J. P.: Stochastic systematic search algorithm for satisfiability, in Proceedings of the LICS Workshop on Theory and Applications of Satisfiability Testing, 2001, pp. 1–7. · Zbl 0990.90554 |
| [16] | Lynce, I. and Marques-Silva, J. P.: Complete unrestricted backtracking algorithms for satisfiability, in Proceedings of the International Symposium on Theory and Applications of Satisfiability Testing, 2002, pp. 214–221. |
| [17] | Lynce, I. and Marques-Silva, J. P.: On implementing more efficient SAT data structures, in Proceedings of the International Symposium on Theory and Applications of Satisfiability Testing, 2003, pp. 510–516. |
| [18] | Marques-Silva, J. P. and Sakallah, K. A., GRASP–A search algorithm for propositional satisfiability, IEEE Trans. Comput. 48(5) (1999), 506–521. · doi:10.1109/12.769433 |
| [19] | Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L. and Malik, S.: Engineering an efficient SAT solver, in Design Automation Conference, 2001, pp. 530–535. |
| [20] | Prestwich, S.: A hybrid search architecture applied to hard random 3-SAT and low-autocorrelation binary sequences, in R. Dechter (ed.), Proceedings of the International Conference on Principles and Practice of Constraint Programming, Vol. 1894 of Lecture Notes in Computer Science, 2000, pp. 337–352. · Zbl 1044.68789 |
| [21] | Prosser, P.: Hybrid algorithms for the constraint satisfaction problems, Comput. Intell. 9(3) (1993), 268–299. · doi:10.1111/j.1467-8640.1993.tb00310.x |
| [22] | Richards, E. T. and Richards, B.: Non-systematic search and no-good learning, J. Autom. Reason. 24(4) (2000), 483–533. · Zbl 0961.68517 · doi:10.1023/A:1006362926464 |
| [23] | Selman, B. and Kautz, H.: Domain-independent extensions to GSAT: Solving large structured satisfiability problems, in Proceedings of the International Joint Conference on Artificial Intelligence, 1993, pp. 290–295. |
| [24] | Stallman, R. M. and Sussman, G. J.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis, Artif. Intell. 9 (1977), 135–196. · Zbl 0372.94024 · doi:10.1016/0004-3702(77)90029-7 |
| [25] | Yokoo, M.: Weak-commitment search for solving satisfaction problems, in Proceedings of the National Conference on Artificial Intelligence, 1994, pp. 313–318. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
