Next: Summary Up: Quantification and QPROP Previous: Subsearch and quantification

Inference and Learning

As in Section 3, working with a modified representation allows certain inference techniques that are not applicable in the Boolean case.

As an example, suppose that we are resolving

with

to conclude
 (45)

where the capital letters indicate ground elements of the domain as before and the resolvents are actually ground instances of
 (46)

and
 (47)

It is obviously possible to resolve (46) and (47) directly to obtain
 (48)

which is more general than (45). For a procedure that learns new nogoods and uses them to prune the resulting search, the impact of learning the more general (48) can be substantial and can easily outweigh the cost of the unification step required to conclude that and resolve if . We have also discussed this elsewhere [ParkesParkes1999].

There are two new difficulties that arise when we implement these ideas. The first is a consequence of the fact that resolution can be ambiguously defined for two quantified clauses. Consider resolving

 (49)

with
 (50)

If we unify the first term in (50) with the first term in (49), we obtain as the resolvent; if we unify with the second term of (49), we obtain .

In practice, however, this need not be a problem:

Proposition 5.4   Let and be two lifted clauses, and and ground instances that resolve to produce . Then there is a unique natural resolvent of and of which is a ground instance.

Proof. If there is more than one pair of resolving literals in and the result of the resolution will be vacuous, so we can assume that there is a single literal in with in . If is the th literal in and the th literal in , it follows that we can resolve the original and by unifying the th literal in and the th literal in . It is clear that this resolution will be a generalization of .

What this suggests is that the reasons being associated with literal values be not the lifted nogoods that are retained as clauses, but ground instances thereof that were initially used to prune the search space and can subsequently be used to break ambiguities in learning.

The second difficulty is far more substantial. Suppose that we have the axiom

or, in a more familiar form, the usual transitivity axiom

This might be used in reasoning about a logistics problem, for example, if it gave conditions under which two cities were connected by roads.

Now suppose that we are trying to prove for an and a that are far apart'' given the skeleton of the relation that we already know. It is possible that we use resolution to derive

as we search for a proof involving a single intermediate location, and then

as we search for a proof involving two such locations, and so on, eventually deriving the wonderfully concise
 (51)

for some suitably large .

The problem is that if is the size of our domain, (51) will have ground instances and is in danger of overwhelming our unit propagation algorithm even in the presence of reasonably sophisticated subsearch techniques. Some technique needs to be adopted to ensure that this difficulty is sidestepped in practice. One way to do this is to learn not the fully general (51), but a partially bound instance that has fewer ground instances.

Procedure 5.5   To construct , the nogood that will be learned after a clause has been produced in response to a backtrack, with the ground reason associated with :

We may still learn a nogood with an exponential number of ground instances, but at least have some reason to believe that each of these instances will be useful in pruning subsequent search. Note that there is a subsearch component to Procedure 5.5, since we need to find ground instances of that are irrelevant. This cost is incurred only once when the clause is learned, however, and not at every unit propagation or other use.

It might seem more natural to learn the general (51), but to modify the subsearch algorithm used in unit propagation so that only a subset of the candidate clauses is considered. As above, the most natural approach would likely be to restrict the subsearch to clauses of a particular irrelevance or better. Unfortunately, this won't help, since irrelevant clauses cannot be unit. Restricting the subsearch to relevant clauses is no more useful in practice than requiring that any search algorithm expand only successful nodes.

Before moving on, let us note that a similar phenomenon occurs in the pseudo-Boolean case. Suppose we have a partial assignment and constraints

 (52) (53)

Unit propagation now causes the variable to be simultaneously true (by virtue of (52)) and false (because of (53)). Resolving these reasons together as in Proposition 3.12 gives us
 (54)

The conflict set here is easily seen to be , and this is indeed prohibited by the derived constraint (54). But (54) eliminates some additional bad assignments as well, such as . Just as in the lifted case, we have learned something about a portion of the search space that has yet to be examined.

Next: Summary Up: Quantification and QPROP Previous: Subsearch and quantification
Matt Ginsberg 2004-02-19