<< Prev | - Up - | Next >> |
We illustrate the usage of disjunctive propagators at an example for propositional logics. We would like to solve the following propositional logics formula:
The variables denote Boolean values that we represent by 0 and 1. We would like to enumerate all solutions of the above formula. We would like the following propogation rules to apply (unit propagation):
If A1=0
then A2=0
. If A1=1
then A2=1
.
We can define the following propagators to achieve this behaviour.
thread or A1=1 [] A2=0 end end
thread or A1=0 [] A2=1 end end
If A1=0
is imposed then the first clause of the first propagator gets removed since its guard becomes inconsistent with the global store. Only the second clause remains. Thus the first propagator commits to its second clause and thereby adds the constraint A2=0
to the global store.
Impose A1=1
has a symmetric effect. The first clause of the second propagator gets removed since its guard becomes inconsistent. Only its second clause remains such that the second propagator commits to its second clause. Thereby A2=1
is imposed globally.
Note that each of the or-statement propagators has to run in its own thread. Otherwise the first stated or-statement would block the exectution of the second or-statement.
We obain the following solver for the above propositional formula.
declare
proc{Predicate Sol}
A1 A2
Vars = [A1 A2]
Vars ::: 0#1
in
Sol = vars(a1:A1 a2:A2)
thread or A1=1 [] A2=0 end end
thread or A1=0 [] A2=1 end end
{FD.distribute naive [A1 A2]}
end
{Explorer.all Predicate}
<< Prev | - Up - | Next >> |