## Abstract

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 2^{n-Ω(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 2^{n-Ω(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 2^{n-Ω(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 2^{n-Ω(n)}. As a consequence, we get strong superlinear average-case formula size lower bounds for the Parity function.

Original language | English |
---|---|

Title of host publication | Annual IEEE Symposium on Foundations of Computer Science |

Place of Publication | Los Alamitos, CA, USA |

Publisher | Institute of Electrical and Electronics Engineers (IEEE) |

Pages | 183-192 |

Number of pages | 10 |

ISBN (Print) | 978-1-4244-8525-3, 978-0-7695-4244-7 |

DOIs | |

Publication status | Published - 2010 |