15.5.3 Propositional Logic

We illustrate the usage of disjunctive propagators at an example for propositional logics. We would like to solve the following propositional logics formula:

$\begin{array}{lc@{\vee}c} & A_1 & \neg A_2 \\ \wedge & \neg A_1 & A_2 \end{array}$

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.

<Disjunctive Propagators (Unit Progagation)>=: 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.

<Solve the 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}