Backjumping is Exception Handling

DOI10.1017/S1471068420000435MaRDI QIDQ4957217zbMATH OpenOpenAlexFDO

Authors

Publication date 3 September 2021

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2008.04720

zbMATH Keywords

backjumpingconflict-driven clause learningexception handlingSAT

Mathematics Subject Classification ID

Coloring of graphs and hypergraphs (05C15) Logic programming (68N17) Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: ISO Prolog provides catch and throw to realise the control flow of exception handling. This pearl demonstrates that catch and throw are inconspicuously amenable to the implementation of backjumping. In fact, they have precisely the semantics required: rewinding the search to a specific point, and carrying of a preserved term to that point. The utility of these properties is demonstrated through an implementation of graph colouring with backjumping and a backjumping SAT solver that applies Conflict Driven Clause Learning.

Recommendations

• Backing backtracking
• Exploiting exceptions
• scientific article; zbMATH DE number 1113993
• Object-oriented backtracking
• scientific article; zbMATH DE number 2185662
• Exception handling—A static approach

Cites work

• A pearl on SAT and SMT solving in Prolog
• A Pearl on SAT Solving in Prolog
• A theoretical evaluation of selected backtracking algorithms.
• Algorithm = logic + control
• Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
• scientific article; zbMATH DE number 3684931 (Why is no real title available?)
• scientific article; zbMATH DE number 42857 (Why is no real title available?)
• scientific article; zbMATH DE number 867332 (Why is no real title available?)
• Logic + control: on program construction and verification
• PROGRAMMING PEARL: Enhancing a search algorithm to perform intelligent backtracking
• SICStus Prolog -- the first 25 years
• SWI-Prolog

Cited in

(3)

• Constraint learning for non-confluent proof search
• Implementing backjumping by means of exception handling
• Automatic differentiation in Prolog

Describes a project that uses

Uses Software

• Chaff
• SICStus
• SWI-Prolog

This page was built for publication: Backjumping is Exception Handling

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