Beyond sAT

The success with SAT solvers has emboldened researchers to consider problems related to, but more difficult than SAT. The most promising of these is Satisfiability Modulo Theories (SMT) that has received significant attention in recent years.

In SAT, the variables are assumed to be constrained only by the clauses in the formula. SMT extends SAT by considering the case when the variables may be connected by one or more underlying theories. For example, consider the formula (x1 ∧ Øx2 ∧ x3). This formula is clearly satisfiable with (x1 = 1, x2=0, x3= 1). However, if x1, x2 and x3 represent the following relationships among the real variables y1 and y2:

x1: y1 <0 x2: y1 + y2 < 1 x3: y2 < 0

Then, in fact, there is no assignment to y1 and y2 for which (x1 = 1, x2=0, x3= 1), i.e., y1 and y2 cannot be both negative and their sum at least one. Thus, the original formula is unsatisfiable given this underlying relationship. In this example, the specific theory used to determine the validity of a satisfying assignment is Linear Real Arithmetic. Emerging SMT solvers can incorporate reasoning for a range of theories such as Linear Integer Arithmetic, Difference Logic, Arrays, Lists, Uninterpreted Functions and many others, including their combinations. 1 The theoretical difficulty depends on the specific theories considered. SMT is seeing rapid progress and initial commercial use in software verification.

conclusion

The success with SAT has led to its widespread commercial use in certain domains such as design and verification of hardware and software systems. There is even a sense in parts of the computer science community that this problem has been successfully tamed in practice. This is probably too optimistic a view. There are still enough instances that are difficult for current solvers, and it is unclear if they will be able to handle the change in scale/na-ture of instances from yet unseen domains. However, there is definitely a sense of confidence that we will be able to continue to strengthen our solvers.

Given its theoretical hardness, the

practical success of SAT has come as a surprise to many in the computer science community. The combination of strong practical drivers and open competition in this experimental research effort created enough momentum to overcome the pessimism based on theory. Can we take these lessons to other problems and domains?

 

References

1. barrett, C., sebastiani, r., seshia, s., and tinelli, C. satisfiability modulo theories. a. biere, h. van Maaren, t. Walsh, eds. Handbook of Satisfiability 4, 8 (2009), Ios Press, amsterdam.

2. bayardo r., and schrag, r. using CsP look-back techniques to solve real-world sat instances. National Conference on Artificial Intelligence, 1997.

3. biere, a., Cimatti, a., Clarke, e. M., and zhu, y. symbolic model checking without bDDs. Tools and Algorithms for the Analysis and Construction of Systems, 1999.

4. braunstein, a., Mezard, M., and zecchina, r. survey propagation: an algorithm for satisfiability. Random Structures and Algorithms 27 (2005), 201–226.

5. bryant, r.e. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C- 35 (1986), 677–691.

6. Clarke, e.M., Grumberg, o., and Peled, D.a. Model Checking. MIt Press, Cambridge, Ma, 1999.

7. Copty, f., fix, l., fraer, r., Giunchiglia, e., kamhi, G., tacchella, a., and Vardi, M.y. benefits of bounded model checking at an industrial setting. Proceedings of the 13th International Conference on Computer-Aided Verification, 2001.

8. Cook, s.a. the complexity of theorem-proving procedures. Third Annual ACM Symposium on Theory of Computing, 1971.

9. Davis, M., logemann, G., and loveland, D. a machine program for theorem proving. Comm. ACM 5 (1962), 394–397.

10. Davis, M., and Putnam, h. a computing procedure for quantification theory. JACM 7 (1960), 201–215.

11. eén, n., and biere, a. effective preprocessing in sat through variable and clause elimination. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, 2005.

12. Garey, M.r., and Johnson, D.s. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. h. freeman, 1979

13. Gomes, C. P., selman, b., and kautz, h. boosting combinatorial search through randomization. In Proceedings of National Conference on Artificial Intelligence (Madison, WI, 1998).

14. hamadi, y., Jabbour, s., and sais, l. Manysat: solver description. Microsoft research, tr-2008-83.

15. huth, M. and ryan, M. Logic in Computer Science: Modeling and Reasoning about Systems. Cambridge university Press, 2004.

16. hutter, f., babic, D., hoos, h.h., and hu, a. J. boosting verification by automatic tuning of decision procedures. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, (austin, tx, nov. 2007).

17. Jackson, D., and Vaziri, M., finding bugs with a constraint solver. In Proceedings of the International Symposium on Software Testing and Analysis (Portland, or, 2000).

18. Jain, h. Verification using satisfiability checking, predicate abstraction, and Craig interpolation. Ph. D. thesis, Carnegie-Mellon university, school of Computer science, CMu-Cs-08-146, 2008.

