2 Backjumping and Prolog exception handling

In this section we present and compare backjumping and the Prolog exception handling.

2.1 Backjumping

A Prolog computation can be seen as a depth-first left-to-right traversal of an SLD-tree. Each node with i children is visited $i+1$ times (it is first entered from its parent and then from each of its children). Moving from a node to its parent is called backtracking. By backjumping we mean skipping a part of the traversal, by moving immediately from a node to one of its non-immediate ancestors (called the backjumping target). Intelligent backtracking (Bruynooghe and Pereira Reference Bruynooghe, Pereira and Campbell1984) is backjumping in which it is known that there are no successes in the omitted part of the SLD-tree.

Let us a have a more detailed look. Consider a node Q with k children $Q_1,\ldots,Q_k$ (Figure 1). We may say that k backtrack points correspond to Q; backtracking from $Q_i$ means arriving to Q at its i-th backtrack point. Obviously, this is followed by visiting $Q_{i+1}$ when $i<k$ , and by backtracking to the parent of Q when $i=k$ . Similarly, backjumping to Q from a node in the subtree rooted in $Q_i$ should arrive at the i-th backtrack point. Thus such backjumping is followed by visiting $Q_{i+1}$ when $i<k$ , and the parent of Q when $i=k$ .

Fig. 1. Backjumping to Q from the subtree ${\cal S}$ rooted in $Q_i$ (when $i<k$ ) is followed by visiting $Q_{i+1}$ . For $i=k$ the backjumping is followed by visiting the parent of Q.

Consider exception handling (implemented by making N to be catch(Q,s,H)). Exception s raised in ${\cal S}$ (and not caught in ${\cal S}$ ) results in skipping $Q_{i+1},\ldots,Q_k$ and all their descendants. Additionally, the LD-tree is extended by a subtree corresponding to executing the exception handler H.

One may consider a generalization of backjumping, where not only a part of the subtree rooted in $Q_i$ is skipped, but also the subtrees rooted in $Q_{i+1},\ldots,Q_j$ (for some $j\in\{i{+}1,\ldots,k\}$ ). We do not discuss such a generalization here.

3 Employing exception handling

This section introduces two restricted approaches to implement backjumping. Examples are given in the next section. We consider Prolog without coroutining/delays.

3.1 Approach 1

Assume that we deal with a definite clause program P, which we want to execute with backjumping. The target of backjumping is to be identified by a term id. So backjumping is initiated by throw(id).

Assume that the target of backjumping is a node A,Q of the LD-tree, where A is an atom. Assume that A,Q has k children, ${{Q_{1}, \ldots, Q_{k}}}$ . Let p be the predicate symbol of A and

(1) \begin{equation}\begin{array}{l} p(\vec t_1)\gets B_1. \\ \cdots \\ p(\vec t_n)\gets B_n.\end{array}\end{equation}

where $k\leq n$ , be the procedure p of program P (i.e. the clauses of P beginning with p).

Consider backjumping initiated by throw(id) in the subtree rooted in $Q_i$ . The subtree should be abandoned, but the descendants of $Q_{i+1},\ldots,Q_k$ should not. Thus we need to restrict the exception handling to this subtree. A way to do this is to replace each $B_j$ by $catch( B_j, id, {\it fail} )$ . Then performing throw(id) while executing $B_j$ results in failure of the clause body and backtracking to the next child of A,Q, as required. Assume that a query $b t id(\vec t,Id)$ produces out of the arguments $\vec t$ of p the unique identifier of A,Q as the backjump target. Now, the backjumping is implemented by a transformed procedure consisting of clauses

(2) \begin{equation}{p(\vec t_j)\gets b t id(\vec t_j,Id), \, catch( B_j, Id, fail ) }.\qquad\qquad \mbox{for }j=1,\ldots,n\end{equation}

(where Id is a variable).

Transforming a program in this way correctly implements backjumping, however with an important limitation. Backjumping to a node $p(\vec t\,),Q$ must occur during the execution of $p(\vec t\,)$ . Otherwise the exception is not caught and the whole computation terminates abnormally.

An important class of programs which satisfy this limitation are binary logic programs (i.e. programs with at most one body atom in a clause). The approach presented here works for such programs and arbitrary backjumping. It also works when each backjump target is a node consisting of a single atom.

Sometimes (like in Example 2 below) it may be determined in advance that, for some j, no exception will be caught by the catch/3 in (2). So in practice some clauses of (1) may remain unchanged (or a choice between $B_j$ and ${\it catch( B_j, Id, fail)}$ may be made dynamically, for example by modifying the body of (2) into ${b t id(\vec t_j,Id) \to catch( B_j, Id, {\it fail} ) [3]\mathop; B_j}$ ).

