On quantifying literals in boolean logic and its applications to explainable AI

被引:0
作者
Darwiche A. [1 ]
Marquis P. [2 ]
机构
[1] Computer Science Department, UCLA, Los Angeles, 90095, CA
[2] CRIL, Université d'Artois, CNRS, Institut Universitaire de France, Lens Cedex
基金
美国国家科学基金会; 欧盟地平线“2020”;
关键词
D O I
10.1613/JAIR.1.12756
中图分类号
学科分类号
摘要
Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have been explored over the decades. The existential quantification of literals (variable states) and its applications have also been studied in the literature. In this paper, we complement this by studying universal literal quantification and its applications, particularly to explainable AI. We also provide a novel semantics for quantification, discuss the interplay between variable/literal and existential/universal quantification. We further identify some classes of Boolean formulas and circuits on which quantification can be done efficiently. Literal quantification is more fine-grained than variable quantification as the latter can be defined in terms of the former. This leads to a refinement of quantified Boolean logic with literal quantification as its primitive. © 2021 AI Access Foundation. All rights reserved.
引用
收藏
页码:285 / 328
页数:43
相关论文
共 60 条
  • [1] Audemard G., Koriche F., Marquis P., On tractable XAI queries based on compiled representations, Proc. of KR'20, pp. 838-849, (2020)
  • [2] Beame P., Liew V., New limits for knowledge compilation and applications to exact model counting, Proc. of UAI'15, pp. 131-140, (2015)
  • [3] Bollig B., Buttkus M., On the relative succinctness of sentential decision diagrams, Theory Comput. Syst, 63, 6, pp. 1250-1277, (2019)
  • [4] Boole G., An investigation of the laws of thought, (1854)
  • [5] Bryant R. E., Graph-based algorithms for Boolean function manipulation, IEEE Trans. Computers, 35, 8, pp. 677-691, (1986)
  • [6] Chan H., Darwiche A., Reasoning about Bayesian network classifiers, Proc. of UAI'03, pp. 107-115, (2003)
  • [7] Choi A., Shih A., Goyanka A., Darwiche A., On symbolically encoding the behavior of random forests, Proc. of FoMLAS'20, 3rd Workshop on Formal Methods for ML-Enabled Autonomous Systems, (2020)
  • [8] Cimatti A., Roveri M., Traverso P., Strong planning in non-deterministic domains via model checking, Proc. of AIPS'98, pp. 36-43, (1998)
  • [9] Coste-Marquis S., Berre D. L., Letombe F., Marquis P., Complexity results for quantified Boolean formulae based on complete propositional languages, J. Satisf. Boolean Model. Comput, 1, 1, pp. 61-88, (2006)
  • [10] Darwiche A., Decomposable negation normal form, J. ACM, 48, 4, pp. 608-647, (2001)