Schaefer introduced a framework for generalized satisfiability problems on the Boolean domain and characterized the computational complexity of such problems. We investigate an algebraization of Schaefer's framework in which the Fourier transform is used to represent constraints by multilinear polynomials in a unique way. The polynomial representation of constraints gives rise to a relaxation of the notion of satisfiability in which the values to variables are linear operators on some Hilbert space. For the case of constraints given by a system of linear equations over the two-element field, this relaxation has received considerable attention in the foundations of quantum mechanics, where such constructions as the Mermin-Peres magic square show that there are systems that have no solutions in the Boolean domain, but have solutions via operator assignments on some finite-dimensional Hilbert space. We obtain a complete characterization of the classes of Boolean relations for which there is a gap between satisfiability in the Boolean domain and the relaxation of satisfiability via operator assignments. To establish our main result, we adapt the notion of primitive-positive definability (pp-definability) to our setting, a notion that has been used extensively in the study of constraint satisfaction problems. Here, we show that pp-definability gives rise to gadget reductions that preserve satisfiability gaps. We also present several additional applications of this method. In particular and perhaps surprisingly, we show that the relaxed notion of pp-definability in which the quantified variables are allowed to range over operator assignments gives no additional expressive power in defining Boolean relations.
DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE
证明了命题控制动态逻辑DL-PA和命题控制委托联合逻辑DCL-PC的模型检验和可满足性问题都是在PSPACE中进行的。我们解释了为什么（Balbiani，Herzig，Troquard，2013）中提出的DL-PA的模型检验问题的EXPTIME-硬度证明是错误的。我们还解释了为什么在PSPACE的成员证明的模型检验问题的DCL-PC（van der Hoek，Walther，Wooldridge，2010）是错误的。
Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability
我们考虑的问题，有效地枚举满意的分配给$\AC^0$电路。我们给出了一个零误差随机算法，它以$\AC^0$电路作为输入，并构造了一组限制，这些限制划分$\{0,1\}^n$，使得在每个限制下电路的值是常数。令$d$表示电路的深度，$cn$表示门的数量。该算法在时间$|C| 2^{n(1-μ_{c.d})}$中运行，其中$|C|$是概率至少为$1-2^{-n}$的$μ_{c,d} \ge 1/\bigO[\lg c + d \lg d]^{d-1}$的电路的大小。在此基础上，我们得到了$\AC^0$电路可满足性和计数解的改进指数时间算法。此外，我们还得到了具有奇偶校验的$\AC^0$电路的相关性的一个改进的界。作为我们分析的一个重要组成部分，我们扩展了哈斯塔德开关引理，以处理多个$\kcnf$和$\kdnf$。
Differentiable Satisfiability and Differentiable Answer Set Programming for Sampling-Based Multi-Model Optimization
National University of Ireland, Galway（爱尔兰国立高威大学）
本文提出了一种求解多模型优化问题的可微可满足性和可微答案集编程算法（Differentiable Satisfiability and Differentiable Answer Set Programming，简称SAT/ASP）。模型（答案集或满足真值分配）使用一种新的SAT/ASP求解方法，该方法使用基于梯度下降的分支机制进行采样。采样继续进行，直到用户定义的多模型成本函数的值达到给定阈值。作为我们的方法的主要用例，我们提出了分布感知模型采样和表达但可扩展的概率逻辑编程。作为我们的主要算法方法，微分SAT/ASP，我们介绍了一个增强的国家的最先进的CDNL/CDCL算法SAT/ASP解决。此外，我们提出了替代算法，使用未经修改的ASP求解器（Clingo/扣）和映射的优化任务，以传统的答案集优化或使用所谓的传播。我们还报告了开源软件DelSAT，我们的主要算法的最近原型实现，以及初步实验结果，这些结果表明，DelSAT的性能，当应用于概率逻辑推理的用例时，与马尔可夫逻辑网络（MLN）推理性能相当，尽管与MLN相比具有有利的特性，例如表达归纳定义的能力，以及在所有情况下直接将概率作为权重的能力。我们的实验还表明，我们的主要算法是非常优越的性能相比，所提出的替代方法，减少了一个共同的情况下，一般的问题，定期SAT/ASP。
SMPT: A Testbed for Reachability Methods in Generalized Petri Nets
SMPT（Satisfiability Modulo Petri Net）是一个用于Petri网可达性问题的模型检测器。它最初是一个试验符号模型检验的方法组合，并被设计为易于扩展。一些独特的功能是它能够从结构简化中受益，并生成判决证书。与模型检验竞赛中的其他最先进的工具相比，我们的工具相当成熟，表现良好。
