Number of SAT checks that are needed to find all combinations of subset of boolean variables of a propositional formula

Question

Please mind that I sometimes lack formal mathematical knowledge and English is not my first language, so I might miss the right words. Please change the tile if needed. Also, I have choosen this site as for me the question is loosely related to complexity.

Assume there is a randomly generated propositional formula f that includes n_total number of boolean variables.

I am not interested in all boolean variables, but only in a small subset of n boolean variables of the formula f (thus n < n_total). I want to find all possible combinations that the subset of n boolean variables can take that are part of some model of f.

What is the expected number of SAT calls that are needed to calculate all the combinations of the n boolean variables that I am interested in?

Exmaple:

Assume my formula f has 50 boolean variables and I am only interested in a subset of three (thus n = 3) boolean variables a1, a2, a3. What different truth values can a1, a2 and a3 take where the result is an assigment that is part of a model of f?

Naive solution:

a1 a2 a3
0 0 0
=> check with a SAT solver, if the formula f has a model where all three variables a1, a2, a3 are false.

a1 a2 a3
0 0 1
=> check with a SAT solver, if the formula f has a model where a3 is true and a1 and a2 are false

a1 a2 a3
0 1 0
==> check with a SAT solver, if the formula f has a model where a2 is true and a1 and a3 are false

... etc. ...

a1 a2 a3
1 1 1
=> check with a SAT solver, if the formula f has a model where a1, a2 and a3 are true

Concerning the naive solution, If I am interested in a subset of n boolean variables of f, all the combinations of the n variables can be calculated with 2^n and thus 2^3 = 8 SAT calls.

Optimizations over the naive solution: My preliminary ideas: But what if two variables a1 and a2 are "xor", thus can never be true together in a model of f. In the set of the variables I am interested in (a1...a3 in the example), I can first try to find two boolean variables that are "xor". Or perhaps check all combinations of two variables whether they are "xor" and then proceed.

If I am interested in the expected number of SAT checks, is there an improvement over the 2^n number of checks of the naive solution? Assume the propositional formula f is randomly generated and has random characteristics.

Answer 1

If you really want to enumerate all the assignments, then you really need to find a satisfying assignment and then block it by a clause. E.g. if you find a satisfying assignment $a_1=a_2=a_3=0$ you'd block it by $a_1\lor a_2\lor a_3$.

One, relatively easy improvement, is to reduce the found assignment to a (prime) implicant. For instance, if $a_1\rightarrow f$, then you know that all assignments with $a_1=1$ are satisfying ($a_1$ is an implicant). You can reduce an existing satisfying assignment to an implicant by throwing one variable at a time. Similar approach published first (I think) here [1].

Somewhat more general problem is quantifier elimination, i.e. you're given $\exists X. f$ with some free variables $Y$, where $X$ and $Y$ are sets of variables. The output is a formula $f'$ that has only free variables $Y$ and has the same set of satisfying assignments as $\exists X. f$. Some recent papers on the problem [2][3]. (am a coauthor of the [3]).

[1] McMillan: Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002

[2] Goldberg,Manolios: Quantifier elimination via clause redundancy. FMCAD 2013

[3] Klieber et: al Solving QBF with Free Variables. CP 2013

Answer 2

That's right. If $n$ is the subset you're interested in, then there are, as you said, $2^{|n|}$ possible assignments. If you don't want to go through all those possibilities, you can use various optimization techniques to essentially decrease the size of $n$. Look at the Quine–McCluskey algorithm and K-maps, for example minimization techniques.