SCIENCE CHINA Information Sciences, Volume 61, Issue 11: 112101(2018) https://doi.org/10.1007/s11432-017-9273-5

Efficient zonal diagnosis with maximum satisfiability

More info
  • ReceivedJul 11, 2017
  • AcceptedSep 27, 2017
  • PublishedMay 18, 2018


Model-based diagnosis (MBD) has been widely acknowledged as an effective diagnosis paradigm. However, for large scale circuits, it is difficult to find all cardinality-minimal diagnoses within a reasonable time. This paper proposes a novel method that takes a significant step in this direction. The idea is to divide a circuit into zones and compute the cardinality-minimal diagnoses by finding subset-minimal diagnoses with cardinality-minimal via a maximum satisfiability (MaxSAT) solver on an abstracted circuit that is composed of these zones instead of all components. We also propose a new propagate-extend method for extending the seed-TLDs to obtain all cardinality-minimal diagnoses efficiently. We implement our method with a state-of-the-art core-guided MaxSAT solver, and present evidence that it significantly improves the diagnosis efficiency on ISCAS-85 circuits. Our method outperforms SATbD, which was recently shown to outperform most complete MBD approaches using satisfiability (SAT).


[1] Console L, Dressler O. Model-based diagnosis in the real world: lessons learned and challenges remaining. In: Proceedings of the 16th International Joint Conference on Artificial Intelligence, Stockholm, 1999. 1393--1400. Google Scholar

[2] Xu K, Li W. Many hard examples in exact phase transitions. Theory Comput Sci, 2006, 355: 291-302 CrossRef Google Scholar

[3] Wang Y Y, Ouyang D T, Zhang L M. A novel local search for unicost set covering problem using hyperedge configuration checking and weight diversity. Sci China Inf Sci, 2017, 60: 062103 CrossRef Google Scholar

[4] Gao J, Wang J N, Yin M H. Experimental analyses on phase transitions in compiling satisfiability problems. Sci China Inf Sci, 2015, 58: 032104 CrossRef Google Scholar

[5] Geng X N, Ouyang D T, Zhang Y G. Model-based diagnosis of incomplete discrete-event system with rough set theory. Sci China Inf Sci, 2017, 60: 012205 CrossRef Google Scholar

[6] Wang X Y, Jiang S J, Gao P F. Cost-effective testing based fault localization with distance based test-suite reduction. Sci China Inf Sci, 2017, 60: 092112 CrossRef Google Scholar

[7] Zhou J P, Yin M H, Li X T. Phase transitions of expspace-complete problems: a further step. Int J Found Comput Sci, 2012, 23: 173-184 CrossRef Google Scholar

[8] de Kleer J, Mackworth A K, Reiter R. Characterizing diagnoses and systems. Artif Intel, 1992, 56: 197-222 CrossRef Google Scholar

[9] De K J. US Patent, 9563525, 2017-02-07. Google Scholar

[10] Jannach D, Schmitz T, Shchekotykhin K. Parallelized hitting set computation for model-based diagnosis. In: Proceedings of the 29th AAAI Conference on Artificial Intelligence, Austin, 2015. 1503--1510. Google Scholar

[11] Williams B C, Ragno R J. Conflict-directed A* and its role in model-based embedded systems. Discrete Appl Math, 2007, 155: 1562-1595 CrossRef Google Scholar

[12] Feldman A, Provan G, de Kleer J, et al. Solving model-based diagnosis problems with max-sat solvers and vice versa. In: Proceedings of the 21th International Workshop on Principles of Diagnosis, Portland, 2010. 185--192. Google Scholar

[13] Metodi A, Stern R, Kalech M, et al. Compiling model-based diagnosis to boolean satisfaction. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Toronto, 2012. 793--799. Google Scholar

[14] Metodi A, Stern R, Kalech M. A Novel SAT-Based Approach to Model Based Diagnosis. jair, 2014, 51: 377-411 CrossRef Google Scholar

[15] Zhang J, Ma F F, Zhang Z Q. Faulty interaction identification via constraint solving and optimization. In: Proceedings of the 15th Theory and Applications of Satisfiability Testing, Trento, 2012. 186--199. Google Scholar

[16] Darwiche A. Decomposable negation normal form. J ACM, 2001, 48: 608-647 CrossRef Google Scholar

[17] Siddiqi S, Huang J B. Hierarchical diagnosis of multiple faults. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, 2007. 581--586. Google Scholar

[18] Stern R, Kalech M, Feldman A, et al. Exploring the duality in conflict-directed model-based diagnosis. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Toronto, 2012. 828--834. Google Scholar

