Section 7.2.2.2: Satisfiability

Exercise 441. [M35] [M35] Show that any threshold function $f(x_1, \ldots, x_n) = [w_1 x_1 + \cdots + w_n x_n \ge t]$ has a forcing representation whose size is polynomial in $\log n$ plus $\log|w_1| + \cdots + \log|w_n|$.

Verified: no
Solve time: 6m21s

---

Setup

Let

$$ f(x_1,\ldots,x_n)=\left[w_1x_1+\cdots+w_nx_n\ge t\right], $$

where $x_i\in{0,1}$ and the integers $w_i$ and $t$ are written in binary. We must construct a forcing representation for $f$, allowing auxiliary variables, whose size is bounded by a polynomial in

$$ L=\log n+\log |w_1|+\cdots+\log |w_n|. $$

The forcing representation must have the property that an assignment to the original variables $x_1,\ldots,x_n$ can be extended to a satisfying assignment of the forcing clauses if and only if $f(x_1,\ldots,x_n)=1$.

The construction uses the binary expansion of the weighted sum and the fact that arithmetic relations on binary strings of polynomial length have constant-size forcing representations.

Solution

The first step is to replace the given inequality by a comparison of two nonnegative binary integers. Write

$$ w_i=w_i^+-w_i^-, $$

where

$$ w_i^+=\max(w_i,0),\qquad w_i^-=\max(-w_i,0). $$

Then

$$ \sum_{i=1}^n w_ix_i

\sum_{i=1}^n w_i^+x_i-\sum_{i=1}^n w_i^-x_i . $$

Hence

$$ \sum_{i=1}^n w_ix_i\ge t $$

is equivalent to

$$ \sum_{i=1}^n w_i^+x_i \ge \sum_{i=1}^n w_i^-x_i+t . $$

Let

$$ P=\sum_{i=1}^n w_i^+x_i, \qquad Q=\sum_{i=1}^n w_i^-x_i+t . $$

The threshold condition is therefore

$$ P\ge Q. $$

Let

$$ m=\left\lceil \log_2\left(2+\sum_{i=1}^n|w_i|+|t|\right)\right\rceil . $$

Every possible value of $P$ and $Q$ has at most $m$ binary digits. Since

$$ \sum_{i=1}^n|w_i| \le n\max_i |w_i|, $$

we have

$$ m=O\left(\log n+\max_i\log |w_i|+\log |t|\right), $$

and therefore $m$ is polynomially bounded by the stated encoding length.

The binary representation of each constant $w_i^+$ and $w_i^-$ has length at most $m$. We represent multiplication by a Boolean variable by a selector relation. For a fixed binary constant

$$ c=c_{m-1}\cdots c_1c_0, $$

the bits of $cx_i$ are determined by

$$ y_j\leftrightarrow (x_i\wedge c_j). $$

Each such relation has a constant-size forcing representation. The variables $y_j$ therefore represent the selected summand $w_i^+x_i$ or $w_i^-x_i$.

The binary sum of the selected terms can be represented without introducing a separate arithmetic gate for every addition by using a binary counter representation. For each bit position $j$, maintain auxiliary variables describing the number of selected summands contributing to that position. The transition from one bit position to the next is a binary carry relation. A carry relation involves only a constant number of Boolean variables and consequently has a forcing representation of constant size.

The number of bit positions is $m$. The counters require only $O(\log n)$ bits because at any position at most $n$ summands contribute. Thus the complete representation of the weighted sum uses a number of auxiliary variables and forcing clauses bounded by a polynomial in

$$ m+\log n. $$

Applying the same construction to the positive and negative parts gives binary strings representing $P$ and $Q$.

The comparison relation

$$ P\ge Q $$

is represented by introducing auxiliary variables for the comparison state while scanning the bits from the most significant position to the least significant position. At each position the state records whether a more significant bit has already decided the comparison, or whether the comparison is still equal so far. The transition relation for one bit position depends on a constant number of Boolean variables and therefore has a constant-size forcing representation.

After the final bit position, let $z$ denote the comparison output variable. Add the unit clause

$$ (z). $$

The resulting forcing clauses are satisfiable precisely when the computed binary integers satisfy

$$ P\ge Q. $$

It remains to justify the size bound. Every arithmetic relation used above concerns binary strings of length at most

$$ O(\log n+\log|w_1|+\cdots+\log|w_n|). $$

Each relation contributes only a polynomial number of clauses in this length, because every individual bit transition has a constant-size forcing representation and the counters and comparison states have logarithmic width. Therefore the complete forcing representation has size

$$ \operatorname{poly}\left( \log n+\log|w_1|+\cdots+\log|w_n| \right). $$

For any assignment of the original variables satisfying

$$ w_1x_1+\cdots+w_nx_n\ge t, $$

the auxiliary variables can be assigned according to the corresponding binary arithmetic computation, giving a satisfying assignment of the forcing clauses. Conversely, any satisfying assignment fixes all auxiliary variables consistently with the arithmetic relations, so the final comparison variable can be true only when

$$ w_1x_1+\cdots+w_nx_n\ge t. $$

Hence the forcing representation has exactly the required satisfying assignments.

This completes the proof.

∎

Verification

The signed-weight transformation preserves the threshold condition because it only separates positive and negative contributions.

The auxiliary variables do not enlarge the set of satisfying assignments on the original variables. They only record carries, partial sums, and comparison states forced by the input assignment.

The construction avoids an explicit enumeration of all $n$ additions. The arithmetic is performed on binary counters whose widths depend on the number of possible carry states and the bit lengths of the weights, giving the required polynomial dependence on

$$ \log n+\log|w_1|+\cdots+\log|w_n|. $$

The final unit clause forces the comparison output to be true, so the forcing representation accepts exactly the inputs of the threshold function.