Abstract
Evaluation of local search heuristics for constraint satisfaction and satisfiability problems is based on the generation of instances that are guaranteed to be satisfiable. One popular method for creating hard satisfiable instances is the use of complete search procedures to filter out unsatisfiable instances. This approach however has two problems; first, the size of instances produced is limited considerably and second, the generated instances are far from being random.
Although one can generate satisfiable instances by reducing certain computational problems to SAT, it is not known how a similar generator can be developed directly for k-SAT. In this work we provide a generator for an optimization version of k-SAT that has certain useful properties. First, we show how to produce weighted instances of MAX k-SAT where one seeks to maximize the weight of satisfied clauses. Second, we provide a nice characterization of the optimal solution; in our model not only we know how the optimal solution looks like but we also prove it is unique. Finally, we show that our generator has tunable complexity; by appropriately choosing parameters one can control the hardness of the generated instances leading to an easy-hard-easy pattern in the search complexity for good assignments and a new type of phase transition.
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
Achlioptas, D., Gomes, C., Kautz, H., Selman, B.: Generating satisfiable problem instances. In: Proc. AAAI 2000 (2000)
Asahiro, Y., Iwama, K., Miyano, E.: Random generation of test instances with controlled attributes. In: Second DIMACS Challenge on Cliques, Coloring and Satisfiability (October 1993)
Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters 8(3), 121–123 (1979)
Crawford, J., Kearns, M.: Instances for learning the parity function. In: [7]
Gent, I., Walsh, T.: The SAT Phase Transition. In: Proc. ECAI 1994, pp. 105-109 (1999)
Gent, I., Walsh, T.: The TSP Phase Transition. Artif. Intel. 88, 349–358 (1996)
Hoos, H.: SATLIB. A collection of SAT tools and data (1999), http://www.informatic.tu-darmstadt.de/AI/SATLIB
Kirkpatrick, S., Selman, B.: Critical behavior in the satisfiability of random Boolean expressions. Science 264, 1297–1301 (1994)
Massacci, F.: Using WalkSAt and RelSat for cryptographic key search. In: Proc. IJCAI 1999, pp. 290–295 (1999)
Mitchell, D., Levesque, H.J.: Some pitfalls for experimenters with random SAT. Artificial Intelligence 81(1-2), 111–125 (1996)
Mitchell, D., Selman, B., Levesque, H.J.: Generating hard satisfiability problems. Artificial Intelligence 81(1-2) (1996)
Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity from characteristic phase transitions. Nature 400(8) (1999)
Selman, B., Kautz, H.A., Cohen, B.: Local search strategies for satisfiability testing. In: Second DIMACS Challenge on Cliques, Coloring and Satisfiability (1993)
Slaney, J., Walsh, T.: Backbones in Optimization and Approximation. In: Proc. IJCAI 2001 (2001)
Zhang, W.: Phase transitions and backbones of 3-SAT and MAX 3-SAT. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, p. 153. Springer, Heidelberg (2001)
Zhang, W., Korf, R.E.: A study of complexity transitions on the asymmetric Travelling Salesman Problem. Artificial Intelligence 81, 223–239 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dimitriou, T. (2003). A Wealth of SAT Distributions with Planted Assignments. In: Rossi, F. (eds) Principles and Practice of Constraint Programming – CP 2003. CP 2003. Lecture Notes in Computer Science, vol 2833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45193-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-45193-8_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20202-8
Online ISBN: 978-3-540-45193-8
eBook Packages: Springer Book Archive