A pearl on SAT and SMT solving in Prolog
DOI10.1016/J.TCS.2012.02.024zbMATH Open1248.68455OpenAlexW2121531736MaRDI QIDQ428887FDOQ428887
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
Recommendations
constraint logic programmingSAT solvingSMT solvingPrologdelay declarationsunit propagationwatched literal
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic programming (68N17)
Cites Work
- Theory and Applications of Satisfiability Testing
- Title not available (Why is that?)
- Theory and Applications of Satisfiability Testing
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- A machine program for theorem-proving
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Title not available (Why is that?)
- Title not available (Why is that?)
- Logic programming with satisfiability
- Negation and control in PROLOG
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Control generation by program transformation
- Term Rewriting and Applications
Cited In (16)
- Backjumping is Exception Handling
- On completeness of logic programs
- Correctness and completeness of logic programs
- Title not available (Why is that?)
- OptiLog: a framework for SAT-based systems
- Logic programming with satisfiability
- Logic + control: an example
- Writing declarative specifications for clauses
- Logic + control: on program construction and verification
- Title not available (Why is that?)
- A relaxed condition for avoiding the occur-check
- A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
- A note on occur-check
- Tools and Algorithms for the Construction and Analysis of Systems
- A Pearl on SAT Solving in Prolog
- The Boolean constraint solver of SWI-Prolog (system description)
Uses Software
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)
