Abstract
In this paper we introduce UBCSAT, a new implementation and experimentation environment for Stochastic Local Search (SLS) algorithms for SAT and MAX-SAT. Based on a novel triggered procedure architecture, UBCSAT provides implementations of numerous well-known and widely used SLS algorithms for SAT and MAX-SAT, including GSAT, WalkSAT, and SAPS; these implementations generally match or exceed the efficiency of the respective original reference implementations. Through numerous reporting and statistical features, including the measurement of run-time distributions, UBCSAT facilitates the advanced empirical analysis of these algorithms. New algorithm variants, SLS algorithms, and reporting features can be added to UBCSAT in a straightforward and efficient way. UBCSAT is implemented in C and runs on numerous platforms and operating systems; it is publicly and freely available at www.satlib.org/ ubcsat.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Audemard, G., Le Berre, D., Roussel, O., Lynce, I., Marques-Silva, J.: OpenSAT: an open source SAT software project. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–509. Springer, Heidelberg (2004)
Fukunaga, A.: Efficient implementations of SAT local search. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 287–292. Springer, Heidelberg (2005)
Gent, I.P., Walsh, T.: Towards an understanding of hill–climbing procedures for SAT. In: Proc. of the Eleventh Nat’l Conf. on Artificial Intelligence (AAAI 1993), pp. 28–33 (1993)
Gent, I.P., Walsh, T.: Unsatisfied variables in local search. In: Hybrid Problems, Hybrid Solutions, pp. 73–85 (1995)
Hansen, P., Jaumard, B.: Algorithms for the maximum satisfiability problem. Computing 44, 279–303 (1990)
Hoos, H.H.: On the run-time behaviour of stochastic local search algorithms for SAT. In: Proc. of the Sixteenth Nat’l Conf. on Artificial Intelligence (AAAI 1999), pp. 661–666 (1999)
Hoos, H.H.: An adaptive noise mechanism for WalkSAT. In: Proc. of the 18th Nat’l Conf. in Artificial Intelligence (AAAI 2002), pp. 655–660 (2002)
Hoos, H.H., Stützle, T.: Stochastic Local Search: Foundations and Applications. Morgan Kaufmann, San Francisco (2005)
Hutter, F., Tompkins, D.A.D., Hoos, H.H.: Scaling and probabilistic smoothing: Efficient dynamic local search for SAT. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 233–248. Springer, Heidelberg (2002)
Matsumoto, M., Nishimura, T.: Mersenne twister: a 623-dimensionally equidistributed uniform pseudo-random number generator. ACM Trans. on Modeling & Computer Simulation 8(1), 3–30 (1998)
Mazure, B., Saïs, L., Grégoire, É.: Tabu search for SAT. In: Proc. of the Fourteenth Nat’l Conf. on Artificial Intelligence (AAAI 1997), pp. 281–285 (1997)
McAllester, D., Selman, B., Kautz, H.: Evidence for invariants in local search. In: Proc. of the Fourteenth Nat’l Conf. on Artificial Intelligence (AAAI 1997), pp. 321–326 (1997)
Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proc. of the 12th Nat’l Conf. on Artificial Intelligence (AAAI 1994), pp. 337–343 (1994)
Selman, B., Levesque, H., Mitchell, D.: A new method for solving hard satisfiability problems. In: Proc. of the Tenth Nat’l Conf. on Artificial Intelligence (AAAI 1992), pp. 459–465 (1992)
Smyth, K., Hoos, H.H., Stützle, T.: Iterated robust tabu search for MAX-SAT. In: Proc. of the 16th Conf. of the Canadian Society for Computational Studies of Intelligence, pp. 129–144 (2003)
Tompkins, D.A.D., Hoos, H.H.: Warped landscapes and random acts of SAT solving. In: Proc. of the Eighth Int’l Symposium on Artificial Intelligence and Mathematics (ISAIM 2004) (2004)
Van Hentenryck, P., Michel, L.: Control abstractions for local search. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 65–80. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tompkins, D.A.D., Hoos, H.H. (2005). UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT. In: Hoos, H.H., Mitchell, D.G. (eds) Theory and Applications of Satisfiability Testing. SAT 2004. Lecture Notes in Computer Science, vol 3542. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11527695_24
Download citation
DOI: https://doi.org/10.1007/11527695_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27829-0
Online ISBN: 978-3-540-31580-3
eBook Packages: Computer ScienceComputer Science (R0)