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 ( sharad@princeton.edu) is a professor in
the Department of electrical engineering at Princeton
university, Princeton, nJ.
Lintao Zhang ( lintaoz@microsoft.com) is a researcher at
Microsoft research asia, beijing, China.