A.8.8 Example: Boolean circuit

Consider a Boolean circuit that express the Boolean function XOR with 4 NAND gates. We can model such a circuit with CLP(B) constraints as follows:

:- use_module(library(clpb)).

nand_gate(X, Y, Z) :- sat(Z =:= ~(X*Y)).

xor(X, Y, Z) :-
        nand_gate(X, Y, T1),
        nand_gate(X, T1, T2),
        nand_gate(Y, T1, T3),
        nand_gate(T2, T3, Z).

Using universally quantified variables, we can show that the circuit does compute XOR as intended:

?- xor(x, y, Z).
sat(Z=:=x#y).