[19] Smith A, Veneris A, Ali M F. Fault diagnosis and logic debugging using Boolean satisfiability. IEEE Trans Comput-Aided Design, 2005, 24: 1606-1621 CrossRef Google Scholar

[20] Mangassarian H, Veneris A, Safarpour S, et al. A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test. In: Proceedings of the 26th International Conference on Computer-Aided Design, San Jose, 2007. 240--245. Google Scholar

[21] Suelflow A, Fey G, Bloem R, et al. Using unsatisfiable cores to debug multiple design errors. In: Proceedings of the 18th ACM Great Lakes Symposium on VLSI, Orlando, 2008. 77--82. Google Scholar

[22] Safarpour S, Veneris A. Abstraction and refinement techniques in automated design debugging. In: Proceedings of the 10th Design, Automation and Test in Europe Conference and Exhibition, Nice, 2007. 1182--1187. Google Scholar

[23] Gao J, Li R Z, Yin M H. A randomized diversification strategy for solving satisfiability problem with long clauses. Sci China Inf Sci, 2017, 60: 092109 CrossRef Google Scholar

[24] Liu J, Xu K. A novel weighting scheme for random k-SAT. Sci China Inf Sci, 2016, 59: 092101 CrossRef Google Scholar

[25] Safarpour S, Mangassarian H, Veneris A, et al. Improved design debugging using maximum satisfiability. In: Proceedings of the 7th Formal Methods in Computer Aided Design, Austin, 2007. 13--19. Google Scholar

[26] Kutsuna T, Sato S, Chujo N. Diagnosing automotive control systems using abstract model-based diagnosis. In: Proceedings of the 20th International Workshop on Principles of Diagnosis, Stockholm, 2009. 99--105. Google Scholar

[27] Chen Y B, Safarpour S, Veneris A, et al. Spatial and temporal design debug using partial MaxSAT. In: Proceedings of the 19th ACM Great Lakes Symposium on VLSI, Boston Area, 2009. 345--350. Google Scholar

[28] Cai S W, Luo C, Thornton J, et al. Tailoring local search for partial MaxSAT. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence, Quebec, 2014. 2623--2629. Google Scholar

[29] Marques-Silva J, Janota M, Ignatiev A, et al. Efficient model based diagnosis with maximum satisfiability. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence, Buenos Aires, 2015. 1966--1972. Google Scholar

[30] Kirkland T, Mercer M. A topological search algorithm for ATPG. In: Proceedings of the 24th ACM/IEEE Design Automation Conference, Miami Beach, 1987. 502--508. Google Scholar

[31] Huang J B, Darwiche A. On compiling system models for faster and more scalable diagnosis. In: Proceedings of the 20th National Conference on Artificial Intelligence, London, 2005. 300--306. Google Scholar

[32] Reiter R. A theory of diagnosis from first principles. Artif Intel, 1987, 32: 57-95 CrossRef Google Scholar

[33] de Kleer J, Williams B C. Diagnosing multiple faults. Artif Intel, 1987, 32: 97-130 CrossRef Google Scholar

[34] Siddiqi S. Computing minimum-cardinality diagnoses by model relaxation. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, Barcelona, 2011. 1087--1092. Google Scholar

[35] Martins R, Joshi S, Manquinho V, et al. Incremental cardinality constraints for MaxSAT. In: Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming, Lyon, 2014. 531--548. Google Scholar

