Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases.

*(English)*Zbl 1309.68181The article discusses and empirically evaluates various methods for computing minimal inconsistent subsets (MISs), a problem known to be intractable in the worst case. A connection between MISs and the related problem of minimal unsatisfiable sets of clauses (MUSs) is established, which allows the authors to explore the use of methods developed by the Boolean satisfiability community for computing MISs. An alternative algorithm for computing inconsistent subsets based on the existing Boolean satisfiability algorithms, is presented. A tool, called MIMUS, was developed to empirically evaluate the discussed algorithms. Experiments were performed on randomly generated knowledge bases. The total runtime of MINUS is analyzed in terms of the number of MISs. A set of measures to deal with inconsistencies for both flat and stratified knowledge bases is proposed. The authors advocate that these measures provide a practical and viable way for inconsistency handling. A review of related work in presented. The article contains multiple examples and a detailed description of MIMUS’s runtime performance.

Reviewer: Neli Zlatareva (New Britain, CT)

##### MSC:

68T35 | Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence |

68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |

68T30 | Knowledge representation |

##### Keywords:

inconsistency measures; minimal inconsistent subsets; minimal unsatisfiable subformulae; SAT; random SAT
PDF
BibTeX
XML
Cite

\textit{K. McAreavey} et al., Int. J. Approx. Reasoning 55, No. 8, 1659--1693 (2014; Zbl 1309.68181)

Full Text:
DOI

##### References:

[1] | Benferhat, Salem; Dubois, Didier; Prade, Henri, Argumentative inference in uncertain and inconsistent knowledge bases, (Proceedings of the 9th International Conference on Uncertainty in Artificial Intelligence, (1993)), 411-419 |

[2] | Belnap, Nuel, A useful four-valued logic, (Modern Uses of Multiple-Valued Logic, (1977)), 8-37 · Zbl 0424.03012 |

[3] | Besnard, Philippe; Grégoire, Éric; Piette, Cédric; Raddaoui, Badran, MUS-based generation of arguments and counter-arguments, (Proceedings of the 2010 IEEE International Conference on Information Reuse & Integration, (2010)), 239-244 |

[4] | Besnard, Philippe; Hunter, Anthony, Quasi-classical logic: non-trivializable classical reasoning from inconsistent information, (Symbolic and Quantitative Approaches to Uncertainty, LNCS, vol. 946, (1995)), 44-51 |

[5] | Belov, Anton; Järvisalo, Matti; Marques-Silva, João, Formula preprocessing in MUS extraction, (Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (2013)), 108-123 · Zbl 1381.68146 |

[6] | Birnbaum, Elazar; Lozinskii, Eliezer, Consistent subsets of inconsistent systems: structure and behaviour, J. Exp. Theor. Artif. Intell., 15, 1, 25-46, (2003) · Zbl 1025.68090 |

[7] | Brewka, Gerhard, Preferred subtheories: an extended logical framework for default reasoning a framework for nonmonotonic systems, (Proceedings of the 11th International Joint Conference on Artificial Intelligence, (1989)), 1043-1048 · Zbl 0713.68053 |

[8] | Bruni, Renato, Minimal unsatisfiable subformulae by means of adaptive core search, Discrete Appl. Math., 130, 2, 85-100, (2003) · Zbl 1029.68075 |

[9] | Barker, Steve; Stuckey, Peter, Flexible access control policy specification with constraint logic programming, ACM Trans. Inf. Syst. Secur., 6, 4, 501-546, (2003) |

[10] | Bailey, James; Stuckey, Peter, Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization, (Proceedings of the 7th International Conference on Practical Aspects of Declarative Languages, (2005)), 174-186 |

[11] | Cayrol, Claudette; Lagasquie-Schiex, Marie-Christine; Schiex, Thomas, Nonmonotonic reasoning: from complexity to algorithms, Ann. Math. Artif. Intell., 22, 3-4, 207-236, (1998) · Zbl 0905.68142 |

[12] | Coja-Oghlan, Amin; Frieze, Alan, Random k-SAT: the limiting probability for satisfiability for moderately growing k, Electron. J. Comb., 15, 1, N2, (2008) · Zbl 1163.68337 |

