City Research Online

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.

Publication Type:	Article
Additional Information:	This article is published in a revised form in Theory and Practice of Logic Programming: https://doi.org/10.1017/S1471068420000435. This version is published under a Creative Commons CC-BY-NC-ND. No commercial re-distribution or re-use allowed. Derivative works cannot be distributed. © the authors.
Publisher Keywords:	Backjumping, Exception handling, Conflict Driven Clause Learning, SAT
Subjects:	Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments:	School of Science & Technology > Computer Science > Software Reliability
SWORD Depositor:	Symplectic Administrator

Export

Downloads