article

A pearl on SAT and SMT solving in Prolog

Authors:

Andy KingAuthors Info & Claims

Theoretical Computer Science, Volume 435

Pages 43 - 55

https://doi.org/10.1016/j.tcs.2012.02.024

Published: 01 June 2012 Publication History

Abstract

A succinct SAT solver is presented that exploits the control provided by delay declarations to implement watched literals and unit propagation. Despite its brevity the solver is surprisingly powerful and its elegant use of Prolog constructs is presented as a programming pearl. Furthermore, the SAT solver can be integrated into an SMT framework which exploits the constraint solvers that are available in many Prolog systems.

References

[1]

Barrett, C., Deters, M., Oliveras, A. and Stump, A., Design and results of the 3rd annual satisfiability modulo theories competition (SMT-Comp 2007). International Journal on Artificial Intelligence Tools. v17 i4. 569-606.

[2]

Bruynooghe, M., Intelligent backtracking revisited. In: Computational Logic, Essays in Honor of Alan Robinson, MIT Press. pp. 166-177.

[3]

Bruynooghe, M., Enhancing a search algorithm to perform intelligent backtracking. Theory and Practice of Logic Programming. v4 i3. 371-380.

[4]

Carlsson, M., Ottosson, G. and Carlson, B., An open-ended finite domain constraint solver. In: Lecture Notes in Computer Science, vol. 1292. Springer. pp. 191-206.

Digital Library

[5]

Codish, M., Lagoon, V. and Stuckey, P.J., Logic programming with satisfiability. Theory and Practice of Logic Programming. v8 i1. 121-128.

[6]

Davis, M., Logemann, G. and Loveland, D., A machine program for theorem proving. Communications of the ACM. v5 i7. 394-397.

[7]

Dovier, A., Formisano, A. and Policriti, A., On T logic programming. In: International Logic Programming Symposium, MIT Press. pp. 323-337.

[8]

Eén, N. and Biere, A., Effective preprocessing in SAT through variable and clause elimination. In: Lecture Notes in Computer Science, vol. 3569. pp. 61-75.

[9]

Eén, N. and Sörensson, S., An extensible SAT-solver. In: Lecture Notes in Computer Science, vol. 2919. Springer. pp. 502-518.

Digital Library

[10]

Gent, I.P., Jefferson, C. and Miguel, I., Watched literals for constraint propagation in Minion. In: Lecture Notes in Computer Science, vol. 4204. Springer. pp. 182-197.

[11]

C. Holzbaur, OFAI clp(q,r) Manual, Ed. 1.3.3. Technical report, Austrian Research Institute for Artificial Intelligence, 1995.

[12]

Howe, J.M. and King, A., Positive boolean functions as multiheaded clauses. In: Lecture Notes in Computer Science, vol. 2237. Springer. pp. 120-134.

Digital Library

[13]

Howe, J.M. and King, A., Efficient groundness analysis in Prolog. Theory and Practice of Logic Programming. v3 i1. 95-124.

[14]

Howe, J.M. and King, A., A pearl on SAT solving in Prolog. In: Lecture Notes in Computer Science, vol. 6009. Springer. pp. 165-174.

Digital Library

[15]

Imbert, J.-L. and Van Hentenrych, P., On the handling of disequations in CLP over linear rational arithmetic. In: Constraint Logic Programming, MIT Press. pp. 49-71.

[16]

Jaffar, J., Michaylov, S., Stuckey, P. and Yap, R., The CLP(R) language and system. ACM Transactions of Programming Languages and Systems. v14 i3. 339-395.

[17]

Jaffar, J., Santosa, A.E. and Voicu, R., An interpolation method for CLP traversal. In: Lecture Notes in Computer Science, vol. 5732. Springer. pp. 454-469.

Digital Library

[18]

Shostak's congruence closure as completion. In: Lecture Notes in Computer Science, vol. 1232. Springer. pp. 23-37.

Digital Library

[19]

King, A. and Martin, J.C., Control generation by program transformation. Fundamenta Informaticae. v69 i1-2. 179-218.

[20]

Kowalski, R.A., Algorithm = logic + control. Communication of the ACM. v22 i7. 424-436.

[21]

Kroening, D. and Strichman, O., Decision Procedures. 2008. Springer.

[22]

D. Le Berre, O. Roussel, L. Simon, The International SAT Competitions Webpage, 2009. http://www.satcompetition.org/.

[23]

Marques-Silva, J.P. and Sakallah, K.A., GRASP ¿ a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design, ACM and IEEE Computer Society. pp. 220-227.

