Link Search Menu Expand Document
PyCSP3
Models & Data GitHub XCSP3 About
Documentation
XCSP web site is provided by CRIL
This site uses Just the Docs, a documentation theme for Jekyll.
download notebook
COP  difficult 

Problem Diagnosis

From CSPLib (Problem 42): Model-based diagnosis can be seen as taking as input a partially parameterized structural description of a system and a set of observations about that system. Its output is a set of assumptions which, together with the structural description, logically imply the observations, or that are consistent with the observations. Diagnosis is usually applied to combinational digital circuits, seen as black-boxes where there is a set of controllable input bits but only a set of primary outputs is visible. The problem is to find the set of all (minimal) internal faults that explain an incorrect output (different than the modelled, predicted, output), given some input vector. The possible faults consider the usual stuck-at fault model, where faulty circuit gates can be either stuck-at-0 or stuck-at-1, respectively outputting value 0 or 1 independently of the input.

As an example, for the full-adder circuit displayed below, if we assume that the input is A=0, B=0, C${in}$=0 and the observed output is S=1, C${out}$=0 (although it should be S=0, C$_{out}$=0), the single faults that explain the incorrect output are the first XOR gate stuck-at-1 or the second XOR gate stuck-at-1.

Image from commons.wikimedia Adder

To build a COP (Constraint Optimization Problem) model, we need first to import the library PyCSP$^3$:

from pycsp3 import *

Then, we need some data. Here, we need to describe the functions and the gates (we use named tuples to represent them).

f_or = [
    [0,1],
    [1,1]
]
f_and = [
    [0,0],
    [0,1]
]
f_xor = [
    [0,1],
    [1,0]
]
functions = cp_array([f_or, f_and, f_xor])

Gate = namedtuple('Gate', 'f in1 in2 out')
gates = [None, None, Gate(2,0,0,-1), Gate(1,0,0,-1), Gate(2,0,2,1), Gate(1,0,2,-1), Gate(0,3,5,0)]
nGates = len(gates)

Logical functions are given under their matrix forms; here, we have successively the functions OR (index 0), AND (index 1), and XOR (index 2). Each gate is given its logical function (index given by ’f’), its two input (with 0 for false, 1 for true and the index of another gate otherwise), and its observed output (0 or 1 if any, -1 otherwise). Note that the two first gates are special; they are inserted (with None values) for reserving indexes 0 and 1 (for false and true).

Remark. Because it is not possible to use a special object as an index of a list of integers in Python (later, we need this when posting some constraints), we have to transform the lists of integers of the three functions into more specific lists with the function cp_array(). The good news is that when the data is loaded from a file (which is the usual case), all lists of integers have the specific type of list returned by cp_array(), and so, it is very rare to need to call this function explicitly.

print(gates)

[None, None, Gate(f=2, in1=0, in2=0, out=-1), Gate(f=1, in1=0, in2=0, out=-1), Gate(f=2, in1=0, in2=2, out=1), Gate(f=1, in1=0, in2=2, out=-1), Gate(f=0, in1=3, in2=5, out=0)]

We start our COP model by introducing a first array $x$ of variables. This will allow us to identify the faulty gates.

# x[i] is -1 if the ith gate is not faulty (otherwise 0 or 1 when stuck at 0 or 1)
x = VarArray(size=nGates, dom=lambda i: {-1} if i < 2 else {-1, 0, 1})

We can display the structure of the array, as well as the domain of the variables. Remember that the two first variables are very special (and so, cannot be faulty).

print("Array x: ", x)
for i in range(nGates):
    print(f"  Domain of {x[i]} is: {x[i].dom}")                        

Array x:  [x[0], x[1], x[2], x[3], x[4], x[5], x[6]]
  Domain of x[0] is: -1
  Domain of x[1] is: -1
  Domain of x[2] is: -1 0 1
  Domain of x[3] is: -1 0 1
  Domain of x[4] is: -1 0 1
  Domain of x[5] is: -1 0 1
  Domain of x[6] is: -1 0 1

We introduce a second array $y$ of variables to be able to reason with intermediate computations (outputs).

# y[i] is the (possibly faulty) output of the ith gate
y = VarArray(size=nGates, dom=lambda i: {i} if i < 2 else {0, 1})

Concerning the constraints, we have first to ensure that some variables of $y$ are coherent with respect to the observed output. Note that we could have directly integrated these unary constraints when defining the domain of variables of $y$. Here, we post a group of constraints Intension.

satisfy(
    # ensuring that y is coherent with the observed output
    y[i] == j for i in range(2, nGates) if (j:=gates[i].out) != -1
);

We can display the internal representation of the two posted constraints; this way, although a little bit technical, we can see that the two constraints are correctly formed (note that ‘eq’ stands for ‘equal to’).

