Abstract
Here we give a short overview of the DPLL(T) approach to Satisfiability Modulo Theories (SMT), which is at the basis of current state-of-the-art SMT systems. After that, we provide a documented list of theoretical and practical current challenges related to SMT, including some new ideas to exploit SAT techniques in Constraint Programming.
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
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: System description: MathSAT 3. In: Nieuwenhuis, R. (ed.) Proceedings of the 20th Conference on Automated Deduction. LNCS (LNAI), vol. 3632, pp. 315–321. Springer, Heidelberg (2005)
Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Barrett, C., Tinelli, C.: CVC3. In: Computer Aided Verification, 19th International Conference (CAV). Springer LNCS (to appear, 2007)
Dutertre, B., de Moura, L.: The YICES SMT Solver (2006), http://yices.csl.sri.com/tool-paper.pdf
Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Comm. of the ACM 5(7), 394–397 (1962)
de Moura, L., Bjorner, N.: Efficient E-matching for SMT Solvers. In: xx, (submitted 2007)
Detlefs, D.L., Nelson, G., Saxe, J.: Simplify: the ESC theorem prover. Technical report, Compaq (December 1996)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)
Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. J. of the Association for Computing Machinery 27(4), 758–771 (1980)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT) pp. 502–518 (2003)
ILOG. ilog cplex, http://www.ilog.com/products/cplex
Kautz, H.A., Ruan, Y., Achlioptas, D., Gomes, C.P., Selman, B., Stickel, M.E.: Balance and Filtering in Structured Satisfiable Problems. In: Nebel, B. (ed.) 17th International Joint Conference on Artificial Intelligence, IJCAI 2001, pp. 351–358. Morgan Kaufmann, San Francisco (2001)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. 38th Design Automation Conference (DAC 2001) (2001)
Marques-Silva, J., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)
Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005)
Nieuwenhuis, R., Oliveras, A.: Proof-Producing Congruence Closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 453–468. Springer, Heidelberg (2005)
Nieuwenhuis, R., Oliveras, A.: On sat modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006)
Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Information and Computation 205(4), 557–580 (2007)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM 53(6), 937–977 (2006)
Régin, J-C.: A filtering algorithm for constraints of difference in CSPs. In: Proceedings of 12th National Conference on AI (AAAI 1994), vol. 1, pp. 362–367, Seattle, (July 31 - August 4, 1994)
Ranise, S., Tinelli, C.: The SMT-LIB Format: An Initial Proposal. In: Proceedings of the 1st Workshop on Pragmatics of Decision Procedures in Automated Reasoning, Miami (2003)
Roos, C., Terlaky, T., Vial, J.P.: Theory and Algorithms for Linear Optimization: An Interior Point +Approach. Wiley, Chichester, UK (1997)
Stump, A., Löchner, B.: Knuth-bendix completion of theories of commuting group endomorphisms. Inf. Process. Lett. 98(5), 195–198 (2006)
Stump, A., Tan, L.-Y.: The algebra of equality proofs. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 469–483. Springer, Heidelberg (2005)
Terlaky, T. (ed.): Interior Point Methods of Mathematical Programming, Applied Optimization, vol. 5. Kluwer Academic Publishers, Dordrecht (1996)
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A. (2007). Challenges in Satisfiability Modulo Theories. In: Baader, F. (eds) Term Rewriting and Applications. RTA 2007. Lecture Notes in Computer Science, vol 4533. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73449-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-73449-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73447-5
Online ISBN: 978-3-540-73449-9
eBook Packages: Computer ScienceComputer Science (R0)