Satisfiability on Mixed Instances
Satisfiability on Mixed Instances
复制标题
混合实例的可满足性
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
R. Santhanam
中科院分区：
文献类型：
--
作者：
Ruiwen Chen;R. Santhanam
近年来，对布尔可满足性（SAT）问题的最坏情况复杂性的研究取得了很大进展，包括CNF、布尔公式和常深度电路等。我们系统地研究了解决混合实例的复杂性，其中实例的不同部分来自不同的类型。我们的调查的动机部分是由实际情况，如SMT（可满足性模理论）解决，部分是由理论问题，如图问题的精确复杂性和希望找到一个统一的框架，已知的可满足性算法。我们研究了两种混合：合取混合，其中混合实例是由不同类型的纯实例的合取而形成的，以及组合混合，其中混合实例是由不同类型的电路的组合而形成的。对于合取混合，我们表明，非平凡的储蓄超过蛮力搜索可以获得一些实例类型在一个通用的方式使用子立方体分区的范例。我们应用这个通用的结果来显示关于图优化问题的元算法结果：可以在Monadic SNP中形式化的任何优化问题都可以通过暴力搜索的指数节省来精确解决。这以统一的方式捕获了关于诸如团、独立集和顶点覆盖等问题的已知结果。对于某些种类的合取混合，如混合物的$k$-CNFs和CNFs的有界大小，和k-CNFs和布尔公式，我们获得了改进的储蓄子立方体分区结合现有的算法思想，在一个更细粒度的方式。我们使用的角度来看，成分混合，以显示第一个非平凡的量化布尔公式的可满足性算法，其中没有深度限制的公式。我们证明了存在一个算法，对于任何这样的公式，具有常数数量的量词块和大小nc，其中c < 5/4，在时间上解决可满足性2 ^{n-n^{Omega（1）}}。
The study of the worst-case complexity of the Boolean Satisfiability (SAT) problem has seen considerable progress in recent years, for various types of instances including CNFs, Boolean formulas and constant-depth circuits. We systematically investigate the complexity of solving mixed instances, where different parts of the instance come from different types. Our investigation is motivated partly by practical contexts such as SMT (Satisfiability Modulo Theories) solving, and partly by theoretical issues such as the exact complexity of graph problems and the desire to find a unifying framework for known satisfiability algorithms. We investigate two kinds of mixing: conjunctive mixing, where the mixed instance is formed by taking the conjunction of pure instances of different types, and compositional mixing, where the mixed instance is formed by the composition of different kinds of circuits. For conjunctive mixing, we show that non-trivial savings over brute force search can be obtained for a number of instance types in a generic way using the paradigm of subcube partitioning. We apply this generic result to show a meta-algorithmic result about graph optimisation problems: any optimisation problem that can be formalised in Monadic SNP can be solved exactly with exponential savings over brute-force search. This captures known results about problems such as Clique, Independent Set and Vertex Cover, in a uniform way. For certain kinds of conjunctive mixing, such as mixtures of $k$-CNFs and CNFs of bounded size, and of k-CNFs and Boolean formulas, we obtain improved savings over subcube partitioning by combining existing algorithmic ideas in a more fine-grained way. We use the perspective of compositional mixing to show the first non-trivial algorithm for satisfiability of quantified Boolean formulas, where there is no depth restriction on the formula. We show that there is an algorithm which for any such formula with a constant number of quantifier blocks and of size nc, where c < 5/4, solves satisfiability in time $2^{n-n^{Omega(1)}}$.