<p>If you really want to enumerate <em>all</em> the assignments, then you really need to find a satisfying assignment and then <em>block</em> 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$.</p>

<p>One, relatively easy improvement, is to reduce the found assignment to a (prime) <em>implicant</em>. 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].</p>

<p>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]).</p>

<p>[1] <a href="http://link.springer.com/chapter/10.1007%2F3-540-45657-0_19" rel="nofollow">McMillan: Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002</a></p>

<p>[2] <a href="http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=6679395" rel="nofollow">Goldberg,Manolios: Quantifier elimination via clause redundancy. FMCAD 2013</a></p>

<p>[3] <a href="http://link.springer.com/chapter/10.1007%2F978-3-642-40627-0_33" rel="nofollow">Klieber et: al Solving QBF with Free Variables. CP 2013</a></p>

CC BY-SA 3.0
2014-04-30T16:36:52.640Z
2014-04-30T16:36:52.640Z
Mikolas
<p>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 <a href="http://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm" rel="nofollow">Quine–McCluskey algorithm</a> and <a href="http://en.wikipedia.org/wiki/Karnaugh_map" rel="nofollow">K-maps</a>, for example minimization techniques.</p>

CC BY-SA 3.0
2014-04-30T04:50:51.213Z
2014-04-30T04:50:51.213Z
Hunan Rostomyan
<p>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.</p>

<p>Assume there is a randomly generated propositional formula <code>f</code> that includes <code>n_total</code> number of boolean variables.</p>

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

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

<p><strong>Exmaple:</strong></p>

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

<p><em>Naive solution:</em></p>

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

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

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

<p>... etc. ...</p>

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

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

<p><strong>Optimizations over the naive solution:</strong>
My preliminary ideas: But what if two variables <code>a1</code> and <code>a2</code> are "xor", thus can never be true together in a model of <code>f</code>. 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.</p>

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

CC BY-SA 3.0
2014-04-30T10:17:14.597Z
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.
George
<time-complexity><sat><boolean-formulas>
Number of SAT checks that are needed to find all combinations of subset of boolean variables of a propositional formula
mrsteve
# Number of SAT checks that are needed to find all combinations of subset of boolean variables of a propositional formula

(Asked by: username_0 on 2014-04-30)

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.

**Tags:** time-complexity, sat, boolean-formulas

> **Comments:**
> **username_1**: 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.  

---

## 2 answers

### Answer by username_2 on 2014-04-30. Score: 4 | Accepted answer

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](http://link.springer.com/chapter/10.1007%2F3-540-45657-0_19)

[2] [Goldberg,Manolios: Quantifier elimination via clause redundancy. FMCAD 2013](http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=6679395)

[3] [Klieber et: al Solving QBF with Free Variables. CP 2013](http://link.springer.com/chapter/10.1007%2F978-3-642-40627-0_33)


---

### Answer by username_3 on 2014-04-30. Score: 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](http://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm) and [K-maps](http://en.wikipedia.org/wiki/Karnaugh_map), for example minimization techniques.


---

