Little Solver

We present a sketch on how a little custom constraint solver can be implemented via forward chaining rules. The basic idea of the sketch can be used as a boiler plate to implement various constraint solvers. But more able and efficient solvers probably need additional ideas. Our little solver will allow elementary reasoning for the following constraints:

X = c ,    c is a number
X ∈ D ,    D is a finite set of numbers

Our little solver will use atoms to represent constraint variables. Many existing Prolog systems use Prolog variables to represent constraint variables. We might also do so in the future, but atoms are currently easier to deal with in forward chaining rules. We will represent the constraints by forward facts. The forward chaining rules will implement the desired elementary reasoning

We start with the rules for the X = c constraints. The constraint will be represented by bound/2 forward facts. We find only two rules:

X = c, X = c →    X = c
X = c, X = d →    ⊥ ,    c ≠ d

To implement these rules we will need to draw upon all features of our forward chaining en-gine. In particular we will make use of the condition annotations posted/1, phaseout/1 and phaseout_posted/1. We will also make use of the actions true/0 and fail/0. In the first rule we need an arrival and delete phaseout_posted/1 annotation since two equalities are replaced by a single equality. In the second rule we need a fail since the result is bottom. We also make use of the cut (!):

:- multifile bound/2.
:- thread_local bound/2.

true <=
phaseout_posted(bound(X, C)), bound(X, C), !.
fail <=
posted(bound(X, _)), bound(X, _).

Let’s turn to the rules for the X ∈ D constraints. The constraint will be represented by domain/2 forward facts. We find rules that transform a domain/2, that combine a domain/2 with a bound/2 and that combine a domain/2 with another domain/2:

X ∈ {} →    ⊥
X ∈ {c} →    X = c
X ∈ D, X = c →    X = c ,    c ∈ D
X ∈ D, X = c →    ⊥ ,    c ∉ D
X ∈ D, X ∈ E →    X ∈ D ∩ E

The above rules need additional computations. The rules that combine a domain/2 and a bound/2 will make use of a member/2 predicate to check the member ship (∈). The rules that combine a domain/2 with another domain/2 will make use of an intersection/2 predicate to compute the set intersection (∩). The implementation of these predicates is drawn from some standard modules. The forward rules read as follows:

:- multifile domain/2.
:- thread_local domain/2.

fail <=
posted(domain(_, [])), !.
post(bound(X, C)) <=
phaseout_posted(domain(X, [C])), !.
true <=
phaseout_posted(domain(X, D)), posted(bound(X, C)),
member(C, D), !.
fail <=
posted(domain(X, _)), posted(bound(X, _)).
post(domain(X, F)) <=
phaseout_posted(domain(X, D)), phaseout(domain(X, E)),
intersection(D, E, F).

The forward store and thus constraint store can be inspected with the predicate listing/1. The forward chaining can be triggered via the predicate post/1. Let’s run some tests:

?- post(domain(x,[1])), listing(bound/2), listing(domain/2).
bound(x, 1).

?- post(domain(x,[1,2,3])), post(domain(y,[2,3,4])),
listing(bound/2), listing(domain/2).
domain(x, [1,2,3]).
domain(y, [2,3,4]).

?- post(domain(x,[1,2,3])), post(domain(x,[2,3,4])),
listing(bound/2), listing(domain/2).
domain(x, [2,3]).

?- post(domain(x,[1,2,3])), post(bound(x,4)),
listing(bound/2), listing(domain/2).
No

Kommentare