Approach 1a. Here we present a variant of Approach 1. Roughly speaking, in the former approach control is transferred to the next clause due to failure of a clause body. So catching an exception causes an explicit failure. Here control is transferred to the next clause by means of an exception (hence standard backtracking is to be implemented by means of exceptions). To simplify the presentation we assume that in (1) all the clause heads are the same, $\vec t_1=\cdots=\vec t_n=\vec t$ .

Assume first that $n=2$ . Backjumping equivalent to that of Approach 1 can be implemented by

(3) \begin{equation}\begin{array}{l}p(\vec t\,) \gets b t id(\vec t,Id), catch( \begin{array}[t]{l} (B_1 \mathrel; throw(Id)), \\ Id, \\{ catch( B_2, Id, {\it fail})\ ).} \end{array}\end{array}\end{equation}

Invocation of $B_2$ is placed in the exception handler, so we additionally raise an exception when $B_1$ (the first clause body) fails. For arbitrary n, the transformed procedure (1) is:

(4)

Generalizing this transformation to clauses with different heads is rather obvious. Note that in this approach it is possible to augment backjumping by passing information (from the place where the backjump originates to the backjump target).^{Footnote 1} Such augmenting is impossible in Approach 1 and Approach 2 below.

3.2 Approach 2, approximate backjumping

We have shown how to implement backjumping to an LD-tree node $N = A,Q$ (with atomic A) from within the execution of A. It remains to discuss backjumping originating in the execution of Q.

Assume that the initial query is atomic; dealing with arbitrary initial queries is similar. In such case, the program contains a clause $H{\gets}B_0,B_1$ (where $B_0,\,B_1$ are nonempty), such that, speaking informally, the backjumping is from within the execution of $B_1$ , and its target N is within the execution of $B_0$ .

Let us prove that such clause exists. Assume that the backjumping target is $N=A,Q$ (A is an atom), and that the backjumping originates in a node N’ in the execution of Q in N (Figure 2). Let $\cal{D}$ be a branch of the LD-tree containing N and N’.

Fig. 2. Dotted lines connect an atom sequence with a query from its execution. N,N’ are of the form $N=A,\ldots,(B_1,Q_0)\theta\rho$ , $ N'={\it throw(id)},\ldots,Q_0\theta\rho\varphi$ .