print(posted())

intension(function:eq(y[4],1))
intension(function:eq(y[6],0))

For simulating the behaviour of a gate, we introduce the following function that involves a partial form of constraint ElementMatrix:

def apply(gate):
    return functions[gate.f][y[gate.in1]][y[gate.in2]]

We can now post a group of constraints Intension.

satisfy(
    # ensuring that each gate either meets expected outputs based on its function or is broken (stuck on or off)
    If(
        y[i] != x[i],
        Then=[
            y[i] == apply(gates[i]),
            x[i] == -1
        ]
    ) for i in range(2, nGates)
);

Note how we use the structure If for logically combining constraints. Another way of posting equivalent constraints is:

(y[i] == x[i]) | (y[i] == apply(gates[i])) & (x[i] == -1) for i in range(2, nGates)

The expression of these new constraints are rather complex. In order to remain in the perimeter of XCSP$^3$-core, some auxiliary variables, called aux_gb, are introduced automatically. We can then combine constraints Intension and ElementMatrix, as we can see when executing:

print(posted(-1))

intension(function:or(eq(y[2],x[2]),eq(aux_gb[0],y[2])))
intension(function:or(eq(y[2],x[2]),eq(x[2],-1)))
intension(function:or(eq(y[3],x[3]),eq(aux_gb[1],y[3])))
intension(function:or(eq(y[3],x[3]),eq(x[3],-1)))
intension(function:or(eq(y[4],x[4]),eq(aux_gb[2],y[4])))
intension(function:or(eq(y[4],x[4]),eq(x[4],-1)))
intension(function:or(eq(y[5],x[5]),eq(aux_gb[3],y[5])))
intension(function:or(eq(y[5],x[5]),eq(x[5],-1)))
intension(function:or(eq(y[6],x[6]),eq(aux_gb[4],y[6])))
intension(function:or(eq(y[6],x[6]),eq(x[6],-1)))
element(matrix:(0,1)(1,0), index:[y[0], y[0]], condition:(eq,aux_gb[0]))
element(matrix:(0,0)(0,1), index:[y[0], y[0]], condition:(eq,aux_gb[1]))
element(matrix:(0,1)(1,0), index:[y[0], y[2]], condition:(eq,aux_gb[2]))
element(matrix:(0,0)(0,1), index:[y[0], y[2]], condition:(eq,aux_gb[3]))
element(matrix:(0,1)(1,1), index:[y[3], y[5]], condition:(eq,aux_gb[4]))

Interestingly, by calling the function solve(), we can check that the problem is satisfiable (SAT). We can also display the found solution. Here, we call the function values() that collects the values assigned to a specified list of variables.

if solve() is SAT:
    print(values(x))

[*, *, -1, -1, 1, -1, -1]

Here, we have only one faulty gate. Anyway, in the general case, we want to be sure to have a minimal number of faulty gates. This can be written: 

minimize(
    # minimizing the number of faulty gates
    Sum(x[i] != -1 for i in range(2, nGates))
);

We can run again the solver, with this optimization task. Note that we need to check that the status returned by the solver is now OPTIMUM.

if solve() is OPTIMUM:
    print(values(x))
    print("Number of faulty gates: ", bound())
    print("Faulty gates: ", [i for i in range(2,nGates) if x[i].value != -1])

[*, *, -1, -1, 1, -1, -1]
Number of faulty gates:  1
Faulty gates:  [4]

Finally, we give below the model in one piece. Here the data is expected to be given by the user (in a command line).

from pycsp3 import *

functions, gates = data  # note that the two first gates are special, reserving indexes 0 and 1 (for false and true)
nGates = len(gates)

# x[i] is -1 if the ith gate is not faulty (otherwise 0 or 1 when stuck-at-0 or stuck-at-1)
x = VarArray(size=nGates, dom=lambda i: {-1} if i < 2 else {-1, 0, 1})

# y[i] is the (possibly faulty) output of the ith gate
y = VarArray(size=nGates, dom=lambda i: {i} if i < 2 else {0, 1})


def apply(gate):
    return functions[gate.f][y[gate.in1]][y[gate.in2]]


satisfy(
    # ensuring that y is coherent with the observed output
    [y[i] == j for i in range(2, nGates) if (j:=gates[i].out) != -1],

    # ensuring that each gate either meets expected outputs based on its function or is broken (stuck on or off)
    [
        If(
            y[i] != x[i],
            Then=[
                y[i] == apply(gates[i]),
                x[i] == -1
            ]
        ) for i in range(2, nGates)
    ]
)

minimize(
    # minimizing the number of faulty gates
    Sum(x[i] != -1 for i in range(2, nGates))
)