[36] Nica I, Pill I, Quaritsch T, et al. The route to success-a performance comparison of diagnosis algorithms. In: Proceedings of the 22th International Joint Conference on Artificial Intelligence, Beijing, 2013. 1039--1045. Google Scholar

  • Figure 1

    Example circuit, where seed-components are indicted by circles and zones are indicated by rectangles.

    Previous MBD to MaxSAT method (SD,Comps,Obs)
    1 FindDominator()
    2 CircuitAbstraction()
    3 ObtainTLDbyMaxSAT()

    Algorithm 1 ZD: zonal diagnosis algorithm (SD, Obs)

    Require:SD, Obs;

    Output:$D$: set of cardinality-minimal diagnosis.

    $C$ $\leftarrow$ Components(SD);

    Out $\leftarrow$ Outputs(Obs, SD); # find system outputs and each component outputs

    SeedC $\leftarrow$ FindSeedComponents($C$, Out);

    Zones $\leftarrow$ GetZones($C$, Out, SeedC);

    $P$ $\leftarrow$ Model(Zones, SD);

    STLDs $\leftarrow$ GetSeedTLDs($P$, $C$, SeedC);

    $D$ $\leftarrow~\emptyset$;

    STLD $\leftarrow$ GetOneSTLD(STLDs);

    while true do

    if all STLD $\in$ STLDs are visited then



    $D$ $\leftarrow$ $D$ $\cup$ Extend(STLD);

    STLD $\leftarrow$ NextSTLD(STLDs);

    end if

    end while

    Previous TLD expansion process (TLD)
    1 ObtainSubCircuitDiagnoses(Dominator in TLD) or ObtainDominatedComponent(Dominator in TLD)
    2 IterationEnumerationReplaceTLD(SubCircuitDiagnoses) or IterationEnumerationReplaceTLD(DominatedComponent)
    3 CheckConsistency(each extended TLD)

    Algorithm 2 GSTLDs: GetSeedTLDs($P$,$C$,SeedC) # obtain seed-TLDs in order of cardinality and discard those diagnoses that are not cardinality-minimal

    Require:$P$: file of CNF, $C$, SeedC: set of components;

    Output:STLDs: set of seed-TLDs.

    SCs $\leftarrow$ SoftClauses(SeedC);

    HCs $\leftarrow$ HardClauses($C~\backslash~{\rm~SeedC}$);

    HCs $\leftarrow$ HCs $\cup$ HardClauses($P$);

    $W$ $\leftarrow$ HCs $\cup$ SCs;

    STLDs $\leftarrow~\emptyset$;

    while STLD $\leftarrow$ MaxSAT($W$) do

    $W~\leftarrow~W$ $\cup$ ($\infty$, $\neg$STLD); # avoid repetitive solutions;

    STLDs $\leftarrow$ STLDs $\cup$ STLD;

    end while

    Circuit Components Hierarchical diagnosis ZD
    Health vars Reduce (%) Zones Reduce (%)
    c432 160 59 63.1 65 59.4
    c499 202 58 71.3 66 67.3
    c880 383 77 79.9 132 65.5
    c1355 546 58 70.3 266 51.3
    c1908 880 160 57.5 392 55.5
    c2670 1193 167 86.0 399 66.6

    Algorithm 3 Extend(STLD)

    Require:STLD: set of components;

    Output:ETLDs: set of extended seed-TLDs.

    Comp $\leftarrow$ GetOneComp(STLD); # the Comp is a seed-component

    while true do

    if all Comp $\in$ STLD are visited then



    SeedComp $\leftarrow$ Comp;

    ETLD $\leftarrow$ PropagateExtend(SeedComp,Comp); # the first Comp is to retain the seed-component in each iteration of PropagateExtend

    ETLDs $\leftarrow$ ETLDs $\cup$ ETLD;

    Comp $\leftarrow$ NextComp(STLD);

    end if

    end while

    Circuit Diagnosis number $\leq$ 10 Diagnosis number $\leq$ 100
    c432 0 0.04 0 0.18 0.21 0.06
    c499 0.01 0.05 0 0.16 0.36 0
    c880 0.02 0.02 0 0.08 0.49 0.09
    c1355 0.05 0.11 0 0.09 0.96 0.08
    c1908 0.34 0.26 0.02 0.64 1.76 0.41
    c2670 0.24 0.47 0.07 0.74 4.46 0.71
    Diagnosis number $\leq$ 1000 Diagnosis number $\leq$ 10000
    c432 0.24 0.54 0.27 0.42 1.41 0.31
    c499 0.74 1.01 0.41 1.74 1.84 0.95
    c880 0.42 1.41 0.27 1.46 2.97 0.93
    c1355 0.57 1.52 0.45 1.82 6.85 1.02
    c1908 0.84 3.11 0.90 3.33 12.75 2.98
    c2670 1.32 10.87 1.09 7.65 36.49 4.96

    a) Bold: the winner for each scenario.


    Algorithm 4 PropagateExtend: diagnosis of zone (SeedComp,Comp)


    the later steps (lines 10–26) will be passed when we want cardinality-minimal diagnoses

    Require:SeedComp: a seed-component, Comp: a component;

    Output:ZDiag: set of cardinality-minimal/subset-minimal diagnosis.

    if HasFaninComp(Comp) = true then

    if Comp has no sensitive inputs then

    FIComp $\leftarrow$ GetOneNonSensitiveFIComp(Comp);

    if flipping the value of FIComp can make the output of SeedComp opposite with its expected value then

    ZDiag $\leftarrow$ ZDiag $\cup$ FIComp;

    FIZDiag $\leftarrow$ PropagateExtend(SeedComp,FIComp);

    ZDiag $\leftarrow$ ZDiag $\cup$ FIZDiag;

    FIComp $\leftarrow$ NextSensitiveFIComp(Comp);

    end if

Copyright 2019 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有