I'm trying to implement the #2-SAT algorithm from the paper "Counting Satisfying Assignments in 2-SAT and 3-SAT" (Dahllöf, Jonsson and Wahlström, Theor. Comput. Sci. 332(1–3):265–291, 2005). A few lines into the algorithm description the authors denotes a sub algorithm and claims "The function $C_E$ computes #2-SAT by exhaustive search. It will be applied only to formulas of size ≤ 4 and can thus be safely assumed to run in O(1) time". The size of formulas is referred to the number of clauses.

I've been trying to find this exhaustive search algorithm that computes a #2-sat instance with number of clauses less than 4. But the results only returns algorithms for generally solving/counting models for #2 or #3-SAT and does not talk about a special case when size ≤ 4. First of all, is this claim true? Since the paper was published by a well known journal, I guess it is. But if so, does anyone know about this special case?


For any fixed $k$, a $k$-CNF with at most four clauses has at most $4k$ variables. So you can count the satisfying assigments with

count = 0
j = number of variables
for v1 = 0 to 1 do
    for v2 = 0 to 1 do
        for vj = 0 to 1 do
            if formula_value(phi, v1, ..., vj) == true
                count = count + 1

This runs in time $\Theta(2^j) = O(2^k) = \Theta(1)$, since $k$ is fixed.

  • $\begingroup$ Wow, thanks man!! $\endgroup$ – Rikard Olsson Mar 16 at 21:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.