Fighting Perebor: New and Improved Algorithms for Formula and QBF Satisfiability

Rahul Santhanam

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


We investigate the possibility of finding satisfying assignments to Boolean formulae and testing validity of quantified Boolean formulae (QBF) asymptotically faster than a brute force search. Our first main result is a simple deterministic algorithm running in time 2n-Ω(n) for satisfiability of formulae of linear size in n, where n is the number of variables in the formula. This algorithm extends to exactly counting the number of satisfying assignments, within the same time bound. Our second main result is a deterministic algorithm running in time 2n-Ω(n/log(n)) for solving QBFs in which the number of occurrences of any variable is bounded by a constant. For instances which are "structured", in a certain precise sense, the algorithm can be modified to run in time 2n-Ω(n). To the best of our knowledge, no non-trivial algorithms were known for these problems before. As a byproduct of the technique used to establish our first main result, we show that every function computable by linear-size formulae can be represented by decision trees of size 2n-Ω(n). As a consequence, we get strong superlinear average-case formula size lower bounds for the Parity function.

Original languageEnglish
Title of host publicationAnnual IEEE Symposium on Foundations of Computer Science
Place of PublicationLos Alamitos, CA, USA
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages10
ISBN (Print)978-1-4244-8525-3, 978-0-7695-4244-7
Publication statusPublished - 2010


Dive into the research topics of 'Fighting Perebor: New and Improved Algorithms for Formula and QBF Satisfiability'. Together they form a unique fingerprint.

Cite this