×

Speeding-up non-clausal local search for propositional satisfiability with clause learning. (English) Zbl 1138.68554

Kleine Büning, Hans (ed.) et al., Theory and applications of satisfiability testing – SAT 2008. 11th international conference, SAT 2008, Guangzhou, China, May 12–15, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79718-0/pbk). Lecture Notes in Computer Science 4996, 257-270 (2008).
Summary: In this paper we discuss search heuristics for non-clausal stochastic local search procedures for propositional satisfiability. These heuristics are based on a new method for variable selection as well as a novel clause learning technique for dynamic input formula simplification as well as for guiding the search for a model.
For the entire collection see [Zbl 1136.68007].

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T05 Learning and adaptive systems in artificial intelligence

Software:

UBCSAT
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Achlioptas, D.; Jia, H.; Moore, C., Hiding Satisfying Assignments: Two are Better than One, J. of Artificial Intelligence Research, 24, 623-639 (2005) · Zbl 1080.68653
[2] Crawford, J.M., Kearns, M.J., Shapire, R.E.: The Minimal Disagreement Parity Problem as Hard Satisfiability Problem. Computational Intell. Research Lab and AT&T Bell Labs TR (1994)
[3] Fang, H., Ruml, W.: Complete Local Search for Propositional Satisfiability. In: AAAI, pp. 161-166 (2004)
[4] Hoos, H.H.: Local Search - Methods, Models, Applications. TU Dermstadt, FB Informatik, Darmstadt, Germany (1998)
[5] Hoos, H.H.: On the Run-Time Behavior of Stochastic Local Search Algorithms for SAT. In: AAAI/IAAI, pp. 661-666 (1999)
[6] Hoos, H.H.: An Adaptive Noise Mechanism for WalkSAT. In: AAAI, pp. 655-660 (2002)
[7] Hoos, H. H.; Stutzle, T., Local Search Algorithms for SAT: An Empirical Evaluation, Journal of Automated Reasoning, 24, 421-481 (2000) · Zbl 0961.68039 · doi:10.1023/A:1006350622830
[8] Hoos, H. H.; Stutzle, T., Stochastic Local Search: Foundations and Applications (2005), Amsterdam: Elsevier, Amsterdam · Zbl 1126.68032
[9] Kautz, H., Selman, B., McAllester, D.: Exploiting Variable Dependency in Local Search. In: IJCAI (1997)
[10] Lynce, I., Marques-Silva, J.P.: An Overview of Backtrack Search Satisfiability Algorithms. Annals of Mathematics and Artificial Intelligence, 307-326 (2003) · Zbl 1010.68069
[11] McAllester, D., Selman, B., Kautz, H.: Evidence for Invariants in Local Search. In: AAAI, pp. 321-326 (1997)
[12] Navarro, J.A., Voronkov, A.: Generation of Hard Non-Clausal Random Satisfiability Problems. In: AAAI, pp. 436-442 (2005)
[13] Prestwich, S. D.; Marques-Silva, J.; Sakallah, K. A., Variable Dependency in Local Search: Prevention Is Better Than Cure, Theory and Applications of Satisfiability Testing - SAT 2007, 107-120 (2007), Heidelberg: Springer, Heidelberg · Zbl 1214.68369 · doi:10.1007/978-3-540-72788-0_14
[14] Stachniak, Z.: Going Non-clausal. In: SAT, pp. 316-322 (2002)
[15] Tompkins, D. A.; Hoos, H.; H. Hoos, H.; Mitchell, D. G., UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT, Theory and Applications of Satisfiability Testing, 306-320 (2005), Heidelberg: Springer, Heidelberg · Zbl 1122.68620
[16] Velev, M.: Miroslav Velev’s SAT Benchmarks, http://www.miroslav-velev.com/sat_benchmarks.html
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.