A pearl on SAT and SMT solving in Prolog

DOI10.1016/J.TCS.2012.02.024MaRDI QIDQ428887zbMATH OpenOpenAlexFDO

Authors Jacob M. Howe, Andy King

Publication date 25 June 2012

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2012.02.024

zbMATH Keywords

constraint logic programmingSAT solvingSMT solvingPrologdelay declarationsunit propagationwatched literal

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic programming (68N17)

Recommendations

• A Pearl on SAT Solving in Prolog
• Logic programming with satisfiability
• Theory and Applications of Satisfiability Testing
• Logic + control: an example
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)

Cites work

• scientific article; zbMATH DE number 599028 (Why is no real title available?)
• scientific article; zbMATH DE number 2085273 (Why is no real title available?)
• scientific article; zbMATH DE number 1903342 (Why is no real title available?)
• scientific article; zbMATH DE number 1407682 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• A Pearl on SAT Solving in Prolog
• A machine program for theorem-proving
• Algorithm = logic + control
• Control generation by program transformation
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Efficient groundness analysis in Prolog
• Logic programming with satisfiability
• Negation and control in PROLOG
• PROGRAMMING PEARL: Enhancing a search algorithm to perform intelligent backtracking
• Shostak's congruence closure as completion
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Term Rewriting and Applications
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Watched Literals for Constraint Propagation in Minion

Cited in

(16)

• A Pearl on SAT Solving in Prolog
• OptiLog: a framework for SAT-based systems
• A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
• A note on occur-check
• Logic programming with satisfiability
• On completeness of logic programs
• The Boolean constraint solver of SWI-Prolog (system description)
• Backjumping is Exception Handling
• Writing declarative specifications for clauses
• Logic + control: on program construction and verification
• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• Logic + control: an example
• A relaxed condition for avoiding the occur-check
• Tools and Algorithms for the Construction and Analysis of Systems
• Correctness and completeness of logic programs
• scientific article; zbMATH DE number 7552282 (Why is no real title available?)

Describes a project that uses

Uses Software

• MiniSat
• Chaff

This page was built for publication: A pearl on SAT and SMT solving in Prolog

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q428887)