2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ The simplest thing you can do is to (a) find a satisfying assignment, (b) add a clause that does not allow your variables to take the same values as in the original assignment, (c) repeat step (a), until no more satisfying assignment exists. This will find all possible assignments of your variables, but I'm pretty sure there are better solutions. $\endgroup$ – George Apr 30 '14 at 10:17
4
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

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.