A Novel Encoding for Model-Based Diagnosis
-
摘要:
基于模型诊断（model-based diagnosis，MBD）是人工智能诊断领域中著名的诊断求解方法之一，旨在识别诊断问题的根本原因.由于求解诊断解在计算上具有挑战性，一些MBD算法提出通过修改模型的编码来提高诊断效率，如面向统治者的编码（dominator-oriented encoding, DOE）方法.面向观察的编码（observation-oriented encoding，OOE）方法使用2种方法对MBD模型进行约简. 首先，利用系统观测和统治组件输出的一些过滤边来约简系统描述和观测.其次，通过查找基于观测的过滤节点来过滤更多的组件, 进而有效约简组件的编码规模. 此外，在ISCAS85和ITC99基准测试用例上的实验结果表明，与目前最新的MBD编码方法DOE和传统的基础编码（basic encoding , BE）相比，上述2种约简方法有效减少了MBD实例的编码子句数量比，降低MaxSAT求解器求解诊断的难度，进而能在更短的时间内返回一个诊断解.
Abstract:Model-based diagnosis (MBD), a well-known approach in the AI field, aims at identifying the root cause of a diagnosis problem. Since computing diagnosis is computationally challenging, some MBD algorithms by modifying the model encode are presented successively, such as Dominator-Oriented Encoding (DOE) approach. In this study, we propose a new encoding process, Observation-Oriented Encoding (OOE), which uses two ideas to simplify MBD model. Firstly, we consider more filtered edges based on observation of system and output of dominated components. This idea can reduce the number of encoded clauses for diagnosis system and observations. Secondly, more components are filtered by finding out observation-based filtered nodes. This approach reduces the number of encoded clauses for components. All of them can reduce the number of encoded clauses efficiently. Furthermore, experiment evaluations on ISCAS85 and ITC99 benchmarks, which contain well-known combinational circuits used for MBD algorithms, show that OOE approach generates less weighted conjunctive normal forms (WCNF) and makes diagnosis easier with maximum satisfiability (MaxSAT) solver, compared with DOE, the latest encoding algorithms for MBD, and Basic Encoding (BE), which is the traditional encoding approach for MBD. In addition, OOE approach returns a solution in a shorter time than DOE and BE approaches.
-
-
![]()
图 3 BE和OOE方法在ISCAS85实例上的运行时间比较
Figure 3. Comparison of the run time of BE and OOE approaches on ISCAS85 benchmark
![]()
图 4 DOE和OOE方法在ISCAS85实例上的运行时间比较
Figure 4. Comparison of the run time of DOE and OOE approaches on ISCAS85 benchmark
![]()
图 5 BE和OOE方法在ITC99实例上的运行时间比较
Figure 5. The run time of BE and OOE approaches on ITC99 benchmark
![]()
图 6 DOE和OOE方法在ITC99实例上的运行时间比较
Figure 6. The run time of DOE and OOE approaches on ITC99 benchmark
表 1 在ITC99实例上的求解结果
Table 1 Solved Results for ITC99 Benchmark
电路名称 观测个数 所用时间比竞争
对手短的实例个数所用时间比竞争
对手短的实例个数OOE BE OOE DOE[22] b14 919 433 164 569 2 b15 995 663 188 819 2 b17 1000 946 54 1000 0 b18 1000 884 46 917 2 b19 1000 823 56 833 42 b20 997 596 222 782 0 b21 919 636 166 780 0 b22 992 722 223 932 0 
下载: 导出CSV
表 2 在ISCAS85 实例上的求解结果
Table 2 Solved Results for ISCAS85 Benchmark
电路名称 观测个数 所用时间比竞争
对手短的实例个数所用时间比竞争
对手短的实例个数OOE BE OOE DOE[22] c17 63 48 14 56 7 c432 301 280 17 278 23 c499 835 734 96 760 71 c880 1182 1182 0 1157 20 c1355 836 719 113 832 4 c1908 864 664 182 834 12 c2670 1162 1128 34 1158 4 c3540 756 705 51 756 0 c5315 2038 2028 10 2038 0 c6288 404 246 158 398 6 c7552 1557 1536 21 1557 0
下载: 导出CSV
-
[1] Reiter R. A theory of diagnosis from first principles[J]. Artificial Intelligence, 1987, 32(1): 57−95 doi: 10.1016/0004-3702(87)90062-2
[2] Torlak E, Chang F S H, Jackson D. Finding minimal unsatisfiable cores of declarative specifications[C] //Proc of the 13th Int Symp on Formal Methods. Berlin: Springer, 2008: 326–341
[3] Safarpour S, Mangassarian H, Veneris A, et al. Improved design debugging using maximum satisfiability[C] //Proc of the 7th Formal Methods in Computer Aided Design. Piscataway, NJ: IEEE, 2007: 13–19
[4] Jannach D, Schmitz T. Model-based diagnosis of spreadsheet programs: A constraint-based debugging approach[J]. Automated Software Engineering, 2016, 23(1): 105−144 doi: 10.1007/s10515-014-0141-7
[5] Jose M, Majumdar R. Cause clue clauses: Error localization using maximum satisfiability[J]. ACM SIGPLAN Notices, 2011, 46(6): 437−446 doi: 10.1145/1993316.1993550
[6] Feldman A, Provan G M, Van Gemund A J C. Computing minimal diagnoses by greedy stochastic search[C] //Proc of the 23rd AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2008: 911–918
[7] Siddiqi S A, Huang Jinbo. Hierarchical diagnosis of multiple faults[C] //Proc of the 20th Int Joint Conf on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 2007: 581–586
[8] Jannach D, Schmitz T, Shchekotykhin K M. Parallelized hitting set computation for model-based diagnosis[C] //Proc of the 29th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2015: 1503–1510
[9] Ansótegui C, Bonet M L, Levy J. SAT-based MaxSAT algorithms[J]. Artificial Intelligence, 2013, 196: 77–105
[10] Feldman A, Provan G, de Kleer J. Solving model-based diagnosis problems with Max-SAT solvers and vice versa[C] //Proc of the 21st Int Workshop on Principles of Diagnosis. New York: PHM Society, 2010: 185–192
[11] Stern R T, Kalech M, Feldman A. Exploring the duality in conflict-directed model-based diagnosis[C] //Proc of the 26th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2012: 828–834
[12] Lamraoui S M, Nakajima S. A formula-based approach for automatic fault localization of imperative programs[C] //Proc of the 19th Int Conf on Formal Engineering Methods. Berlin: Springer, 2014: 251–266
[13] Lamraoui S M, Nakajima S. A formula-based approach for automatic fault localization of multi-fault programs[J]. Journal of Information Processing, 2016, 24(1): 88−98 doi: 10.2197/ipsjjip.24.88
[14] Ignatiev A, Morgado A, Weissenbacher G. Model-based diagnosis with multiple observations[C] //Proc of the 28th Int Joint Conf on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 2019: 1108–1115
[15] Ignatiev A, Morgado A, Marques-Silva J. Model based diagnosis of multiple observations with implicit hitting sets[J]. arXiv preprint, arXiv: 1707.01972, 2017
[16] Feldman A, Provan G, Van Gemund A. Approximate model-based diagnosis using greedy stochastic search[J]. Journal of Artificial Intelligence Research, 2010, 38: 371–413
[17] Williams B C, Ragno R J. Conflict-directed A* and its role in model-based embedded systems[J]. Discrete Applied Mathematics, 2007, 155(12): 1562−159 doi: 10.1016/j.dam.2005.10.022
[18] Darwiche A. Decomposable negation normal form[J]. Journal of the ACM, 2001, 48(4): 608−647 doi: 10.1145/502090.502091
[19] Piotrów M. UwrMaxSAT: Efficient solver for MaxSAT and Pseudo-Boolean problems[C] //Proc of the 32nd Int Conf on Tools with Artificial Intelligence. Piscataway, NJ: IEEE, 2020: 132–136
[20] Metodi A, Stern R, Kalech M, et al. A novel SAT-based approach to model based diagnosis[J]. Journal of Artificial Intelligence Research, 2014, 51: 377–411
[21] De Kleer J. Hitting set algorithms for model-based diagnosis[C] //Proc of the 22nd Int Workshop on Priciples of Diagnosis. New York: PHM Society, 2011: 100–105
[22] Marques-Silva J, Janota M, Ignatiev A, et al. Efficient model based diagnosis with maximum satisfiability[C] //Proc of the 24th Int Joint Conf on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 2015: 1966–1972
[23] 刘梦,欧阳丹彤,刘伯文,等. 结合问题特征的分组式诊断方法[J]. 电子学报,2018,46(3):589−594 doi: 10.3969/j.issn.0372-2112.2018.03.011 Liu Meng, Ouyang Dantong, Liu Bowen, et al. Grouped diagnosis approach using the feature of problem[J]. Acta Elecronica Sinica, 2018, 46(3): 589−594 (in Chinese) doi: 10.3969/j.issn.0372-2112.2018.03.011
[24] 欧阳丹彤,刘伯文,刘梦,等. 结合电路结构基于分块的诊断方法[J]. 电子学报,2018,46(7):1571−1577 doi: 10.3969/j.issn.0372-2112.2018.07.005 Ouyang Dantong, Liu Bowen, Liu Meng, et al. A block-based diagnostic method combining with the circuit structure[J]. Acta Elecronica Sinica, 2018, 46(7): 1571−1577 (in Chinese) doi: 10.3969/j.issn.0372-2112.2018.07.005
计量
- 文章访问数: 223
- HTML全文浏览量: 18
- PDF下载量: 110