[13] | Dellert, Johannes, Interactive extraction of minimal unsatisfiable cores enhanced by meta learning, (2013), Eberhard Karls Universität Tübingen, Informatik diplom |

[14] | Di Rosa, Emanuele; Giunchiglia, Enrico; Maratea, Marco, Solving satisfiability problems with preferences, Constraints, 15, 4, 485-515, (2010) · Zbl 1208.68199 |

[15] | de Kleer, Johan; Williams, Brian, Diagnosing multiple faults, Artif. Intell., 32, 1, 97-130, (1987) · Zbl 0642.94045 |

[16] | Garcia de la Banda, Maria; Stuckey, Peter; Wazny, Jeremy, Finding all minimal unsatisfiable subsets, (Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, (2003)), 32-43 |

[17] | Eén, Niklas; Biere, Armin, Effective preprocessing in SAT through variable and clause elimination, (Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing, (2005)), 1-15 · Zbl 1128.68463 |

[18] | Eiter, Thomas; Gottlob, Georg, On the complexity of propositional knowledge base revision, updates, and counterfactuals, Artif. Intell., 57, 2-3, 227-270, (1992) · Zbl 0763.68038 |

[19] | Eén, Niklas; Sörensson, Niklas, An extensible SAT-solver, (Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, (2003)), 502-518 · Zbl 1204.68191 |

[20] | Fourdrinoy, Olivier; Grégoire, Éric; Mazure, Bertrand; Saïs, Lakhdar, Eliminating redundant clauses in SAT instances, (Proceedings of the 4th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, (2007)), 71-83 · Zbl 1214.68333 |

[21] | Flaxman, Abraham, Algorithms for random 3-SAT, (Encyclopedia of Algorithms, (2008)), 742-744 |

[22] | Franco, John; Martin, John, A history of satisfiability, (Biere, Armin; Heule, Marijn; van Maaren, Hans; Walsh, Toby, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, (2009), IOS Press), 3-76, (Chapter 1) |

[23] | Friedgut, Ehud, Sharp thresholds of graph properties, and the k-sat problem, J. Am. Math. Soc., 12, 4, 1017-1054, (1999) · Zbl 0932.05084 |

[24] | Felfernig, Alexander; Schubert, Monika; Zehentner, Christoph, An efficient diagnosis algorithm for inconsistent constraint sets, Artif. Intell. Eng. Des. Anal. Manuf., 26, 1, 53-62, (2011) |

[25] | Govaerts, John; Bandara, Arosha; Curran, Kevin, A formal logic approach to firewall packet filtering analysis and generation, Artif. Intell. Rev., 29, 3-4, 223-248, (2009) |

[26] | Grant, John; Hunter, Anthony, Measuring consistency gain and information loss in stepwise inconsistency resolution, (Proceedings of the 11th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, (2011)), 362-373 · Zbl 1341.68256 |

[27] | Grégoire, Éric; Mazure, Bertrand; Piette, Cédric, Local-search extraction of muses, Constraints, 12, 3, 325-344, (2007) · Zbl 1211.90307 |

[28] | Grégoire, Éric; Mazure, Bertrand; Piette, Cédric, Does this set of clauses overlap with at least one MUS?, (Automated Deduction - CADE-22, LNCS, vol. 5663, (2009)), 100-115 · Zbl 1250.68234 |

[29] | Grégoire, Éric; Mazure, Bertrand; Piette, Cédric, Using local search to find msses and muses, Eur. J. Oper. Res., 199, 3, 640-646, (2009) · Zbl 1176.90410 |

[30] | Grant, John, Classifications for inconsistent theories, Notre Dame J. Form. Log., 19, 3, 435-444, (1978) · Zbl 0305.02040 |

[31] | Hunter, Anthony; Konieczny, Sébastien, Approaches to measuring inconsistent information, (Inconsistency Tolerance, LNCS, vol. 3300, (2005)), 189-234 · Zbl 1111.68125 |

[32] | Hunter, Anthony; Konieczny, Sébastien, Measuring inconsistency through minimal inconsistent sets, (Proceedings of the 11th International Conference on Knowledge Representation, (2008)), 358-366 |

