Projects per year
Abstract
The study of the worstcase complexity of the Boolean Satisfiability (SAT) problem has seen considerable progress in recent years, for various types of instances including CNFs, Boolean formulas and constantdepth 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 nontrivial 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 metaalgorithmic result about graph optimisation problems: any optimisation problem that can be formalised in Monadic SNP can be solved exactly with exponential savings over bruteforce 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 kCNFs and Boolean formulas, we obtain improved savings over subcube partitioning by combining existing algorithmic ideas in a more finegrained way.
We use the perspective of compositional mixing to show the first nontrivial 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^{nn^{\Omega(1)}}$.
Original language  English 

Title of host publication  Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science 
Place of Publication  New York, NY, USA 
Publisher  ACM 
Pages  393402 
Number of pages  10 
ISBN (Print)  9781450340571 
DOIs  
Publication status  Published  2016 
Event  2016 ACM Conference on Innovations in Theoretical Computer Science  Cambridge, United States Duration: 14 Jan 2016 → 16 Jan 2016 https://projects.csail.mit.edu/itcs/ 
Conference
Conference  2016 ACM Conference on Innovations in Theoretical Computer Science 

Abbreviated title  ITCS'16 
Country/Territory  United States 
City  Cambridge 
Period  14/01/16 → 16/01/16 
Internet address 
Fingerprint
Dive into the research topics of 'Satisfiability on Mixed Instances'. Together they form a unique fingerprint.Projects
 1 Finished

ALUnif  Algorithms and Lower Bounds: A Unified Approach
Santhanam, R.
1/03/14 → 28/02/19
Project: Research