Obviously N occurs in the execution in $\cal{D}$ of A in N, and N’ does not. As the root of the tree is atomic, there exist in $\cal{D}$ a node $N_0$ and its child $N_1$ such that N and N’ (i) occur in the execution in $\cal{D}$ of a single atom $A_0$ in $N_0$ and (ii) do not occur in the execution in $\cal{D}$ of a single atom in $N_1$ . Note that $A_0$ is the first atom of $N_0$ (otherwise (ii) does not hold). The two nodes are of the form $N_0=A_0,Q_0$ and $N_1=(Q',Q_0)\theta$ , and a clause $H\gets Q'$ was used to obtain $N_1$ .

Now Q’ can be split as $Q'=B_0,B_1$ (hence $N_1=(B_0,B_1,Q)\theta$ ), so that N occurs in the execution of $B_0\theta$ in $N_1$ , and N’ occurs in the execution of $B_1\theta$ in $N_1$ . So $H\gets B_0,B_1$ has the required property.

We are going to implement backjumping from N’ to the last node N” of the execution of $B_0\theta$ in $N_1$ . To make N” as close as possible to N, one should choose $B_0,B_1$ so that N is in the execution of the last atom of $B_0\theta$ .

As discussed in Section 2.3, such backjumping (from within the execution of $B_1$ to a target in the execution of $B_0$ ) cannot be implemented by means of throw/1 and catch/3. What can be done is to force $B_1$ to fail when an exception is thrown. This means, speaking informally, backjumping to the success of $B_0$ , instead of the original target N. This in a sense approximates backjumping to N. In some cases such shorter backjumping may still be useful. It may exclude from the search space a major part of what would be excluded by backjumping to N.

The success of $B_0$ (formally of $B_0\theta$ ) is the topmost descendant of N of the form $N''=(B_1,Q_0)\theta\rho\psi$ (here $\theta,\rho$ , $Q_0,N',N''$ are as in Figure 2 and the proof above). Node N” appears in the tree branch between N and node N’ that originates the backjump. To catch the exception at N” we modify the program, so that the instance $B_1\theta\rho\psi$ of $B_1$ in node N” is replaced by $catch(B_1\theta\rho\psi,id,{\it fail})$ . (The resulting backjumping may be understood as arriving to the last backtrack point of N”, or – due to the handler fail – to the parent of N”.) To obtain this, the clause

\[H\gets B_0,B_1\ \quad \mbox{ is transformed to } \ \quad H\gets B_0,\, b t id(\ldots,Id), \, catch(B_1,Id,{\it fail})\]

where b t id, as previously, is used to obtain the unique identifier for the backjump target.

4 Examples

We apply the approaches introduced above to a simple program, a naive SAT solver. It uses the representation of clauses proposed by Howe and King (Reference Howe and King2012). (Note that we deal here with two kinds of clauses – those of the program, and the propositional clauses of a SAT problem.) A conjunction of clauses is represented as a list of (the representations of) clauses. A clause is represented as a list of (the representations of) literals. A positive literal is represented as a pair ${\mbox{true-}} X$ and a negative one as ${\mbox{false-}} X$ , where the Prolog variable represents a propositional variable. For instance a formula $(x\lor\neg y\lor z)\land(\neg x\lor v)$ is represented as [[true-X,false-Y,true-Z],[false-X,true-V]]. In what follows we do not distinguish literals, clauses, etc from their representations.

Thus solving a SAT problem for a conjunction of clauses sat means instantiating the variables of sat in such way that each of the lists contains an element of the form $t{\mbox{-}} t$ . This can be done by a program $P_1$ :

and a query ${\it sat\_c n f}(sat)$ . See the paper by Drabent (Reference Drabent2018, Section 3) for further discussion and a formal treatment of the program.

The examples below add backjumping to program $P_1$ . They are not intended to provide a correct SAT solver, their role is only to illustrate Approaches 2 and 1. In the examples, the backjumping is performed after a failure of ${\it sat\_c l}(cl)$ (where cl is the representation of a partly instantiated clause). The intended backjumping target is the last point where a variable from clause cl was assigned a value.

Note that such backjumping does not correctly implement intelligent backtracking, some answers are lost. For example for $(x\lor y)\land(\neg z\lor z)\land(\neg x\lor\neg y)\land (\neg x\lor y\lor z)$ no solution with z being true is found. An explanation is that, speaking informally, backjumping from the last clause (with x,y,z instantiated to true, false, false or to true, false, false) arrives to the previous one (where y or x was set), this causes backjumping to the first clause.

We augment the values of variables; the value of a variable is going to be of the form (l,v), where l is a number (the level of the variable) and v a logical value true or false. The level shows at which recursion depth of ${\it sat\_c n f}$ the value was assigned. The levels will be used as identifiers for backjump targets. In such setting, a substitution $\theta$ assigning values to variables makes a SAT problem sat satisfied when each member of list $sat\theta$ contains a pair of the form $ v{\mbox{-}}(l, v)$ . This leads to transforming the first clause of $P_1$ to .

We transform $P_1$ into a program $P_2$ which takes levels into account. We add the current level as the second argument of ${\it sat\_c n f}$ and of ${\it sat\_c l}$ . A third argument is added to ${\it sat\_c l}$ ; it is used in finding the highest variable level in a clause. The declarative semantics of the new program is similar to that of $P_1$ ; the answers of $P_2$ are as follows. If the first argument of ${\it sat\_c l}$ is a list then it has a member of the form $t{\mbox{-}}(t',t)$ . Also, this condition is satisfied by each element of the list that is the first argument of ${\it sat\_c n f}$ .

Operationally, an invariant will be maintained that, whenever ${\it sat\_cl(cl,l,h l)}$ is selected in LD-resolution, cl is a list and l and h l are numbers, $l>h l$ and l is greater than any number occurring in cl. List cl is the not yet processed fragment of a clause $cl_0$ (possibly instantiated), l is the current level, and ${\it h l}$ is the highest level of those variables that occur in the already processed part of $cl_0$ and have been bound to some values at previous levels; ${\it h l}=-1$ when there is no such variable. In case of failure of ${\it sat\_c l(cl,l,h l)}$ , an exception will be raised with the ball being the maximum of h l and the levels of the variables occurring in cl (provided the maximum is $\geq0$ ).

Checking the value already assigned to a variable must be treated differently from assigning a value to an unbound variable (as its level is set only in the latter case). This leads to two clauses playing the role of the first clause of $P_1$ . So procedure ${\it sat\_c l}$ of $P_1$ is transformed into the following procedure of $P_2$ :

(5)

(6)

(7)

Predicate ${\it new\_highest}$ takes care of updating the highest level of the variables from the already processed part of the clause.

(8)

(9)

(10)

Procedure ${\it sat\_c n f}$ is transformed into

(11)

(12)

Program $P_2$ consists of clauses (5)–(12). An initial query ${\it sat\_c n f}(sat,0)$ results in checking the satisfiability of a conjunction of clauses sat.

Now we add backjumping to $P_2$ . The backjumping has to be triggered instead of a failure of ${\it sat\_cl}$ . The latter happens when the first argument of ${\it sat\_cl}$ is $[\,]$ . The new program $P_3$ contains the procedure ${\it sat\_cl}$ of $P_2$ , and additionally a clause

(13)

triggering a backjump. When ${\it H L}<0$ then there is no target for backjumping, and standard backtracking is performed.

The procedure ${\it sat\_c n f}$ of the new program $P_3$ , is constructed out of that of $P_2$ by transforming clause (12) as described in Approach 2:

(14)

So backjumping related to the variable with level l, implemented as throw(l), arrives to an instance of clause (14) where L is l. The whole $catch(\ldots)$ fails, and the control backtracks to the invocation of ${\it sat\_c l}$ that assigned the variable. (An additional predicate ${\it b t id}$ was not needed, as L is the unique identifier.)

Now program $P_3$ consists of clauses (5)–(11) and (13)–(14). To avoid leaving unnecessary backtrack points in some Prolog systems, each group of clauses with var/1 and ${\it non var}$ /1 (clause (5) with (6), and (8) with (9) and (10)) may be replaced by a single clause employing $({\it var(V) \mathop\to \ldots{;}\ldots })$ and, in the second case additionally $({\it H{<}L \mathop\to \ldots{;}\ldots })$ . To simplify a bit the initial queries, a top level predicate may be added, defined by a clause

Note that in Example 1 the unprocessed part of the current clause was an argument of ${\it sat\_cl}$ , now it is the head of the argument of ${\it sat\_b}$ . In what follows we do not explain some details which are as in the previous example.

As previously we introduce levels, and represent a value of a variable by (l, v), where l is a level and v a logical value. As previously, we first transform $P_{{\rm b}}$ into $P_{{\rm b}2}$ dealing with levels, and then add backjumping to $P_{{\rm b}2}$ . We add two arguments to ${\it sat\_b}$ , they are the same as the arguments added to ${\it sat\_cl}$ in Example 1. The declarative semantics is similar, the first argument of ${\it sat\_b}$ (in an answer of $P_{{\rm b}2}$ ) is as the first argument of ${\it sat\_c n f}$ in $P_2$ . An invariant similar to that of Example 1 will be maintained by the operational semantics. Whenever ${\it sat\_b(cl s,l,h l)}$ is selected, l and h l are numbers, $l>h l$ and l is greater than any number occurring in ${\it cl s}$ . List ${\it cl s}$ is a conjunction of clauses (possibly instantiated), and its head, say cl, is the not yet processed fragment of the current clause, say $cl_0$ ; number l is the current level, and ${\it h l}$ is the highest level of variables from the already processed part of $cl_0$ . Now program $P_{{\rm b}2}$ is:

(15)

(16)

(17)

(18)

Procedure ${\it new\_highest}$ /3 is the same as in the previous example. Program $P_{{\rm b}2}$ with a query ${\it sat\_b}(sat,0,-1)$ checks satisfiability of the conjunction of clauses sat.

Now we add backjumping to $P_{{\rm b}2}$ . Approach 1 is applicable, as each backjump target of interest consists of a single atom ${\it sat\_b}(\ldots)$ . As previously, backjumping originates when an empty clause is encountered:

(19)

Let us discuss backjump targets. Speaking informally, we backjump to a place where a variable obtained a value; this happens only in clause (17). So only this clause has to be modified to implement backjump target. For a proof, assume that the nodes of an LD-tree satisfy the invariant. Consider the descendants of a node $N = {\it sat\_b(cl s,l,h l)}$ obtained by first resolving N with clause (16) or (18). A ball thrown from such a descendant $N_2$ is not l.^{Footnote 2} So (16), (18) transformed to the form (2) will never catch a ball, and transforming them is unnecessary.

Out of (17) we obtain:

(20)

The final program $P_{{\rm b}3}$ consists of clauses (15), (16), (20), (18), (19), and (8)–(10).

In (20), the first atom ${\it var}(V)$ from the body of (17) can be moved outside of catch, transforming the body of (20) to ${\it var(V), catch(\ldots)}$ . (This is because ${\it var}(V)$ is deterministic and not involved in backjumping.) Now, similarly as in the previous example, some backtrack points may be avoided by replacing clauses (20) and (16) by a single clause with the body

Let us also mention that applying Approach 1a to $P_{{\rm b}2}$ results in adding clause (19) and replacing clauses (16)–(18) by

5. Simulating backjumping by backtracking

This section complements the current paper by presenting an approach not based on exception handling. We discuss simulating backjumping by means of Prolog backtracking, as suggested by Bruynooghe (Reference Bruynooghe2004). A backjump is initiated by a failure preceded by depositing in the Prolog database an identifier of the backjump target. At each backtracking step, the database is queried to check if backjumping is being performed and if its target is reached; further backtracking is caused if necessary. This is done by some extra code placed at the beginning of the body of each clause involved in backjumping. (In the presented example (Bruynooghe Reference Bruynooghe2004), there is only one such clause.)

The paper by Bruynooghe is focused on a single example, here we make it explicit how to implement the idea in a general case. Let us introduce a predicate catch/1, to deal with backtracking that simulates backjumping. The role of catch(t) is to succeed immediately, unless during backjumping. In the latter case catch(t) fails if t is not unifiable with (the identifier of) the backjumping target. In this way the backjumping is continued. Otherwise it removes the target from the database and succeeds (instantiating t in the obvious way). This means completing the backjump.

We can use ${\it assert(target(t')), fail}$ to cause a backjump, and define

Query ${\it retract(target(t))}$ fails when t is not unifiable with the recorded target t’. Otherwise it succeeds and removes the database item, in this way indicating the end of the backjump.

To maintain such simulated backjumping, we convert each clause $p(\vec{t}\, )\gets B$ of the program into

(21)

where b t id/2 is as in Section 3. Let us present an informal explanation. Note first that if the database is empty then the behaviour of (21) does not differ from that of the original clause. Assume now that backjumping has been initiated, so target(t’) is asserted and backtracking has started. At each backtrack point, a clause of the form (21) is involved. If catch finds that the backjumping target is reached, B is executed. Otherwise catch fails, and the simulated backjump continues.

Often for many clauses of the program it is known that ${\it catch(Id)}$ in (21) will not catch any backjump. In such case the clause can be simplified to

(22)

Note that there are no restrictions in this approach on the origin or target of backjumping, in contrast to those discussed in Section 3.

6 Final comments

Related work. For the approach of DBLPBruynooghe (Reference Bruynooghe2004), see the previous section. Robbins et al . (Reference Robbins, King and Howe2021) do not present any general approach, but they show a sophisticated example of using Prolog exception handling to implement backjumping. (The main example is preceded by a simple introductory one.) The program is a SAT solver with conflict-driven clause learning. A learned clause determines the target of a backjump. Note that the issue dealt with is not exactly backjumping, understood as in Section 2. In the SAT solver, not only a fragment of the SLD-tree is to be skipped, but additionally the tree has to be extended, as a new clause is added to the SAT problem.

The program employs Prolog coroutining in a fundamental way. It uses exception handling also to deal with plain backtracking. It keeps the learned clauses in the Prolog database, to preserve them during backjumping. The program is rather complicated; it seems impossible to view it as some initial program with added backjumping. To understand it one has to reason about the details of the operational semantics. This is not easy, due to sophisticated interplay of coroutining and exception handling. (The involved semantic issues are discussed here in Appendix A.)

That paper does not propose any general way of adding backjumping to logic programs. The difference between backjumping and Prolog exception handling discussed here in Section 2 is not noticed.^{Footnote 3} We cannot agree with the claims “backjumping is exception handling" and that “catch and throw [provide] exactly what is required for programming backjumping” (Robbins et al . Reference Robbins, King and Howe2021, the title, and pp. 142–143).

Conclusions. The subject of this paper is adding backjumping to logic programs. We discussed the differences between backjumping and Prolog exception handling, and showed that implementing the former by the latter is impossible in a general case (Section 2.3). We proposed two approaches to such implementation. The first approach imposes certain restrictions on where backjumping can be started. The second one – on the target of backjumping. The restrictions seem not severe. The first approach is applicable, among others, to binary programs with arbitrary backjumping. For the second approach, the presented example shows that sometimes the difference between the required and the actual target may be unimportant. As every program can be transformed to a binary one (Maher Reference Maher, Minker and Kaufmann1988; Tarau and Boyer Reference Tarau, Boyer, Deransart and Maluszynski1990), the first approach is indirectly applicable to all cases.