[33] | Hunter, Anthony; Konieczny, Sébastien, On the measure of conflicts: Shapley inconsistency values, Artif. Intell., 174, 14, 1007-1026, (2010) · Zbl 1210.68106 |

[34] | Hunter, Anthony, Measuring inconsistency in knowledge via quasi-classical models, (Proceedings of the 18th American National Conference on Artificial Intelligence, (2002)), 68-73 |

[35] | Hunter, Anthony, Logical comparison of inconsistent perspectives using scoring functions, Knowl. Inf. Syst., 6, 5, 1-16, (2004) |

[36] | Jabbour, Said; Raddaoui, Badran, Measuring inconsistency through minimal proofs, (Proceedings of the 12th European Conference Symbolic and Quantitative Approaches to Reasoning with Uncertainty, (2013)), 290-301 · Zbl 1352.68228 |

[37] | Junker, Ulrich, QUICKXPLAIN: preferred explanations and relaxations for over-constrained problems, (Proceedings of the 19th National Conference on Artificial Intelligence, (2004)), 167-172 |

[38] | Knight, Kevin, Measuring inconsistency, J. Philos. Log., 31, 1, 77-98, (2002) · Zbl 1003.03022 |

[39] | Konieczny, Sébastien; Roussel, Stéphanie, A reasoning platform based on the MI Shapley inconsistency value, (Proceedings of the 12th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, (2013)), 315-327 · Zbl 1390.68611 |

[40] | Liffiton, Mark; Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem, A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas, Constraints, 14, 4, 415-442, (2008) · Zbl 1181.90291 |

[41] | Liffiton, Mark; Moffitt, Michael; Pollack, Martha; Sakallah, Karem, Identifying conflicts in overconstrained temporal problems, (Proceedings of the 19th International Joint Conference on Artificial Intelligence, (2005)), 205-211 |

[42] | Lynce, Inês; Marques-Silva, João, On computing minimum unsatisfiable cores, (Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, (2004)), 305-310 |

[43] | Liffiton, Mark; Sakallah, Karem, Algorithms for computing minimal unsatisfiable subsets of constraints, J. Autom. Reason., 40, 1, 1-33, (2007) · Zbl 1154.68510 |

[44] | Malouf, Robert, Maximal consistent subsets, Comput. Linguist., 33, 2, 153-160, (2007) |

[45] | Mu, Kedian; Jin, Zhi; Liu, Weiru; Zowghi, Didar; Wei, Bo, Measuring the significance of inconsistency in the viewpoints framework, Sci. Comput. Program., 78, 9, 1572-1599, (2013) |

[46] | Mu, Kedian; Jin, Zhi; Lu, Ruqian; Liu, Weiru, Measuring inconsistency in requirements specifications, (Proceedings of the 8th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, (2005)), 440-451 · Zbl 1122.68666 |

[47] | Mu, Kedian; Liu, Weiru; Jin, Zhi, A general framework for measuring inconsistency through minimal inconsistent sets, Knowl. Inf. Syst., 27, 1, 85-114, (2010) |

[48] | Mu, Kedian; Liu, Weiru; Jin, Zhi, Measuring the blame of each formula for inconsistent prioritized knowledge bases, J. Log. Comput., 22, 3, 481-516, (2012) · Zbl 1241.68108 |

[49] | McAreavey, Kevin; Liu, Weiru; Miller, Paul; Mu, Kedian, Measuring inconsistency in a network intrusion detection rule set based on snort, Int. J. Semant. Comput., 5, 3, 281-322, (2011) · Zbl 1234.68376 |

[50] | McAreavey, Kevin; Liu, Weiru; Miller, Paul; Meenan, Chris, Tools for finding inconsistencies in real-world logic-based systems, (Proceedings of the 6th Starting AI Researchers’ Symposium, (2012)), 192-203 · Zbl 1394.68381 |

[51] | Ma, Yue; Qi, Guilin; Hitzler, Pascal; Lin, Zuoquan, Measuring inconsistency for description logics based on paraconsistent semantics, (Proceedings of the 9th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, (2007)), 30-41 · Zbl 1148.68487 |

[52] | Rafiq, Muhammad; Stuckey, Peter, A stochastic non-CNF SAT solver, (Proceedings of the 9th Pacific Rim International Conference on Artificial Intelligence, (2006)), 120-129 |

