Content deleted Content added
trying again |
→Program reformulations: constraint handling rules |
||
Line 87:
A third reformulation that can increase efficiency is the addition of redundant constrains. If the programmer knows (by whatever means) that the solution of a problem satisfies a specific constraint, they can include that constraint to cause inconsistency of the constraint store as soon as possible. For example, if it is known beforehands that the evaluation of <code>B(X)</code> will result in a positive value for <code>X</code>, the programmer may add <code>X>0</code> before any occurrence of <code>B(X)</code>. As an example, <code>A(X,Y):-B(X),C(X)</code> will fail on the goal <code>A(-2,Z)</code>, but this is only found out during the evaluation of the subgoal <code>B(X)</code>. On the other hand, if the above clause is replaced by <code>A(X,Y):-X>0,A(X),B(X)</code>, the interpreter backtracks as soon as the constraint <code>X>0</code> is added to the constraint store, which happens before the evalation of <code>B(X)</code> even starts.
==Constraint handling rules==
Constraint handling rules specify how to rewrite the constraints in the constraint store. The programmer can use these rules to specify that some new constraints are equivalent or follows from other constraints, allowing for a rewriting or addition of new constraints in the store. The following are example rules:
A(X) <==> B(X) | C(X)
A(X) ==> B(X) | C(X)
The first rule tells that, if <code>B(X)</code> is entailed by the store, the constraint <code>A(X)</code> can be rewritten as <code>C(X)</code>. As an example, <code>N*X>0</code> can be rewritten as <code>X>0</code> if the store implies that <code>N>0</code>. The symbol <code><==></code> resembles equivalence in logic, and tells that the first constraint is equivalent to the latter. In practice, this implies that the first constraint can be ''replaced'' with the latter.
The second rule instead specifies that the latter constraint is a consequence of the first, if the constraint in the middle is entailed by the constraint store. As a result, if <code>A(X)</code> is in the constraint store and <code>B(X)</code> is entailed by the constraint store, then <code>C(X)</code> can be added to the store. Differently from the case of equivalence, this is an addition and not a replacement: the new constraint is added but the old one remains.
Equivalence allows for simplifying the constraint store. In particular, if the third constraint is <code>true</code>, and the second constraint is entailed, the first constraint is removed from the constraint store. Inference allows for the addition of new constraints, which may lead to proving inconsistency of the constraint store, and may generally reduce the amount of search needed to establish its satisfiability.
A specific method for establishing satisfiability of constraints can be defined using different clauses for implementing the different choices of the method, and the constraint handling rules for specifying how to rewrite the constraint store during execution. As an example, one can implement backtracking with [[unit propagation]] this way. Let <code>holds(L)</code> represents a propositional clause, in which the literals in the list <code>L</code> are in the same order as they are evaluated. The algorithm can be implemented using clauses for the choice of assigning a literal to true or false, and constraint handling rules to specify propagation. In particular, these rules specify that <code>holds([l|L])</code> can be removed if <code>l=true</code> follows from the store, and it can be rewritten as <code>holds(L)</code> if <code>l=false</code>.
==Bottom-up evaluation==
| |||