6.3.2 Solve

Explanation of the solve/2 predicate.

solveConstraint.pl: View Download

The main predicate of our constraint solver is solve/2 (to be found in solveConstraint.pl). This predicate is a straightforward implementation of the enumeration algorithm from Section 6.2.3. It takes a constraint graph as its first argument, and returns the list of its solved forms in the second argument. Our solve/2-predicate calls some low-level predicates that implement normalization and distribution. We will define these predicates later.

The predicate solve/2 itself consists of three clauses. Its first clause handles the case of a constraint graph that still contain one or more nodes with two incoming dominance edges. It normalizes the input graph, and then calls distribute/3 to select one such node and compute the two constraints with the additional dominance edge (hence it corresponds to the Choice Rule discussed above). Then it calls itself recursively, once for each of the two alternatives, and appends the two lists of solved forms thus obtained.

solve(Usr,Solutions) :-
        normalize(Usr,NormalUsr),
        distribute(NormalUsr,Dist1,Dist2),
        solve(Dist1,Solutions1),
        solve(Dist2,Solutions2),
        append(Solutions1,Solutions2,Solutions).

cllsLib.pl: View Download

The second clause takes care of the base case, a constraint graph in which no node has two incoming dominance edges. It is used only if the call to distribute/3 in the first clause fails (as we shall see shortly, normalize/2 can never fail). Such a graph is a solved form iff it has no cycles, which we check with the predicate hasCycle/1 (from cllsLib.pl).

solve(Usr,[NormalUsr]) :-
        normalize(Usr,NormalUsr),
        \+ hasCycle(NormalUsr).

If the constraint graph does have a cycle, the second clause will fail as well. In this case, the following final clause applies. It simply returns an empty list of solved forms. We can't just let it fail because in that case, the entire original call of solve/2 would fail. This is wrong in general because it's very possible that the original constraint has solutions, but we have made some wrong choices along the way that have made our current graph unsatisfiable.

solve(_Usr,[]).

?- Question!

Look at the implementation of hasCycle/1 in cllsLib.pl and explain in your own words how this test works.


Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)