[53] | Mazure, Bertrand; Saïs, Lakhdar; Grégoire, Éric, A powerful heuristic to locate inconsistent kernels in knowledge-based systems, (Proceedings of the International Conference on Information Processing and Management of Uncertainty in Knowledge-Base Systems, (1996)), 1265-1269 |

[54] | Marques-Silva, João; Heras, Federico; Janota, Mikoláš; Previti, Alessandro; Belov, Anton, On computing minimal correction subsets, (Proceedings of the 23rd International Joint Conference on Artificial Intelligence, (2013)), 615-622 |

[55] | Nöhrer, Alexander; Biere, Armin; Egyed, Alexander, Managing SAT inconsistencies with HUMUS, (Proceedings of the 6th International Workshop on Variability Modeling of Software-Intensive Systems, (2012)), 83-91 |

[56] | Nadel, Alexander; Ryvchin, Vadim; Strichman, Ofer, Efficient MUS extraction with resolution, (Proceedings of the 13th Conference on Formal Methods in Computer Aided Design, (2013)), 197-200 |

[57] | Navarro, Juan; Voronkov, Andrei, Generation of hard non-clausal random satisfiability problems, (Proceedings of the 20th National Conference on Artificial Intelligence, (2005)), 436-442 |

[58] | Oh, Yoonna; Mneimneh, Maher; Andraus, Zaher; Sakallah, Karem; Markov, Igor, AMUSE: a minimally-unsatisfiable subformula extractor, (Proceedings of the 41st Annual Conference on Design Automation, (2004)), 518-523 |

[59] | Priest, Graham, Minimally inconsistent LP, Stud. Log., 50, 2, 321-331, (1991) · Zbl 0748.03017 |

[60] | Papadimitriou, Christos; Wolfe, David, The complexity of facets resolved, J. Comput. Syst. Sci., 37, 1, 2-13, (1988) · Zbl 0655.68041 |

[61] | Qi, Guilin; Hunter, Anthony, Measuring incoherence in description logic-based ontologies, (The Semantic Web, LNCS, vol. 4825, (2007)), 381-394 |

[62] | Qi, Guilin; Liu, Weiru; Bell, David, Measuring conflict and agreement between two prioritized belief bases, (Proceedings of the 19th International Joint Conference on Artificial Intelligence, (2005)), 552-557 |

[63] | Reiter, Raymond, A theory of diagnosis from first principles, Artif. Intell., 32, 1, 57-95, (1987) · Zbl 0643.68122 |

[64] | Roesch, Martin, Snort-lightweight intrusion detection for networks, (Proceedings of the 13th USENIX Systems Administration Conference, (1999)), 229-238 |

[65] | Carsten Sinz; Kaiser, Andreas; Küchlin, Wolfgang, Formal methods for the validation of automotive product configuration data, Artif. Intell. Eng. Des. Anal. Manuf., 17, 1, 75-97, (2003) |

[66] | Tjhai, Gina; Papadaki, Maria; Furnell, Steven; Clarke, Nathan, Investigating the problem of IDS false alarms: an experimental study using snort, (Proceedings of the IFIP TC 11 23rd International Information Security Conference, (2008)), 253-267 |

[67] | Tjhai, Gina; Papadaki, Maria; Furnell, Steven; Clarke, Nathan, The problem of false alarms: evaluation with snort and DARPA 1999 dataset, (Proceedings of the 5th International Conference: Trust, Privacy and Security in Digital Business, (2008)), 139-150 |

[68] | Tseitin, Grigorii Samuilovich, On the complexity of derivation in propositional calculus, (Studies in Mathematics and Mathematical Logics, vol. 2, (1968)), 115-125 |

[69] | Xiao, Guohui; Ma, Yue, Inconsistency measurement based on variables in minimal unsatisfiable subsets, (Proceedings of the 20th European Conference on Artificial Intelligence, (2012)), 864-869 · Zbl 1327.68263 |

[70] | Zhang, Lintao; Mali, Sharad, Extracting small unsatisfiable cores from unsatisfiable Boolean formula, (Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, (2003)) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.