[Rule] 3-Satisfiability to Fault Detection in Logic Circuits

[isPANN]

Source: 3-Satisfiability (3SAT)
Target: Fault Detection in Logic Circuits

Motivation: Establishes NP-completeness of fault detection (testability) in combinational logic circuits by encoding a 3SAT instance as a circuit where detecting a specific stuck-at fault is equivalent to finding a satisfying assignment. The key insight is that a circuit can be constructed from a 3SAT formula such that a stuck-at-1 fault on a particular line is detectable if and only if there exists an input that makes the formula true. This connects propositional satisfiability to hardware testing.
Reference: Garey & Johnson, Computers and Intractability, A1.2 MS17; Ibarra and Sahni 1975

GJ Source Entry

[MS17] FAULT DETECTION IN LOGIC CIRCUITS
INSTANCE: Logic circuit C (a dag of AND, OR, NOT gates), subset V' ⊆ V of vertices of C.
QUESTION: Can all "single stuck-at faults" on lines corresponding to members of V' be "detected"?
Reference: [Ibarra and Sahni, 1975]. Transformation from 3-SATISFIABILITY.
Comment: NP-complete even if V' = V or V' is a single input vertex.

Reduction Algorithm

Summary:
Given a 3SAT instance with variables x_1, ..., x_n and clauses C_1, ..., C_m (each clause has exactly 3 literals), construct a Fault Detection instance as follows:

1. Circuit construction: Build a combinational circuit C that computes the 3SAT formula directly:

   • Create n primary input lines for variables x_1, ..., x_n.
   • For each negated literal ¬x_i used in the formula, add a NOT gate.
   • For each clause C_j = (l_1 ∨ l_2 ∨ l_3), create a 3-input OR gate (or a tree of 2-input OR gates) taking the three literal signals.
   • Create a final AND gate (or tree of AND gates) combining all m clause outputs to produce the circuit output. The output is 1 iff all clauses are satisfied.

2. Fault vertex selection: The specific construction of Ibarra and Sahni places the fault at a carefully chosen line. For the simplest version: set V' to contain a single line — the output of the final AND gate, with stuck-at-0 fault. This fault is detectable iff there exists an input making the output 1, which is exactly SAT.

   More precisely: a stuck-at-0 fault on the output line is detected by any input that makes the fault-free output = 1 (since the faulty output is stuck at 0). So the fault is detectable iff the formula is satisfiable.

3. Correctness (forward): If the 3SAT formula is satisfiable with assignment τ, then input τ makes the circuit output 1 (fault-free). Under stuck-at-0 on the output, the faulty output is 0 ≠ 1. So the fault is detected.

4. Correctness (reverse): If the stuck-at-0 fault on the output is detectable, there exists an input making the fault-free output 1, meaning the formula is satisfiable under that input.

5. Solution extraction: The detecting test pattern is exactly a satisfying assignment for the 3SAT formula.

Key invariant: The circuit computes the conjunction of all clause disjunctions. A stuck-at-0 fault on the circuit output is detectable iff the formula is satisfiable.

Time complexity of reduction: O(n + m) gates and wires (linear in formula size).

Size Overhead

Symbols:

• n = num_variables of source 3SAT instance
• m = num_clauses of source 3SAT instance

Target metric (code name)	Polynomial (using symbols above)
num_inputs	num_variables
num_gates	O(num_variables + num_clauses)
num_fault_vertices	1 (or num_gates + num_inputs for V'=V variant)

Derivation: n input lines, at most n NOT gates, m OR gates (each with 2-3 inputs), and O(m) AND gates for the conjunction tree. Total gates: O(n + m). For the V' = {output} variant, only 1 fault vertex.

Validation Method

• Closed-loop test: construct a 3SAT instance, reduce to Fault Detection, check that fault detectability on the target circuit matches satisfiability of the source formula.
• Test with a known satisfiable 3SAT instance: (x1 ∨ x2 ∨ x3). Verify the stuck-at-0 fault on the output is detectable (e.g., input x1=1, x2=0, x3=0 detects it).
• Test with a known unsatisfiable instance: (x1) ∧ (¬x1) — no input makes output 1, so stuck-at-0 on output is undetectable. Verify NO.
• Verify circuit structure: check gate count matches formula size, check that circuit output matches formula evaluation for all 2^n inputs.

Example

Source instance (3SAT):
Variables: x_1, x_2, x_3
Clauses: C_1 = (x_1 ∨ ¬x_2 ∨ x_3), C_2 = (¬x_1 ∨ x_2 ∨ ¬x_3)
Satisfying assignment: x_1=1, x_2=1, x_3=0 → C_1 = (1 ∨ 0 ∨ 0) = 1, C_2 = (0 ∨ 1 ∨ 1) = 1.

Constructed target instance (Fault Detection):
Circuit:

• Inputs: x_1, x_2, x_3
• NOT gates: g_1 = NOT x_2, g_2 = NOT x_1, g_3 = NOT x_3
• OR gates: g_4 = x_1 OR g_1 OR x_3 (clause C_1), g_5 = g_2 OR x_2 OR g_3 (clause C_2)
• AND gate: g_6 = g_4 AND g_5 (output)
• Total: 3 inputs, 3 NOT gates, 2 OR gates, 1 AND gate = 6 gates
• V' = {g_6} (output line, stuck-at-0)

Solution mapping:

• Test input (1, 1, 0):
  • g_1 = NOT 1 = 0, g_2 = NOT 1 = 0, g_3 = NOT 0 = 1
  • g_4 = 1 OR 0 OR 0 = 1 (clause C_1 satisfied)
  • g_5 = 0 OR 1 OR 1 = 1 (clause C_2 satisfied)
  • g_6 = 1 AND 1 = 1 (fault-free output)
  • Under stuck-at-0 on g_6: faulty output = 0 ≠ 1
  • Fault detected ✓
• Extracted satisfying assignment: x_1=1, x_2=1, x_3=0 ✓

References

• [Ibarra and Sahni, 1975]: O. H. Ibarra and S. Sahni (1975). "Polynomially complete fault detection problems." IEEE Transactions on Computers C-24(3), pp. 242-249.
• [Garey and Johnson, 1979]: M. R. Garey and D. S. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, pp. 227 (MS17).