Satisfiability of CTL* with constraints
Claudia Carapelle, Alexander Kartzow, Markus Lohrey
我们证明了在Z上具有等式，顺序和模约束的CTL* 的可满足性是可判定的。以前，仅知道CTL* 的某些片段的可判定性，例如，存在主义和积极的碎片和EF。
We show that satisfiability for CTL* with equality-, order-, and modulo-constraints over Z is decidable. Previously, decidability was only known for certain fragments of CTL*, e.g., the existential and positive fragments and EF.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL
研究了概率计算树逻辑（PCTL）的可满足性和有限可满足性问题，其中算子不受任何步界的限制。我们建立了几个片段包含定量运算符的可判定性，并指出了在更复杂的片段中出现的困难，其中可判定性仍然是开放的。
Satisfiability and Model Checking of CTL* with Graded Path Modalities
分次路径模态计算满足一个性质的路径的数量，并推广了CTL* 的存在（E）和泛（A）路径模态。生成的逻辑称为GCTL*。我们解决了GCTL* 可满足性的复杂性，即，2 ExpTime-Complete，以及GCTL* 的模型检验问题的复杂性，即，PSpace-Complete。对于CTL*，下限已经成立，因此，使用自动机理论方法，我们提供上限。这项工作的意义是双重的：GCTL* 比CTL* 更有表达力，而在计算复杂性方面没有额外的成本，并且GCTL* 具有CTL* 优于CTL的所有优点，例如，表达公平的能力。
Satisfiability Games for Branching-Time Logics
分支时间时态逻辑如CTL*、CTL和CTL+的可满足性问题在程序规范和验证中有重要的应用。它们的计算复杂性是已知的：CTL* 和CTL+对于双指数时间是完全的，CTL对于单指数时间是完全的.这些逻辑的一些决策程序是已知的;它们使用树自动机，tableaux或公理系统。在本文中，我们提出了一个统一的博弈论框架，这些分支时间时序逻辑的可满足性问题。我们定义可满足性游戏的完整的分支时间时序逻辑CTL* 使用高层次的定义获胜的条件，抓住了最少不动点展开的本质的良好基础。这些获胜条件构成了ω-词的形式语言。我们分析了在何种情况下需要哪种确定性ω-自动机来识别这些语言。然后，我们得到一个减少的问题，解决奇偶校验或Büchi游戏。所获得的算法的最坏情况下的复杂性匹配这些逻辑的已知下界。这种方法提供了一个统一的，但复杂性理论上的最佳处理分支时间时序逻辑的可满足性。它将时序逻辑机器的使用与自动机的使用分开，从而保留了输入公式和表示可满足性的对象之间的语法关系，即奇偶或Büchi游戏中的获胜策略。这里介绍的游戏只在输入公式的Fischer-Ladner闭包上工作。最后但并非最不重要的是，这里提出的游戏来尝试提供工具支持复杂的分支时间逻辑，如CTL* 和CTL+的可满足性问题。
On the Hybrid Extension of CTL and CTL+
本文研究了分支时间逻辑CTL和CTL+的变量混合扩张的可满足性的表达性、相对简洁性和复杂性。以前的复杂性结果表明，只有一个变量的片段具有基本复杂性。结果表明，H1CTL+和H1CTL，分别与一个变量的CTL+和CTL的混合扩展，是表示等价的，但H1CTL+是指数更简洁比H1CTL。另一方面，具有任意多个变量的CTL的混合扩展HCTL+不捕获CTL*，因为它甚至不能表达简单的CTL* 属性EGFp。H1CTL+的可满足性问题对于三重指数时间是完全的，这对于逻辑的相当弱的片段和相当强的扩展仍然成立。
Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures
本文提出树约束自动机，证明CTL(Z)与CTL*(Z)可满足性分别为ExpTime和2ExpTime完全，解决长期开放问题。
Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables
我们证明了分支时间时序逻辑CTL和CTL*，以及交替时间时序逻辑ATL和ATL*，在具有单个命题变量的语言中与在完整语言中一样具有语义表达性，即，有无限的命题变量由此可见，对于CTL和ATL，用单个变量的可满足性是EXPTIME-完全的，而对于CTL* 和ATL*，用单个变量的可满足性是2 EXPTIME-完全的，即，对于这些逻辑，只有一个变量的公式的可满足性与任意公式的可满足性一样困难。
A Team Based Variant of CTL
我们介绍了两个变种的计算树逻辑CTL的基础上的团队语义：一个异步的和同步的。对于这两个变种，我们调查的计算复杂性的可满足性以及模型检验问题。可满足性问题被证明是EXPTIME-完全的。在这里，考虑两种语义中的哪一种并不重要。对于模型检验，我们证明了同步情况下的PSPACE-完全性，异步情况下的P-完全性。此外，我们证明了这两种语义的几个有趣的基本属性。
A Faster Tableau for CTL*
最近有几个关于tableau系统的建议，用于确定在实际重要的分支时间时态逻辑（称为CTL*）中的可满足性。在本文中，我们提出了一个简化的和更传统的tableau方法建立在作者的早期理论工作。证明了结果的可靠性和完备性。一个原型的实施表明，显着提高性能的新方法的测试公式的范围。我们还看到，它比较有利的最先进的，游戏和自动机为基础的决策程序。
On the Complexity of Branching-Time Logics
我们分类的可满足性问题的CTL和UB的扩展的复杂性。我们考虑的扩展是路径公式，公平性，过去的模态和过去的布尔组合。我们的主要结果表明，所有这些扩展的CTL的可满足性仍然是在2-EXPTIME，这与CTL* 的非初等复杂性与非初等复杂性的强烈对比。我们给出了一个完整的分类，这些扩展的组合，产生一个二分法的扩展与2-EXPTIME完全和那些EXPTIME完全的复杂性。特别是，我们表明，可满足性的UB扩展与过去是完整的2-EXPTIME，矛盾的要求，一个更强的逻辑文献。利用一种新的卵石自动机建立了上界。
SAT-Based ATL Satisfiability Checking
模型与策略的综合是软件工程中一个非常重要的问题。这里的主要内容是检查表达要实现的系统规范的公式的可满足性。提出了一种新的判定交替时序逻辑（ATL）公式可满足性的方法。该方法扩展了CTL利用SAT模单调理论求解器的方法。类似于CTL的情况下，我们的方法似乎是非常有效的。实验结果表明，我们可以快速测试的大型ATL公式，已经达到了现有的方法。
On the Hardness of PCTL Satisfiability
本文证明了概率CTL（简称PCTL）的可满足性问题是不可判定的。通过对具有PCTL获胜目标的$1\frac{1}{2}$ -玩家博弈的简化，证明了PCTL可满足性问题是$Σ_1^1$ -困难的.我们提出了一个指数时间算法的可满足性的有界的，负封闭的片段的PCTL，并表明，可满足性问题，这个片段是EXPTIME困难的。
On relating CTL to Datalog
CTL是实践中占主导地位的时态规约语言，主要是因为它允许线性时间的模型检验。逻辑编程和数据库查询语言数据库经常被用作逻辑语言的实现平台。在本文中，我们提出了确切的CTL和数据库之间的关系，而且我们建立在这种关系和已知的有效算法CTL获得有效的算法分层数据库的片段。本文的主要贡献是：a）将CTL嵌入到STD中，STD是分层数据库的一个适当的片段。此外，我们表明，STD表示完全CTL -我们证明，通过嵌入STD到CTL。两个嵌入都是线性的。b）CTL也可以被嵌入到数据流的片段中而不进行否定。我们定义了一个片段的数据与后继内置谓词，我们称之为TDS和我们嵌入CTL到TDS在线性时间。我们建立在上述关系，以回答分层数据库的开放问题。我们证明了查询评价是线性的，包含性和可满足性问题都是可判定的。本文中提出的结果是第一个分层的Datatrics的片段，比那些只包含一元EDBs更一般。
CTL+FO Verification as Constraint Solving
表达程序正确性通常需要在整个执行（的不同分支）中关联程序数据。这些属性可以用CTL+FO来表示，这是一种允许混合时间和一阶量化的逻辑。判定程序是否满足CTL+FO性质是一个具有挑战性的问题，需要同时进行时间和数据推理。时态量词需要发现不变量和排序函数，而一阶量词需要实例化技术。本文提出了一种基于约束的CTL+FO性质自动证明方法。我们的方法使时间和一阶量化之间的相互作用明确的约束编码，结合递归和存在量化。通过将此约束编码与现成的求解器相结合，我们获得了CTL+FO的自动验证器。
Learning Branching-Time Properties in CTL and ATL via Constraint Solving
本文研究从Kripke结构和并发博弈结构样本中学习CTL与ATL公式的问题，通过将学习问题编码为可满足性问题并结合不动点模型检测算法进行符号化求解，并在Python原型中验证了方法的有效性。
Efficient CTL Verification via Horn Constraints Solving
时态逻辑的使用一直被认为是反应式系统的形式化规范和验证的基本方法。在本文中，我们采取的问题，自动验证的时间属性，由CTL公式，为一个给定的（可能是无限状态）的程序。我们提出了一种方法的基础上编码的问题作为一组霍恩约束。该方法以一个程序，建模为一个过渡系统，并作为输入的CTL公式给出的属性。首先利用CTL公式的句法结构生成一组普遍存在的量化Horn约束和良基约束。然后，通过应用现成的Horn约束求解引擎来求解生成的约束集。当且仅当生成的约束集有解时，程序才满足该性质。我们证明了实际的承诺的方法，通过将其应用于一组具有挑战性的例子。虽然我们的方法是基于一个通用的霍恩约束求解引擎，它是能够超越国家的最先进的方法专门为CTL验证。
Parameterized Complexity of CTL: A Generalization of Courcelle's Theorem
我们提出了一个几乎完整的分类的可满足性问题的计算树逻辑CTL的所有操作符片段的参数化复杂性。研究的参数化是时间深度和结构路径宽度的总和。分类显示了W[1]-硬和固定参数易处理片段之间的二分法。FPT中唯一被证实的真正的操作符片段是仅包含AX的片段。此外，我们证明了一个推广的Courcelle定理的无限签名，这将被用来证明FPT成员的情况。
On Relation between Constraint Answer Set Programming and Satisfiability Modulo Theories
约束回答集编程是将回答集编程与约束处理相结合的一个很有前途的研究方向。它通常与可满足性模理论领域有非正式的联系。然而，由于这两个研究领域使用的术语和概念不同，确切的正式联系被掩盖了。在本文中，我们通过揭示它们之间精确的形式关系来连接这两个研究领域。我们相信，这项工作将促进这两个领域的理论基础和现有的解决方法的交叉施肥。作为在这个方向上的一步，我们提供了一个从整数线性约束的约束答案集程序的可满足性模线性整数运算，铺平了道路，利用现代可满足性模理论求解器计算答案集的约束答案集程序的翻译。
Constraint LTL Satisfiability Checking without Automata
本文提出了一种新的方法来判定用线性时态逻辑语言写的带有将来和过去算子的公式和属于约束系统D的原子公式的可满足性（简称CLTLB（D））。该技术基于有界可满足性的概念，并将CLTLB（D）公式编码为QF-EUD，结合了无量词等式理论和D.类似于标准LTL，其中有界模型检查和SAT求解器可以用作自动机理论方法的模型检查的替代方案，我们的方法允许用户通过SMT求解技术来解决CLTLB（D）公式的可满足性问题，而不是通过检查合适的自动机A_A的语言的空性。该技术是有效的，并已在我们的Zot形式化验证工具中实现。
Boolean Satisfiability with Transitivity Constraints
我们考虑布尔可满足性问题的一个变体，其中出现在公式Fsat中的命题变量的子集E编码N个元素上的对称、传递、二元关系。对于1 <= i < j <= N，这些关系变量e[i，j]中的每一个表示元素i和j之间的关系是否成立。任务是找到对Fsat的满意分配，该分配也满足关系变量上的所有传递性约束（例如，e[1，2] & e[2，3] ==> e[1，3]），或者证明不存在这样的赋值。解决这个可满足性问题是我们的决策过程中的最后一步，也是最困难的一步，对于一个具有未解释函数的等式逻辑。这个过程形成了我们的工具的核心，用于验证流水线微处理器。为了使用传统的布尔可满足性检查器，我们增加了一套条款表达Fsat与条款表达的传递性约束。我们考虑的方法来减少这样的条款的数量的基础上的稀疏结构的关系变量。为了使用有序二元决策图（OBDDs），我们证明了对于某些集合E，传递性约束的OBDD表示对于所有可能的变量排序都具有指数大小。通过只考虑那些发生在OBDD表示的Fsat的关系变量，我们的实验表明，我们可以很容易地构建一个OBDD表示的相关的传递性约束，从而解决约束可满足性问题。
NP Satisfiability for Arrays as Powers
我们证明了具有等价关系的乘积结构的无量词理论的可满足性问题是NP问题。作为一个应用，我们扩展了组合数组逻辑片段来处理基数约束。由此产生的片段是独立的基本元素和索引集理论。
Monadic second order logic as the model companion of temporal logic
本文的主要重点是互模拟不变的MSO，更具体地说，在模型论中，一个理论的模型伴侣是一类模型的一阶描述，其中所有潜在的可解方程组和非方程组有解决方案。我们发现，双模拟不变的MSO树模型伴侣的一个新的时态逻辑，“公平CTL”，丰富的CTL与当地的公平性约束。为了实现这一点，我们给出了一个完整的证明，逻辑公平CTL相结合的tableaux和石头对偶，和一个公平的CTL编码的自动机的模态μ演算。此外，我们还证明了二叉树上的MSO是二元确定性公平CTL的模型伴侣。
Decidable Logics Combining Word Equations, Regular Expressions and Length Constraints
在这项工作中，我们考虑的可满足性问题的逻辑，结合字方程的字符串变量表示的话的无限长度，正则语言的话属于Presburger限制的话的长度。我们提出了一种新的决策过程，在两个可决策的片段，包括二次字方程（即，每个字符串变量最多出现两次）。所提出的过程减少了问题解决的Presburger算法的可满足性。该过程结合了两个主要组成部分：（i）一个算法，以获得一个完整的一组所有的解决方案的词方程和正则表达式的连接;和（ii）两种方法，以精确计算关系约束的字符串长度所隐含的所有solutions.We已经实现了一个原型工具，并评估了一组可满足性问题的逻辑。实验结果表明，该工具是有效和高效的。
The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable
一阶线性实算术丰富的未解释的谓词符号产生一个有趣的建模语言。然而，这样的公式的可满足性是不可判定的，即使我们限制未解释的谓词符号为arity 1。为了找到这种语言的可判定片段，有必要限制算术部分的表达能力。一种可能的途径是将算术表达式限制为$x - y \mathrel{\#} c$形式的差异约束，其中$\#$的范围在标准关系$<, \leq, =, \neq, \geq, >$和$x,y$上，并且是通用量化的。然而，它是已知的，结合差异约束与未解释的谓词符号产生一个不可判定的可满足性问题。在本文中，证明了可满足性成为可判定的，如果我们另外限制泛量化变量的范围。由于实数上的有界区间仍然包含无穷多个值，平凡的实例化过程不足以解决这个问题。
Bounded Reachability for Temporal Logic over Constraint Systems
我们提出了CLTLB（D），一个扩展PLTLB（PLTL与过去和未来的运营商）增加了原子公式建立在一个约束系统D。即使对于可判定的约束系统，这种逻辑的可满足性和模型检验问题也可能是不可判定的。我们引入适当的限制和假设，使扩展逻辑可判定的可满足性问题。此外，对于一个大类的约束系统，我们提出了一个编码，实现了一个有效的决策过程的有界可达性问题。
Deciding the Satisfiability of MITL Specifications
在本文中，我们提出了一个可满足性保持减少MITL解释有限变量连续行为的约束LTL时钟，CLTL的一个变种，是可判定的，并为一个SMT为基础的有界可满足性检查。其结果是一个新的完整的和有效的决策程序的MITL。虽然MITL的决策程序已经存在，他们采用的自动机为基础的技术似乎是很难实现在实践中，而且，据我们所知，目前还没有实现它们。一个原型工具MITL的基础上的编码在这里提出的，而不是，已经实施，并公开提供。
NP Decision Procedure for Monomial and Linear Integer Constraints
受函数符号约束可满足性的启发，我们考虑了非负整数上的数值不等式。我们考虑的约束是线性系统Ax = b和形式为x_i >= x_j^n（x_i <= x_j^n）的（非）凸约束的合取。我们表明，这些约束的可满足性是NP-完全的，即使解决方案的线性部分是明确的。作为结果，我们获得了NP完全的扩展的某些数量自由约束集的基数（QFBAPA）与功能图像S = f[P^n]。
(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints
我们证明了几个可判定性和不可判定性结果的可满足性和有效性问题的语言，可以表示解决方案的字方程的长度约束。这种语言上的原子公式是字符串项上的等式（单词等式）、长度函数上的线性不等式（长度约束）和正则集中的成员资格。这些问题在逻辑、程序分析和形式化验证中很重要。这些问题的变体已经被数学家研究了几十年。最近，这些公式的实际可满足性程序（又名SMT求解器）在字符串操作程序（如Web应用程序）的安全分析中变得越来越重要。我们证明了三个主要定理。首先，我们给出了一个新的证明不可判定的有效性问题的一组句子写为一个forall-exists量词交替应用于正字方程。这个不可判定性结果的一个推论是，这个集合是不可判定的，即使句子中最多出现两次字符串变量。第二，我们考虑布尔组合的量词自由公式构建的词方程和长度约束。我们表明，如果字方程可以转换为一个解决的形式，在实践中相关的形式，然后满足性问题的布尔组合的字方程和长度约束是可判定的。第三，我们证明了无量词公式在正则解形式、长度约束和正则表达式上的成员谓词上的可满足性问题也是可判定的。
Branching-Time Model Checking Gap-Order Constraint Systems (Extended Version)
研究了带间隙序约束系统的模型检验问题。分支时间时序逻辑CTL，特别是它的片段EG和EF。GCS是由整数值变量的演化描述的非确定性无限分支过程，服从形式为$x-y\ge k$的Presburger约束，其中$x$和$y$是变量或常数，$k\in\mathbb{N}$是非负常数。我们表明，EG模型检验是不可判定的GCS，而EF是可判定的。特别是，这意味着GCS和有限状态系统之间的强和弱互模拟等价的可判定性。
Neuro-Symbolic Constrained Optimization for Cloud Application Deployment via Graph Neural Networks and Satisfiability Modulo Theory
本文提出基于图神经网络和可满足性模理论的神经符号框架，用于优化云应用部署，通过结合约束推理与机器学习提升求解器的可扩展性和成本最优性。
Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints
我们介绍和调查的表达描述逻辑（DL）ALCSCC++，在其中的全局和局部基数约束在以前的文件中介绍的可以混合。一方面，我们证明了这不会增加可满足性检查和其他标准推理问题的复杂性。另一方面，可满足性问题成为不可判定的，如果逆角色添加到语言。此外，即使没有相反的角色，合取查询蕴涵在这个DL原来是不可判定的。我们证明了查询的可判定性可以恢复，如果全局和局部约束不混合和全局约束适当的限制。后一个结果基于局部非循环模型构造，并且它将查询蕴涵减少到受限设置中的ABox一致性，即，到ABox一致性w.r.t. ALCSCC中的受限基数约束，我们可以显示ExpTime上限。
Incremental Satisfiability and Implication for UTVPI Constraints
单位两变量不等式（UTVPI）约束形成了多项式时间可解的整数约束的最大类之一（除非P=NP）。有相当大的兴趣在他们的使用约束求解，抽象解释，空间数据库，和定理证明。本文提出了一种新的UTVPI约束满足和蕴涵检验的增量算法，该算法需要O（m + nlogn + p）时间和O（n+m+p）空间来增量检验m个UTVPI约束对n个变量的可满足性和p个UTVPI约束的蕴涵性。
Satisfiability of Context-free String Constraints with Subword-ordering and Transducers
本文研究带子词序和有理转换器的上下文无关字符串约束可满足性，证明该片段在加入转换器后仍可判定，并给出2NExptime与NExptime完全性结果及双指数下界引理。
Analysis of logics with arithmetic
该研究针对带计数与算术的逻辑的有限可满足性问题，给出局部Presburger量词逻辑可满足性复杂度紧界与双变量计数逻辑基数半线性表示，还简化了部分已有关键结果的证明。
Monadic second order finite satisfiability and unbounded tree-width
Seese（1991）的经典结果证明了一元二阶逻辑的有限可满足性问题只能在有界树宽的结构类上判定。本文证明了以下问题是可判定的：输入：（i）一元二阶逻辑语句$α$，（ii）一个语句$β$，该语句在一阶逻辑的两变量片段中扩展为计数量词. $α$和$β$的词汇表可以相交。输出量：是否存在满足$α\landβ$的有限结构，使得该结构对$α$的词汇表的限制具有有界树宽？(The所需结构的树宽度不受限制）。因此，我们证明了可满足性问题的可判定性的有限结构的有界树宽度的逻辑扩展一元二阶逻辑的线性基数约束的形式$|X_{1}|+\cdots+|X_{r}|<|Y_{1}|+\cdots+|Y_{s}|$，其中$X_{i}$和$Y_{j}$是一元二阶变量。我们证明了WS1S的一个类似的扩展的可判定性。
Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
在计算机科学的各个领域中，我们处理一组需要满足的约束。如果不能同时满足这些约束条件，则最好找出其中的核心问题。这些核被称为最小不可满足子集（MUSes）。标识的MUSes越多，获得的关于约束之间的冲突的信息就越多。然而，由于可能的冲突数量巨大（甚至呈指数级），所有MUSes的完整枚举通常是难以处理的。此外，要识别MUSes算法必须测试约束集的同时满足性。测试的类型取决于应用程序域。测试的复杂性可能非常高，特别是对于时态逻辑、模型检验或SMT等领域。在本文中，我们提出了一种递归算法，以在线方式识别MUSes（即，一个接一个），并且可以在任何时间终止。我们的算法的主要特点是，它最大限度地减少可满足性测试的数量，从而加快计算速度。该算法适用于任意约束域，其有效性证明了自己，特别是在昂贵的可满足性检查的领域。我们对我们的算法进行基准测试，对最先进的布尔和SMT约束域的算法，并证明我们的算法真的需要较少的可满足性测试，从而发现更多的MUSes在给定的时间限制。
Satisfiability of ECTL* with tree constraints
最近，我们已经证明了满足$\mathsf{ECTL}^*$的约束$\mathbb{Z}$是可判定的使用一种新的技术。这种方法将带有约束的$\mathsf{ECTL}^*$在某个结构A（或一类结构）上的可满足性问题归结为A是否具有我们称之为EHD的某种模型论性质的问题（因为“同态的存在性是可判定的”）。在这里，我们将这种方法应用到具体的领域，是树状的，并获得几个结果。我们证明了带约束的$\mathsf{ECTL}^*$的可满足性在（i）半线性序（即，树状结构，其中分支形成任意线性次序），（ii）序数树（半线性次序，其中分支形成序数），以及（iii）对于每个固定的$h\in \mathbb{N}$高度为h的无限分支树。我们证明了所有这些结构类具有EHD性质。相反，我们介绍了$\mathsf{WMSO}+\mathsf{B}$（弱$\mathsf{MSO}$与边界量词）的Escherichfeucht-Fraisse-游戏，并使用它们来证明无限（顺序）树不具有属性EHD。因此，必须采取不同的方法，以解决问题是否满足$\mathsf{ECTL}^*$（或甚至$\mathsf{LTL}$）的无限（顺序）树的约束是可判定的。
The Complexity of Boolean Constraint Isomorphism
1978年，Schaefer证明了他著名的广义可满足性问题的二分法。他定义了无限多的命题可满足性问题（现在通常称为布尔约束满足问题），并表明，所有这些可满足性问题要么在P或NP完全。近年来，对于布尔约束的其他一些问题也得到了类似的结果，这些问题几乎都是可满足性问题的变形。在本文中，我们解决了一个问题，这不是一个变化的可满足性，即同构问题的布尔约束。Böhler等人先前的工作表明同构问题要么是coNP-难的，要么可简化为图同构问题（一个NP问题，但不知道是NP-难的），从而区分了困难情况和较容易的情况。然而，他们没有分类哪些情况是真正容易的，即，在P中，这篇论文正是这样做的。证明了布尔约束同构是coNP-困难的（和GI-困难的），或等价于图同构，或在P中，并给出了判断哪种情况成立的简单准则。
Generalized Satisfiability Problems via Operator Assignments
Schaefer介绍了布尔域上的广义可满足性问题的框架，并描述了这类问题的计算复杂性。我们研究了Schaefer框架的代数化，其中傅立叶变换被用来以独特的方式表示多线性多项式的约束。约束的多项式表示引起了可满足性概念的放松，其中变量的值是某些希尔伯特空间上的线性算子。对于由二元场上的线性方程组给出的约束的情况，这种松弛在量子力学的基础中受到了相当大的关注，其中诸如Mermin-Peres幻方的构造表明，存在在布尔域中没有解的系统，但通过在某些有限维希尔伯特空间上的算子赋值有解。我们得到了一个完整的性质的布尔关系类，其中有一个在布尔域的可满足性和可满足性通过操作符分配松弛之间的差距。为了建立我们的主要结果，我们适应的概念连续积极的可定义性（PP-可定义性），我们的设置，一个概念，已被广泛用于约束满足问题的研究。在这里，我们表明，PP-可定义性引起的小工具减少，保持可满足性差距。我们还提出了这种方法的几个额外的应用。特别是，也许令人惊讶的是，我们表明，宽松的概念PP-可定义性，其中量化的变量被允许范围超过运营商的分配，没有额外的表达能力，在定义布尔关系。
Symmetry Breaking for Maximum Satisfiability
对称性是许多组合问题所固有的，包括布尔可满足性（SAT）和约束规划（CP）。在SAT中，对称破缺谓词（SBP）的识别是一种众所周知的，通常有效的解决难题的技术。SAT中SBPs的识别近年来一直是显著改进的主题，从而产生了更紧凑的SBPs和更有效的算法。SBPs的识别也被应用到伪布尔（PB）约束，表明对称破缺也可以是PB约束的有效技术。本文进一步扩展了SBPs的应用，并表明SBPs可以识别和使用在最大可满足性（MaxSAT），以及在其最知名的变体，包括部分MaxSAT，加权MaxSAT和加权部分MaxSAT。与SAT和PB一样，MaxSAT和变体的对称性破缺谓词对于代表性数量的问题域是有效的，允许解决当前最先进的MaxSAT求解器无法解决的问题实例。
Adapting Real Quantifier Elimination Methods for Conflict Set Computation
实闭域上的可满足性问题是可判定的。在可满足性模理论的背景下，限制于文字的合取集，即多项式约束集的问题是特别重要的。中心问题之一是计算这些集合的不可满足性的良好解释，即获得其合取已经不可满足的输入约束的小子集。我们采用两种常用的实量词消去方法，柱形代数分解和虚拟替代，提供这样的冲突集，并证明我们的方法在实践中的性能。
Flexible constraint satisfiability and a problem in semigroup theory
本文研究了灵活约束满足与半群理论中的问题，展示了2-稳健单调1-in-3 3SAT的NP完全性，并通过3元和6元代数实例证明了NP难种类成员资格问题。
SHACL Satisfiability and Containment (Extended Paper)
XML约束语言（SHACL）是最近W3C推荐的用于验证RDF数据的语言。具体来说，SHACL文档是在RDF图上强制特定形状的约束的集合。以前的工作提供了理论和实际的验证问题的结果，但没有考虑标准的决策问题的可满足性和包容性，这是至关重要的验证的可行性的约束和重要的设计和优化的目的。在本文中，我们进行了深入的研究，非递归SHACL的不同功能，提供了一个新的一阶语言，称为SCL的翻译，准确地捕捉语义的SHACL w.r.t.可满足性和包容性。我们研究了SHACL功能在这个逻辑中的相互作用，并提供了详细的地图的可判定性和复杂性的结果，上述决策问题的不同SHACL子语言。值得注意的是，我们证明了这两个问题是不可判定的完整的语言，但我们提出了可判定的组合有趣的功能。
Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
针对有限MDP上带结构约束的鲁棒奖励最优策略计算难题，本文提出结合可满足性求解器与概率模型检查的合成框架，实验证明其可行且性能媲美现有最优方法。
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
我们介绍了一种方法，旨在结合使用的可满足性模理论（SMT）求解器的组合逻辑合成器（CL）的框架。(CL)S是一种用于从用户指定的存储库自动组合软件组件的工具。该框架产生一个树语法，其中包含符合目标类型的所有组合术语。（CL）S的类型规范基于具有交集类型的组合逻辑。我们的方法将树语法转换为SMT功能，这允许考虑额外的特定于域的约束。我们证明了我们的方法在几个实验中的实用性。
Hypergraph Neural Networks Accelerate MUS Enumeration
本文提出基于超图神经网络的领域无关方法，通过强化学习训练代理加速MUS枚举，减少可满足性检查次数。
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
提出了一种确定实数上非线性多项式约束合取可满足性的新算法，该算法可作为非线性实数算术可满足性模理论（SMT）求解的理论求解器.该算法是适应于可满足性的柱形代数分解（CAD）的变体，其中解候选者（样本点）被增量地构造，直到找到满意的样本或者已经采样了足够的样本以得出不可满足性的结论。样本的选择由输入约束和先前的冲突指导。我们的新方法背后的关键思想是从部分样本开始;证明它不能扩展到完整样本;并从排除部分样本周围的更大空间的原因中，逐步建立成空间的圆柱代数覆盖。有相似之处的增量变化的CAD，NLSAT方法的Jovanovic和de Escha，和NuCAD算法的布朗，但我们目前的工作示例和实验结果的初步实施，以证明这些差异，和新方法的好处。
On Algorithms and Complexity for Sets with Cardinality Constraints
类型状态系统确保命令式程序的许多所需属性，包括对象字段的初始化和有状态库接口的正确使用。具有基数约束的抽象集合自然地概括了类型状态属性：对象的类型状态之间的关系可以表示为集合上的子集和不相交关系，集合的元素可以表示为基数为1的集合。受这些应用的启发，本文提出了新的算法和新的复杂性结果的限制集和他们的基数。我们研究了几类约束，并展示了他们的表达能力和复杂性之间的权衡。我们的第一个结果涉及一个无量词片段的布尔代数与Presburger算术。我们给出了一个不确定的多项式时间算法减少满足集的符号基数上的限制常数基数，并给出了一个多项式空间算法所产生的问题。在寻求更有效的片段，我们确定了几个子集的基数约束，其满足性是NP难的。最后，我们确定了一类约束，具有多项式时间的可满足性和蕴涵问题，可以作为有效的程序分析的基础。
Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees
提出XOR-SMC算法，通过随机化XOR约束将NP^PP-完全的模计数可满足性问题转化为SAT问题，在多项式时间内提供常数近似保证，并在AI向善实验中优于基线。
Incremental Cardinality Constraints for MaxSAT
最大可满足性（MaxSAT）是布尔可满足性（SAT）问题的一个优化变体。一般来说，MaxSAT算法执行一系列SAT求解器调用，以达到广泛使用基数约束的最佳解决方案。这些算法中的许多算法本质上是非增量的，即在每次迭代中，公式被重建，并且没有知识从一个迭代重用到另一个迭代。在本文中，我们利用跨迭代获得的知识，使用新的计划，以增量的方式使用基数约束。我们将这些计划与几个MaxSAT算法。我们的实验结果表明，显着的性能提升，这些算法相比，他们的非增量同行。这些结果表明，增量基数约束可能是有益的其他约束求解域。
A Decision Procedure for String Logic with Equations, Regular Membership and Length Constraints
本文研究了长度函数上具有方程、正则隶属和Presburger约束的串逻辑的可满足性问题。困难来自于字符串变量的多次出现，使得最先进的算法无法终止。我们的主要贡献是表明，可满足性问题的片段中没有字符串变量出现两次以上的方程是可判定的。特别是，我们提出了一个半决策过程的任意字符串公式与字方程，经常成员和长度功能。我们的过程的本质是一个算法，枚举一个等价的一组可解析取公式。我们进一步表明，该算法总是终止上述可判定的片段。最后，我们提供了我们的决策过程的复杂性分析，以证明它运行，在最坏的情况下，在阶乘时间。
The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)
我们研究了著名的度量区间时态逻辑MITL[U_I，S_I]的两个一元片段，并确定了它们的表达性和满足复杂性.我们证明了MITL[F_ \inf，P_ \inf ]对于偏序双向确定时间自动机（po 2DTA）是（令人惊讶的）表达完备的，并且从逻辑到自动机的约简给出了它的NP完全可满足性.我们还证明了一元模态只有有界区间的片段MITL[F_b，P_b]具有\nexptime -完全可满足性.但奇怪的是，MITL[F_b，P_b]严格地说不如MITL[F_ \inf，P_ \inf ]有表达性。我们提供了一个全面的图片的可判定性和表现力的各种一元片段的MITL。
New Algorithms and Hardness Results for Robust Satisfiability of (Promise) CSPs
本文提出了针对承诺CSPs鲁棒可满足性的新算法，并在UGC假设下证明了相关结果。
Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
本文提出KOCO-SMC，一种集成的精确模计数可满足性求解器，通过跟踪上下界和部分变量赋值实现早期估计，显著提升求解效率。
Satisfiability and Synthesis Modulo Oracles
在经典的程序合成算法中，例如反例引导归纳合成（CEGIS），算法在合成阶段和预言（验证）阶段之间交替。许多合成算法使用基于可满足性模理论（SMT）求解器的白盒预言机来提供反例。但是，如果白盒Oracle不可用或不容易使用，该怎么办？我们提出了一个框架来解决一般类的预言指导的合成问题，我们长期合成模预言。在这种情况下，预言机可以是黑盒子，具有由合成问题定义的查询-响应接口。作为该框架的一个必要组成部分，我们还形式化了可满足性模理论和预言机问题，并提出了一个算法来解决这个问题。我们实现了一个原型求解器的可满足性和合成模神谕，并证明，通过使用神谕执行功能不容易建模SMT约束，如递归函数或神谕，将编译和执行的代码，SMTO和SyMO能够解决超出标准SMT和合成求解器的能力的问题。
Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
本文提出带极值约束的寄存器自动机模型，证明其空性问题可判定，并应用于二变量逻辑，在树序和线性序存在时证明其可数可满足性及可满足性问题可判定。
An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes
针对现有SMT求解器处理代数数据类型（ADTs）时因惰性方法导致扩展性差的问题，提出一种急切方法，将ADT查询归约为未解释函数（UF）理论，并证明了该方法的可靠性、完备性及优于现有方法的性能。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。