Abstract
We present a simple randomized algorithm that approximates the number of satisfying assignments of Boolean formulas in conjunctive normal form. To the best of our knowledge this is the first algorithm which approximates #kSAT for any k>=3 within a running time that is not only nontrivial, but also significantly better than that of the currently fastest exact algorithms for the problem. More precisely, our algorithm is a randomized approximation scheme whose running time depends polynomially on the error tolerance and is mildly exponential in the number n of variables of the input formula. For example, even stipulating subexponentially small error tolerance, the number of solutions to 3CNF input formulas can be approximated in time O(1.5366^n). For 4CNF input the bound increases to O(1.6155^n).
We further show how to obtain upper and lower bounds on the number of solutions to a CNF formula in a controllable way. Relaxing the requirements on the quality of the approximation, on kCNF input we obtain significantly reduced running times in comparison to the above bounds.
BibTeX  Entry
@InProceedings{thurley:LIPIcs:2012:3440,
author = {Marc Thurley},
title = {{An Approximation Algorithm for #kSAT}},
booktitle = {29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
pages = {7887},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897354},
ISSN = {18688969},
year = {2012},
volume = {14},
editor = {Christoph D{\"u}rr and Thomas Wilke},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3440},
URN = {urn:nbn:de:0030drops34400},
doi = {http://dx.doi.org/10.4230/LIPIcs.STACS.2012.78},
annote = {Keywords: #kSAT, approximate counting, exponential algorithms}
}
Keywords: 

#kSAT, approximate counting, exponential algorithms 
Seminar: 

29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012) 
Issue Date: 

2012 
Date of publication: 

24.02.2012 