Node:CLPB Example 4, Previous:CLPB Example 3, Up:CLPB Examples

The predicate `fault/3`

below describes a 1-bit adder
consisting of five gates, with at most one faulty gate. If one of the
variables `Fi`

is equal to 1, the corresponding gate is
faulty, and its output signal is undefined (i.e. the constraint
representing the gate is relaxed).

Assuming that we have found some incorrect output from a circuit, we
are interesting in finding the faulty gate. Two instances of incorrect
output are listed in `fault_ex/2`

:

fault([F1,F2,F3,F4,F5], [X,Y,Cin], [Sum,Cout]) :- sat( card([0-1],[F1,F2,F3,F4,F5]) * (F1 + (U1 =:= X * Cin)) * (F2 + (U2 =:= Y * U3)) * (F3 + (Cout =:= U1 + U2)) * (F4 + (U3 =:= X # Cin)) * (F5 + (Sum =:= Y # U3)) ). fault_ex(1, Faults) :- fault(Faults, [1,1,0], [1,0]). fault_ex(2, Faults) :- fault(Faults, [1,0,1], [0,0]).

To find the faulty gates, we run the query

| ?-fault_ex(I,L), labeling(L).I = 1, L = [0,0,0,1,0] ?;I = 2, L = [1,0,0,0,0] ?;I = 2, L = [0,0,1,0,0] ?;no

Thus for input data `[1,1,0]`

, gate 4 must be faulty.
For input data `[1,0,1]`

, either gate 1 or gate 3 must be faulty.

To get a symbolic representation of the outputs interms of the input, we
run the query

| ?-fault([0,0,0,0,0], [x,y,cin], [Sum,Cout]).sat(Cout=:=x*cin#x*y#y*cin), sat(Sum=:=cin#x#y)

which shows that the sum and carry out signals indeed compute the intended functions if no gate is faulty.