Abstract
We study a framework called BC SLS for a novel type of stochastic local search (SLS) for propositional satisfiability (SAT). Aimed specifically at solving real-world SAT instances, the approach works directly on a non-clausal structural representation for SAT. This allows for don’t care detection and justification guided search heuristics in SLS by applying the circuit-level SAT technique of justification frontiers. In this paper we extend the BC SLS approach first by developing generalizations of BC SLS which are probabilistically approximately complete (PAC). Second, we develop and study adaptive noise mechanisms for BC SLS, including mechanisms based on dynamically adapting the waiting period for noise increases. Experiments show that a preliminary implementation of the novel adaptive, PAC generalization of the method outperforms a well-known CNF level SLS method with adaptive noise (AdaptNovelty+) on a collection of structured real-world SAT instances.
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.
References
Selman, B., Levesque, H., Mitchell, D.: A new method for solving hard satisfiability problems. In: AAAI, pp. 440–446 (1992)
Selman, B., Kautz, H., Cohen, B.: Noise strategies for improving local search. In: AAAI, pp. 337–343 (1994)
McAllester, D., Selman, B., Kautz, H.: Evidence for invariants in local search. In: AAAI, pp. 321–326 (1997)
Hoos, H.: An adaptive noise mechanism for WalkSAT. In: AAAI, pp. 655–660 (2002)
Braunstein, A., Mézard, M., Zecchina, R.: Survey propagation: An algorithm for satisfiability. Random Structures and Algorithms 27(2), 201–226 (2005)
Kautz, H., Selman, B.: The state of SAT. Discr. Appl. Math. 155(12), 1514–1524 (2007)
Järvisalo, M., Junttila, T., Niemelä, I.: Justification-based non-clausal local search for SAT. In: ECAI. Frontiers in AI and Applications, vol. 178, pp. 535–539. IOS Press, Amsterdam (2008)
Junttila, T., Niemelä, I.: Towards an efficient tableau method for Boolean circuit satisfiability checking. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. Lecture Notes in Computer Science (LNAI), vol. 1861, pp. 553–567. Springer, Heidelberg (2000)
Kuehlmann, A., Ganai, M., Paruthi, V.: Circuit-based Boolean reasoning. In: DAC, pp. 232–237. ACM, New York (2001)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE T-CAD 21(12), 1377–1394 (2002)
Thiffault, C., Bacchus, F., Walsh, T.: Solving non-clausal formulas with DPLL search. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 663–678. Springer, Heidelberg (2004)
Safarpour, S., Veneris, A., Drechsler, R., Lee, J.: Managing don’t cares in Boolean satisfiability. In: DATE 2004. IEEE, Los Alamitos (2004)
Sebastiani, R.: Applying GSAT to non-clausal formulas. J. Artif. Intell. Res. 1, 309–314 (1994)
Kautz, H., McAllester, D., Selman, B.: Exploiting variable dependency in local search. In: IJCAI poster session (1997), http://www.cs.rochester.edu/u/kautz/papers/dagsat.ps
Pham, D., Thornton, J., Sattar, A.: Building structure into local search for SAT. In: IJCAI, pp. 2359–2364 (2007)
Hoos, H.H.: On the run-time behaviour of stochastic local search algorithms for SAT. In: AAAI, pp. 661–666 (1999)
Patterson, D.J., Kautz, H.: Auto-Walksat: A self-tuning implementation of Walksat. In: SAT, 4th Workshop on Theory and Application of Satisfiability Testing (2001)
Selman, B., Kautz, H.: An empirical study of greedy local search for satisfiability testing. In: AAAI, pp. 46–51 (1993)
Hirsch, E., Kojevnikov, A.: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. Ann. Math. Artif. Intell. 43(1), 91–111 (2005)
Junttila, T.: The BC package and a file format for constrained Boolean circuits, http://www.tcs.hut.fi/~tjunttil/bcsat/
Heljanko, K.: Bounded reachability checking with process semantics. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 218–232. Springer, Heidelberg (2001)
Li, C., Wei, W., Zhang, H.: Combining adaptive noise and look-ahead in local search for SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 121–133. Springer, Heidelberg (2007)
Tompkins, D., Hoos, H.: UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306–320. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Järvisalo, M., Junttila, T., Niemelä, I. (2008). Justification-Based Local Search with Adaptive Noise Strategies. In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)