Article

SAT and SMT are still resolution: questions and challenges

Author:

Robert NieuwenhuisAuthors Info & Claims

IJCAR'12: Proceedings of the 6th international joint conference on Automated Reasoning

Pages 10 - 13

https://doi.org/10.1007/978-3-642-31365-3_3

Published: 26 June 2012 Publication History

Publisher Site

Abstract

The aim of this invited talk is to discuss strengths, limitations and challenges around one of the simplest yet most powerful practical automated deduction formalisms, namely propositional SAT and its extensions. We will see some of the reasons why CDCL SAT solvers are so effective for finding solutions to so diverse real-world problems, using a single fully automatic push-button strategy, and, by extending them to SAT Modulo Theories (SMT), also to optimization problems and problems with complex (e.g., arithmetic) constraints for which a full encoding into SAT would be too large and/or inefficient. We will give some examples of trade-offs regarding full SAT encodings vs SMT theory solvers, and discuss why SAT and even SMT are just binary resolution strategies, the consequences of this fact, and possible ways to overcome it. Many aspects of the discussion carry over to first-order logic and beyond.

References

[1]

Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning sat solvers. In: Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence. AAAI (2010).

Digital Library

Google Scholar

[2]

Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195-221 (2011).

Digital Library

Google Scholar

[3]

Abío, I., Stuckey, P.J.: Conflict-directed lazy decomposition (submitted, 2012).

Google Scholar

[4]

Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (February 2009).

Digital Library

Google Scholar

[5]

Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Biere, et al. (eds.) {BHvMW09}, vol. 185, ch. 26, pp. 825-885 (February 2009).

Google Scholar

[6]

Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277-1284 (2010).

Digital Library

Google Scholar

[7]

Larrosa, J., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: A framework for certified boolean branch-and-bound optimization. J. Autom. Reasoning 46(1), 81-102 (2011).

Digital Library

Google Scholar

[8]

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).

Digital Library

Google Scholar

[9]

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).

Digital Library

Google Scholar

[10]

Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357-391 (2009).

Digital Library

Google Scholar

[11]

Zhang, L., Malik, S.: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. In: 2003 Conference on Design, Automation and Test in Europe Conference, DATE 2003, pp. 10880-10885. IEEE Computer Society (2003).

Digital Library

Google Scholar

Cited By

View all

Dai SLiu GZhang ZAnderson JBazargan K(2018)A Scalable Approach to Exact Resource-Constrained Scheduling Based on a Joint SDC and SAT FormulationProceedings of the 2018 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays10.1145/3174243.3174268(137-146)Online publication date: 15-Feb-2018
https://dl.acm.org/doi/10.1145/3174243.3174268

Recommendations

SAT and SMT: Their Algorithm Designs and Applications
APSEC '13: Proceedings of the 2013 20th Asia-Pacific Software Engineering Conference (APSEC) - Volume 02

SAT and SMT (SAT modulo theory) solvers aim to find a satisfiable instance of given constraints. SAT solver accepts a boolean constraints in a conjunctive normal form (CNF), such as, and if a CNF is satisfiable, returns an instance, such as. SMT solver ...
Approximating Quantified SMT-Solving with SAT
SSIRI-C '11: Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement - Companion

Satisfiability Modulo Theories (SMT) is an extension of SAT towards FOL. SMT solvers have proven highly scalable and efficient for problems based on some ground theorems. However, SMT problems involving quantifiers and combination of theorems is a long-...
Resolution for Max-SAT

Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses in a CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

IJCAR'12: Proceedings of the 6th international joint conference on Automated Reasoning

June 2012

568 pages

ISBN:9783642313646

Editors:
Bernhard Gramlich
Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9, E185/2, Wien, Austria
,
Dale Miller
École Polytechnique, INRIA Saclay and Laboratoire d'Informatique, Route de Saclay, Palaiseau Cedex, France
,
Uli Sattler
School of Computer Science, University of Manchester, Oxford Road, Manchester, UK

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 26 June 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Dai SLiu GZhang ZAnderson JBazargan K(2018)A Scalable Approach to Exact Resource-Constrained Scheduling Based on a Joint SDC and SAT FormulationProceedings of the 2018 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays10.1145/3174243.3174268(137-146)Online publication date: 15-Feb-2018
https://dl.acm.org/doi/10.1145/3174243.3174268

Abstract

References

Cited By

Recommendations

SAT and SMT: Their Algorithm Designs and Applications

Approximating Quantified SMT-Solving with SAT

Resolution for Max-SAT

Comments

Information

Published In

Sponsors

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations