No Access

SYSTEMATIC VERSUS LOCAL SEARCH AND GA TECHNIQUES FOR INCREMENTAL SAT

MALEK MOUHOUB

Department of Computer Science, University of Regina, 3737 Wascana Parkway, Regina Saskatchewan, Canada S4S 0A2, Canada

https://doi.org/10.1142/S1469026808002193Cited by:3 (Source: Crossref)

Abstract

Propositional satisfiability (SAT) problem is fundamental to the theory of NP-completeness. Indeed, using the concept of "polynomial-time reducibility" all NP-complete problems can be polynomially reduced to SAT. Thus, any new technique for satisfiability problems will lead to general approaches for thousands of hard combinatorial problems. In this paper, we introduce the incremental propositional satisfiability problem that consists of maintaining the satisfiability of a propositional formula anytime a conjunction of new clauses is added. More precisely, the goal here is to check whether a solution to a SAT problem continues to be a solution anytime a new set of clauses is added and if not, whether the solution can be modified efficiently to satisfy the old formula and the new clauses. We will study the applicability of systematic and approximation methods for solving incremental SAT problems. The systematic method is based on the branch and bound technique, whereas the approximation methods rely on stochastic local search (SLS) and genetic algorithms (GAs). A comprehensive empirical study, conducted on a wide range of randomly generated consistent SAT instances, demonstrates the efficiency in time of the approximation methods over the branch and bound algorithm. However, these approximation methods do not guarantee the completeness of the solution returned. We show that a method we propose that uses nonsystematic search in a limited form together with branch and bound has the best compromise, in practice, between time and the success ratio (percentage of instances completely solved).

Keywords:

Remember to check out the Most Cited Articles!
Check out these titles in artificial intelligence!

References

