Abstract
The satisfiability problem is widely used in research on combinatorial search and for industrial applications such as verification and planning. Real world search problem benchmarks are not plentiful, yet understanding search algorithm behaviour in the real world domain is highly important. This work justifies and investigates a randomised satisfiability problem model with modular properties akin to those observed in real world search problem domains. The proposed problem model provides a reliable benchmark which highlights pitfalls and advantages with various satisfiability search algorithms.
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
S.A. Cook. The complexity of theorem proving procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, 1971.
Roberto J. Bayardo, Jr. and Robert C. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In AAAI-97, 1997.
C. Gomes and B. Selman. Problem structure in presence of perturbations. In AAAI-97, 1997.
D. Achlioptas, C. Gomes, H. Kautz, and B. Selman. Generating satisfiable problem instances. In AAAI-2000, 2000.
David S. Johnson and Michael A. Trick, editors. Cliques, Coloring, and Satisfiability: the Second DIMACS Implementation Challenge, volume 26. American Mathematical Society, 1993.
F. Massacci. Using walk-sat and rel-sat for cryptographic key search. In IJCAI-99, 1999.
I.P Gent, H.H. Hoos, P. Prosser, and T. Walsh. Morphing: Combining structure and randomness. In AAAI-99, 1999.
Irina Rish and Rina Dechter. Resolution versus Search: Two strategies for SAT. Journal of Automated Reasoning, 25(1–2):225–275, 2000.
Tadd Hogg. Refining the phase transition in combinatorial search. Artificial Intelligence, 81, 1996.
S. Grant and B.M. Smith. Where the exceptionally hard problems are. In Proceedings of the CP-95 workshop on Really Hard Problems, 1995.
D.J. Watts and S.H. Strogatz. Collective dynamics of’ small world’ networks. Nature, 393:440–442, 1998.
Toby Walsh. Search in a small world. In IJCAI-99, 1999.
Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In AAAI-97, 1997.
Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, July 1962.
Chu Min Li and Anbulagan. Look-ahead versus look-back for satisfiability problems. In CP-97, 1997.
Jon W. Freeman. Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, University of Pennsylvania, 1995.
Oliver Kullman. Heuristics for sat algorithms: Searching for some foundations. Technical report, Dept. Computer Science, University of Toronto, 1999.
H. Zhang. SATO: An efficient propositional prover. In CADE-14, 1997.
J. M. Crawford and L. D. Auton. Experimental results on the crossover point in random 3-SAT. Artificial Intelligence, 81:31–57, 1996.
E. Amir and S. McIlraith. Partition-based logical reasoning. In KR-2000, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Slater, A. (2002). Modelling More Realistic SAT Problems. In: McKay, B., Slaney, J. (eds) AI 2002: Advances in Artificial Intelligence. AI 2002. Lecture Notes in Computer Science(), vol 2557. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36187-1_52
Download citation
DOI: https://doi.org/10.1007/3-540-36187-1_52
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00197-3
Online ISBN: 978-3-540-36187-9
eBook Packages: Springer Book Archive