A pearl on SAT and SMT solving in Prolog

DOI10.1016/j.tcs.2012.02.024zbMath1248.68455OpenAlexW2121531736MaRDI QIDQ428887

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

Prologconstraint logic programmingSAT solvingSMT solvingdelay declarationsunit propagationwatched literal

Mathematics Subject Classification ID

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

Related Items (7)

Correctness and Completeness of Logic Programs ⋮ On Completeness of Logic Programs ⋮ A relaxed condition for avoiding the occur-check ⋮ A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals ⋮ Logic + control: On program construction and verification ⋮ Unnamed Item ⋮ Backjumping is Exception Handling

Uses Software

• MiniSat
• Chaff

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Negation and control in PROLOG
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Solving SAT and SAT Modulo Theories
• Watched Literals for Constraint Propagation in Minion
• A Pearl on SAT Solving in Prolog
• Algorithm = logic + control
• Efficient groundness analysis in Prolog
• Shostak's congruence closure as completion
• PROGRAMMING PEARL: Enhancing a search algorithm to perform intelligent backtracking
• Theory and Applications of Satisfiability Testing
• Logic programming with satisfiability
• A machine program for theorem-proving
• Term Rewriting and Applications
• Theory and Applications of Satisfiability Testing

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