S. A. Cook, The complexity of theorem proving procedures, 3rd Ann. ACM Symp. Theory of Computing (1971) pp. 151–158. Google Scholar
M. Davis and H. Putnam, J. Assoc. Comput. Mach. 7, 201 (1960). Crossref, Google Scholar
D. Loveland , Automated Theorem-Provingx: A LogicalBasis ( North-Holland , 1978 ) . Google Scholar
J. P. Marques-Silva and K. A. Sakallah, IEEE Trans. Comput. 48, 506 (1999), DOI: 10.1109/12.769433. Crossref, Google Scholar
L. Zhang et al. , Efficient conflict driven learning in a Boolean satisfiability solver , Proc. Int. Conf. Computer Aided Design (ICCAD) ( 2001 ) . Google Scholar
W. Moskewiscet al., Chaff: Engineering an efficient SAT solver, Proc. 38th Design Automation Conference (2001) pp. 530–535. Google Scholar
S. YogeshMahajan , Z. Fu and S. Malik , Lecture Notes in Computer Science , SAT 2004 3542 , eds. H. H. Hoos and D. G. Mitchell ( Springer-Verlag , Berlin, Heidelberg , 2004 ) . Google Scholar
B. Selman and H. A. Kautz, An empirical study of greedy local search for satisfiability testing, AAAI'93 (1993) pp. 46–51. Google Scholar
B. Selman, H. A. Kautz and B. Cohen, AAAI'94 (MIT Press, 1994) pp. 337–343. Google Scholar
H. H. Hoos and T. Stutzle , Stochastic Local Search Foundations and Applications ( Morgan Kaufmann , Elsevier , 2004 ) . Google Scholar
D. A. D. Tompkins and H. H. Hoos, UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT, SAT 2004, Theory and Applications of Satisfiability Testing: Revised Selected Papers of the Seventh Int. Conf.2470, Lecture Notes in Computer Science, eds. H. H. Hoos and D. G. Mitchell (Springer Verlag, Berlin, Germany, 2005) pp. 306–320. Google Scholar
F. Hutter, A. D. Tompkins and H. H. Hoos, Scaling and probabilistic smoothing: Efficient dynamic local search for sat, Eighth Int. Conf. Principles and Practice of Constraint Programming (CP-02)2470, Lecture Notes in Computer Science (Springer Verlag, Berlin, Germany, 2002) pp. 233–248. Google Scholar
Z. Michalewicz , Genetic Algorithms + Data Structures = Evaluation Program ( Springer-Verlag , 1992 ) . Crossref, Google Scholar
K. A. De Jong and W. M. Spears, Using genetic algorithms to solve np-complete problems, Third Int. Conf. Genetic Algorithms, ed. J. D. Schaffer (Morgan Kaufmann, San Mateo, CA, 1989) pp. 124–132. Google Scholar
A. E. Eiben and J. K. van der Hauw, Solving 3-sat with adaptive genetic algorithms, 4th IEEE Conf. Evolutionary Computation (1997) pp. 81–86. Google Scholar
B. Craenen and A. E. Eiben, IEEE Trans. Evol. Comput. 7(5), 424 (2003), DOI: 10.1109/TEVC.2003.816584. Crossref, Google Scholar
G. Folino, C. Pizzuti and C. Spezzano, IEEE Trans. Evol. Comput. 5(4), 323 (2001), DOI: 10.1109/4235.942527. Crossref, Google Scholar
F. Lardeux, F. Saubion and J. K. Hao, Evol. Comput. 14(2), 223 (2006), DOI: 10.1162/evco.2006.14.2.223. Crossref, Google Scholar
J. K. Hao, F. Lardeux and F. Saubion, Applications of Evolutionary Computing, Lecture Notes in Computer Science 2611 (Springer Verlag, 2003) pp. 258–267. Crossref, Google Scholar
J. Gottlieb, E. Marchiori and C. Rossi, Evol. Comput. 10(1), 35 (2002), DOI: 10.1162/106365602317301763. Crossref, Google Scholar
H. H. Hoos and K. O'Neil, Stochastic local search methods for dynamic SAT — an initial investigation, AAAI-2000 Workshop on Leveraging Probability and Uncertainty in Computation (2000) pp. 22–26. Google Scholar
J. Gutierrez and A. D. Mali, Int. Conf. Artif. Intel. 986 (2002). Google Scholar
J. N. Hooker, J. Logic Program. 15, 177 (1993), DOI: 10.1016/0743-1066(93)90018-C. Crossref, Google Scholar
H. Bennaceur, I. Gouachi and Plateau, INFORMS J. Comput. 10, 301 (1998), DOI: 10.1287/ijoc.10.3.301. Crossref, Google Scholar
J. Wittemore, J. Kim and K. A. Sakallah, Satire: A new incremental satisfiability engine, DAC 2001 (2001) pp. 542–545. Google Scholar
R. Dechter , Constraint Processing ( Morgan Kaufmann , 2003 ) . Google Scholar
T. Walsh, Sixth Int. Conf. Principles and Practice of Constraint Programming, Lecture Notes in Computer Science 2470, ed. R. Dechter (Springer Verlag, Berlin, Germany, 2000) pp. 441–456. Crossref, Google Scholar
F. Bacchus, Lecture Notes in Computer Science, SAT 2006 4121, eds. A. Biere and C. P. Gomes (Springer-Verlag, Berlin Heidelberg, 2006) pp. 10–10. Google Scholar
S. Mittal and B. Falkenhainer, Dynamic constraint satisfaction problems, Proc. 8th National Conf. Artificial Intelligence (AAAI Press, Boston, MA, August 1990) pp. 25–32. Google Scholar
D. Sabin and E. C. Freuder, Configuration as composite constraint satisfaction, Proc. 1st Artificial Intelligence and Manufacturing Research Planning Workshop, ed. G. F. Luger (AAAI Press, 1996) pp. 153–161. Google Scholar
D. Sabin, E. C. Freuder and R. J. Wallace, Greater efficiency for conditional constraint satisfaction, Proc. Ninth Int. Conf. Principles and Practice of Constraint Programming — CP 20032833 (2003) pp. 649–663. Google Scholar
E. Gelle and B. Faltings, Constraints 8, 107 (2003), DOI: 10.1023/A:1022394531132. Crossref, Google Scholar
R. Dechter and A. Dechter, Belief maintenance in dynamic constraint networks, 7th National Conf. Artificial Intelligence (1988) pp. 37–42. Google Scholar
A. K. Jónsson and J. Frank, A framework for dynamic constraint reasoning using procedural constraints, ECAI 2000 (2000) pp. 93–97. Google Scholar
A. K. Jónsson and J. Frank, Constraints 8(4), 339 (2003). Google Scholar
I. Tsamardinos, T. Vidal and M. E. Pollack, Constraints 8(4), 365 (2003), DOI: 10.1023/A:1025894003623. Crossref, Google Scholar
R. G. Jeroslow, C. E. Blair and J. K. Lowe, Comput. Oper. Res. 13(5), 633 (1986). Google Scholar
R. J. Wallace and E. C. Freuder , Second DIMACS Implementation Challenge , eds. D. S. Johnson and M. A. Trick ( American Mathematical Society , 1995 ) . Google Scholar
R. E. Jeroslow, Ann. Math. Artif. Intell. 1, 167 (1990), DOI: 10.1007/BF01531077. Crossref, Google Scholar
SAT Competition (Morgan Kaufmann, 2002) . Google Scholar
SAT Competition (Morgan Kaufmann, 2004) . Google Scholar
E. Goldberg and Y. Novikov , Berkmin: A fast and robust sat solver , DATE ( 2002 ) . Google Scholar
D. Shuurmans, F. Southey and R.C. Holte, The exponentiated subgradient algorithm for heuristic Boolean programming, IJCAI-01 (Morgan Kaufmann, 2001) pp. 334–341. Google Scholar
T. Hogg, Artif. Intel. 81, 127 (1996), DOI: 10.1016/0004-3702(95)00050-X. Crossref, Google Scholar
I. Gentet al., Combining structure and randomness, AAAI-99 (1999) pp. 654–660. Google Scholar
J. Singer, I. Gent and A. Smaill, J. Artif. Intell. Res. 235 (2000). Crossref, Google Scholar
P. Cheeseman, B. Kanefsky and W. M. Taylor, Where the really hard problems are, IJCAI-91 (1991) pp. 331–337. Google Scholar
H. H. Hoos and T. Stutzle, Characterizing the run-time behavior of stochastic local search, in Technical Report AIDA-98-01 (1998) . Google Scholar
H. H. Hoos, Heavy-tailed behaviour in randomised systematic search algorithms for sat?, in Technical Report TR-99-16, Department of Computer Science, University of British Columbia (1999) . Google Scholar