Satisfiability on Mixed Instances

Ruiwen Chen, Rahul Santhanam

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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)}}$.
Original languageEnglish
Title of host publicationProceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science
Place of PublicationNew York, NY, USA
PublisherACM
Pages393-402
Number of pages10
ISBN (Print)978-1-4503-4057-1
DOIs
Publication statusPublished - 2016
Event2016 ACM Conference on Innovations in Theoretical Computer Science - Cambridge, United States
Duration: 14 Jan 201616 Jan 2016
https://projects.csail.mit.edu/itcs/

Conference

Conference2016 ACM Conference on Innovations in Theoretical Computer Science
Abbreviated titleITCS'16
Country/TerritoryUnited States
CityCambridge
Period14/01/1616/01/16
Internet address

Fingerprint

Dive into the research topics of 'Satisfiability on Mixed Instances'. Together they form a unique fingerprint.

Cite this