3
$\begingroup$

We are given a finite set of propositional atoms $\{x_1, \dots, x_n\}$ and an integer $k$. Can we capture through a propositional formula $\varphi$ (built from the standard connectives $\neg, \wedge, \vee$ only) the set of all models having at most $k$ atoms valued at $1$, such that the size of $\varphi$ is polynomial w.r.t. $n$? If yes, how?

The only way I see is to define $\varphi$ as an exponential-sized DNF formula containing $\binom{n}{k}$ conjunctions of literals. For instance, for n=5 and k=2, the corresponding formula would be $(\neg x_1 \wedge \neg x_2 \wedge \neg x_3) \vee (\neg x_1 \wedge \neg x_2 \wedge \neg x_4) \vee (\neg x_1 \wedge \neg x_2 \wedge \neg x_5) \vee (\neg x_2 \wedge \neg x_3 \wedge \neg x_4) \vee (\neg x_2 \wedge \neg x_3 \wedge \neg x_5) \vee \dots$

I got the following comment for the same question on https://cstheory.stackexchange.com/ but I do not have the level to understand it. I googled all keywords but I still cannot find the answer.

$d_H(\omega, \omega')$ equals the number of 1 bits in the pointwise XOR of $\omega$ and $\omega'$. So, compute the XORs, count the number of 1 bits, and compare the result to k. It is well known that one can count bits with log-depth circuits (hence polynomial-size formulas), and one easy way to do that is to sum the individual bits using repeated 3-to-2 carry-save addition. See en.wikipedia.org/wiki/Carry-save_adder if you don’t know what that is. The choice of the basis of connectives is immaterial in all this, as long as it is complete

Improve this question
$\endgroup$
4
  • $\begingroup$ Intuitively, I would express it as an exponential sized DNF formula containing $\binom{n}{k}$ conjonctions of literals. For instance, for $n=5$ and $k=2$, the corresponding formula would be $(\neg x_1 \wedge \neg x_2 \wedge \neg x_3) \vee (\neg x_1 \wedge \neg x_2 \wedge \neg x_4) \vee (\neg x_1 \wedge \neg x_2 \wedge \neg x_5) \vee (\neg x_2 \wedge \neg x_3 \wedge \neg x_4) \vee \dots$ I do not see a more succinct way to do it. I have asked the question on cstheory.stackexchange.com, but the question seems not appropriate there. The answer may be obvious, but not to me... $\endgroup$
    – user109711
    Commented Feb 5, 2015 at 16:29
  • $\begingroup$ The initial question is here: cstheory.stackexchange.com/questions/29389/… but I cannot understand the explanation. What about the specific case when n=5 and k=2 as above, for instance? $\endgroup$
    – user109711
    Commented Feb 5, 2015 at 16:47
  • 1
    $\begingroup$ Please edit your question to include your attempts and information you got. $\endgroup$
    – Raphael
    Commented Feb 5, 2015 at 17:35
  • $\begingroup$ possible duplicate of Encoding 1-out-of-n constraint for SAT solvers $\endgroup$
    – D.W. ♦
    Commented Feb 6, 2015 at 23:08

1 Answer 1

Reset to default
4
$\begingroup$

The idea is to use the following steps:

  1. Construct an NC1 circuit computing the binary representation of $x_1+\cdots+x_n$, see for example these lecture notes (Theorem 7). This circuit implements carry-save addition.
  2. Convert the NC1 circuit to a polynomial size formula, see for example these lecture notes (Proposition 1).
  3. For each $k$, it is now easy to construct a polynomial size formula that tests whether $x_1+\cdots+x_n=k$.
  4. Use up to $n$ of the formulas from the previous step to come up with your desired formula.

You can in fact implement the last two steps more efficiently, using $\log n$ rather $n$ copies of the preceding formula, by using a comparison gadget; details left to you.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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