19. Johnson, D.s., Mehrotra, a., and trick, M. a. Preface: special issue on computational methods for graph coloring and its generalizations. Discrete Applied Mathematics 156, 2; Computational Methods for Graph Coloring and its Generalizations. (Jan. 15, 2008), 145–146.

20. kautz, h. and selman, b. Planning as satisfiability. European Conference on Artificial Intelligence, 1992.

21. larrabee, t. test pattern generation using boolean satisfiability. IEEE Transactions on Computer-Aided Design (Jan. 1992) 4–15.

22. Madigan, M. W., Madigan, C.f., zhao, y., zhang, l., and Malik, s. Chaff: engineering an efficient sat solver. In Proceedings of the 38th Conference on Design Automation. (new york, ny, 2001).

23. Marchiori, e. and rossi, C. a flipping genetic algorithm for hard 3-sat problems. In Proceedings of the Genetic and Evolutionary Computation Conference (orlando, fl, 1999), 393–400.

24. Marques-silva, J. P, and sakallah, k.a. Conflict analysis in search algorithms for propositional satisfiability. IEEE International Conference on Tools with Artificial Intelligence, 1996.

25. Mazure, b., sas l., and Grgoire, e., tabu search for sat. In Proceedings of the 14th National Conference on Artificial Intelligence (Providence, rI, 1997).

26. McMillan, k.l., applying sat methods in unbounded symbolic model checking. In Proceedings of the 14th International Conference on Computer Aided Verification. lecture notes In Computer science 2404 (2002). springer-Verlag, london, 250–264.

27. Muscettola, n., Pandurang nayak, P., Pell, b., and Williams, b.C. remote agent: to boldly go where no aI system has gone before. Artificial Intelligence 103, 1–2, (1998), 5–47.

28. nam, G.-J., sakallah, k. a., and rutenbar, r.a. satisfiability-based layout revisited: Detailed routing of complex fPGas via search-based boolean sat. International Symposium on Field-Programmable Gate Arrays (Monterey, Ca, 1999).

29. narain, s., levin, G., kaul, V., Malik, s. Declarative infrastructure configuration and debugging. Journal of Network Systems and Management, Special Issue on Security Configuration. springer, 2008.

30. selman, b., kautz, h.a., and Cohen, b. noise strategies for improving local search. In Proceedings of the 12th National Conference on Artificial Intelligence (seattle, Wa, 1994). american association for artificial Intelligence, Menlo Park, Ca, 337–343.

31. selman, b., levesque, h., and Mitchell, D. a new method for solving hard satisfiability problems. In Proceedings of the 10th National Conference on Artificial Intelligence, (1992) 440–446.

32. seshia, s.a., lahiri, s.k., and bryant, r.e. a hybrid sat-based decision procedure for separation logic with uninterpreted functions. In Proceedings of the 40th Conference on Design Automation (anaheim, Ca, June 2–6, 2003). aCM, ny, 425–430; http://doi.acm. org/10.1145/775832.775945.

33. spears, W. M. simulated annealing for hard satisfiability problems. Cliques, Coloring and Satisfiability, Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science. D.s. Johnson and M.a. trick, eds. american Mathematical society (1993), 533–558.

34. spears, W. M. a nn algorithm for boolean satisfiability problems. In Proceedings of the 1996 International Conference on Neural Networks, 1121–1126.

35. stålmarck, G. a system for determining prepositional logic theorems by applying values and rules to triplets that are generated from a formula. u.s. Patent number 5276897, 1994.

36. tseitin, G. on the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2 (1968), 115–125. reprinted in Automation of reasoning vol. 2. J. siekmann and G. Wrightson, eds. springer Verlag, berlin, 1983, 466–483.

37. Williams, r., Gomes, C., and selman, b. backdoors to typical case complexity. In Proceedings. of the 18th International Joint Conference on Artificial Intelligence (2003), 1173–1178.

38. Williams, r., Gomes, C., and selman, b. on the connections between heavy-tails, backdoors, and restarts in combinatorial search. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, 2003.

39. xu, l., hutter, f., hoos, h. h., leyton-brown, k. satzilla: Portfolio-based algorithm selection for sat. Journal of Artificial Intelligence Research 32, (2008), 565–606.

40. zhang, h. Generating college conference basketball schedules by a sat solver. In Proceedings of the 5th International Symposium on Theory and Applications of Satisfiability Testing. (Cincinnati, oh, 2002).

 

Sharad Malik ( [e-mail]) is a professor in the Department of electrical engineering at Princeton university, Princeton, nJ.

Lintao Zhang ( [e-mail]) is a researcher at Microsoft research asia, beijing, China.