[24]

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L. and Malik, S., Chaff: engineering an efficient SAT solver. In: Design Automation Conference, ACM Press. pp. 530-535.

[25]

Naish, L., Negation and Control in Logic Programs. 1986. Springer-Verlag.

[26]

Nieuwenhuis, R. and Oliveras, A., Proof-producing congruence closure. In: Lecture Notes in Computer Science, vol. 3467. pp. 453-468.

[27]

Nieuwenhuis, R., Oliveras, A. and Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM. v53 i6. 937-977.

[28]

Tseitin, G., On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (Ed.), Studies in Constructive Mathematics and Mathematical Logic, volume Part II, pp. 115-125.

[29]

Zhang, L. and Malik, S., The quest for efficient boolean satisfiability solvers. In: Lecture Notes in Computer Science, vol. 2404. Springer. pp. 17-36.

Digital Library

Cited By

Leuschel M(2024)B2SAT: A Bare-Metal Reduction of B to SATFormal Methods10.1007/978-3-031-71177-0_9(122-139)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_9
Cristiá MRossi G(2023)A Decision Procedure for a Theory of Finite Sets with Finite Integer IntervalsACM Transactions on Computational Logic10.1145/362523025:1(1-34)Online publication date: 18-Nov-2023
https://dl.acm.org/doi/10.1145/3625230
Drabent W(2023)A relaxed condition for avoiding the occur-checkTheoretical Computer Science10.1016/j.tcs.2023.114107975:COnline publication date: 9-Oct-2023
https://dl.acm.org/doi/10.1016/j.tcs.2023.114107
Show More Cited By

A pearl on SAT and SMT solving in Prolog
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
2. Theory of computation
  1. Logic

Recommendations

SMT solving for the validation of B and Event-B models
Abstract
ProB provides a constraint solver for the B-method written in Prolog and can make use of different backends based on SAT and SMT solving. One such backend translates B and Event-B operators to SMT-LIB using the Z3 solver. This translation uses ...
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-...
Truncating abstraction of bit-vector operations for BDD-based SMT solvers
Abstract
During the last few years, BDD-based SMT solvers proved to be competitive in deciding satisfiability of quantified bit-vector formulas. However, these solvers usually do not perform well on input formulas with complicated arithmetic. Hitherto, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 435, Issue

June, 2012

144 pages

ISSN:0304-3975

Issue’s Table of Contents

Copyright © Elsevier B.V. © 2012.

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 01 June 2012

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Leuschel M(2024)B2SAT: A Bare-Metal Reduction of B to SATFormal Methods10.1007/978-3-031-71177-0_9(122-139)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_9
Cristiá MRossi G(2023)A Decision Procedure for a Theory of Finite Sets with Finite Integer IntervalsACM Transactions on Computational Logic10.1145/362523025:1(1-34)Online publication date: 18-Nov-2023
https://dl.acm.org/doi/10.1145/3625230
Drabent W(2023)A relaxed condition for avoiding the occur-checkTheoretical Computer Science10.1016/j.tcs.2023.114107975:COnline publication date: 9-Oct-2023
https://dl.acm.org/doi/10.1016/j.tcs.2023.114107
Leuschel M(2020)Fast and Effective Well-Definedness CheckingIntegrated Formal Methods10.1007/978-3-030-63461-2_4(63-81)Online publication date: 16-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-63461-2_4
Howe JRobbins EKing AVanhoof WPientka B(2017)Theory learning with symmetry breakingProceedings of the 19th International Symposium on Principles and Practice of Declarative Programming10.1145/3131851.3131861(85-96)Online publication date: 9-Oct-2017
https://dl.acm.org/doi/10.1145/3131851.3131861
Drabent W(2016)Correctness and Completeness of Logic ProgramsACM Transactions on Computational Logic10.1145/289843417:3(1-32)Online publication date: 18-May-2016
https://dl.acm.org/doi/10.1145/2898434
Robbins EHowe JKing A(2015)Theory propagation and reificationScience of Computer Programming10.1016/j.scico.2014.05.013111:P1(3-22)Online publication date: 1-Nov-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.05.013
Robbins EHowe JKing APeña RSchrijvers T(2013)Theory propagation and rational-treesProceedings of the 15th Symposium on Principles and Practice of Declarative Programming10.1145/2505879.2505901(193-204)Online publication date: 16-Sep-2013
https://dl.acm.org/doi/10.1145/2505879.2505901

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents