|Did you know ...||Search Documentation:|
|Example: Boolean circuit|
Consider a Boolean circuit that express the Boolean function
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
XOR as intended:
?- xor(x, y, Z). sat(Z=:=x#y).