Belief revision is the task of modifying a knowledge base when new
information becomes available, while also respecting a number of desirable
properties. Classical belief revision schemes have been already specialised to
\emph{binary decision diagrams} (BDDs), the classical formalism to compactly
represent propositional knowledge. These results also apply to \emph{ordered}
BDDs (OBDDs), a special class of BDDs, designed to guarantee canonicity. Yet,
those revisions cannot be applied to \emph{sentential decision diagrams}
(SDDs), a typically more compact but still canonical class of Boolean circuits,
which generalizes OBDDs, while not being a subclass of BDDs. Here we fill this
gap by deriving a general revision algorithm for SDDs based on a syntactic
characterisation of Dalal revision. A specialised procedure for DNFs is also
presented. Preliminary experiments performed with randomly generated knowledge
bases show the advantages of directly perform revision within SDD formalism.

通过语法特征，我们为 Sentential Decision Diagrams（SDDs）推导出具有一般性的修订算法，并呈现了一个特殊的程序，以便于修订任务的直接操作。

命题决策图中的信念修正

Belief Revision in Sentential Decision Diagrams

We consider the compilation of a binary neural network's decision function
into tractable representations such as Ordered Binary Decision Diagrams (OBDDs)
and Sentential Decision Diagrams (SDDs). Obtaining this function as an OBDD/SDD
facilitates the explanation and formal verification of a neural network's
behavior. First, we consider the task of verifying the robustness of a neural
network, and show how we can compute the expected robustness of a neural
network, given an OBDD/SDD representation of it. Next, we consider a more
efficient approach for compiling neural networks, based on a pseudo-polynomial
time algorithm for compiling a neuron. We then provide a case study in a
handwritten digits dataset, highlighting how two neural networks trained from
the same dataset can have very high accuracies, yet have very different levels
of robustness. Finally, in experiments, we show that it is feasible to obtain
compact representations of neural networks as SDDs.

本文研究了如何将一个二进制神经网络的决策函数编译成可行的表示形式，如有序二进制决策图和命题决策图，并讨论了使用这些表示形式来验证神经网络的鲁棒性和计算期望鲁棒性的方法。此外，本文还提出了一种基于伪多项式时间算法编译单个神经元的高效方法，并在手写数字数据集中展示了两个神经网络的高准确度但鲁棒性不同的案例研究。最后，实验证明使用命题决策图可以获得神经网络的紧凑表示形式。

关于二元神经网络可计算性表示的研究

On Tractable Representations of Binary Neural Networks

Sentential decision diagrams (SDDs) introduced by Darwiche in 2011 are a
promising representation type used in knowledge compilation. The relative
succinctness of representation types is an important subject in this area. The
aim of the paper is to identify which kind of Boolean functions can be
represented by SDDs of small size with respect to the number of variables the
functions are defined on. For this reason the sets of Boolean functions
representable by different representation types in polynomial size are
investigated and SDDs are compared with representation types from the classical
knowledge compilation map of Darwiche and Marquis. Ordered binary decision
diagrams (OBDDs) which are a popular data structure for Boolean functions are
one of these representation types. SDDs are more general than OBDDs by
definition but only recently, a Boolean function was presented with polynomial
SDD size but exponential OBDD size. This result is strengthened in several
ways. The main result is a quasipolynomial simulation of SDDs by equivalent
unambiguous nondeterministic OBDDs, a nondeterministic variant where there
exists exactly one accepting computation for each satisfying input. As a side
effect an open problem about the relative succinctness between SDDs and free
binary decision diagrams (FBDDs) which are more general than OBDDs is answered.

本文旨在确定哪些布尔函数可以由小型的 SDDs 表示，同时将多项式大小的布尔函数表示集合与来自 Darwiche 和 Marquis 经典知识编译地图的表示类型进行比较。最主要的结果是通过等效的不明确的非确定性 OBDDs 对 SDDs 进行准多项式仿真，回答了 SDDs 和超过 OBDDs 的 FBDDs 相对简洁性之间的一个开放问题。

句子决策图的相对简洁性

On the Relative Succinctness of Sentential Decision Diagrams

Introduced by Darwiche (2011), sentential decision diagrams (SDDs) are
essentially as tractable as ordered binary decision diagrams (OBDDs), but tend
to be more succinct in practice. This makes SDDs a prominent representation
language, with many applications in artificial intelligence and knowledge
compilation. We prove that SDDs are more succinct than OBDDs also in theory, by
constructing a family of boolean functions where each member has polynomial SDD
size but exponential OBDD size. This exponential separation improves a
quasipolynomial separation recently established by Razgon (2013), and settles
an open problem in knowledge compilation.

本文介绍了一种名为 sentential decision diagrams (SDDs) 的表达语言，证明了在布尔函数的表示中 SDDs 比 ordered binary decision diagrams (OBDDs) 更简洁，该结论解决了知识编译中的一个开放性问题，并且在人工智能和知识编译等领域有广泛的应用。