You are currently browsing the tag archive for the ‘SAT’ tag.

As reported here, here and here, Mark Braverman has just announced a proof of a 1990 conjecture by Linial and Nisan.

Mark proves that if {C} is an AC0 boolean circuit (with NOT gates and with AND gates and OR gates of unbounded fan-in) of depth {d} and size {S}, and if {X} is any {k}-wise independent distribution with {k = (\log S)^{O(d^2)}}, then

\displaystyle  {\mathbb E} C(U_n) \approx {\mathbb E} C(X)

that is, {X} “fools” the circuit {C} into thinking that {X} is the uniform distribution {U_n} over {\{0,1\}^n}. Plausibly, this might be true even for {k = O((\log S)^{d-1})}.

Nothing was known for depth 3 or more, and the depth-2 case was settled only recently by Bazzi, with a proof that, as you may remember, has been significantly simplified by Razborov about six months ago.

Mark’s proof relies on approximating {C} via low-degree polynomials. The point is that if {p} is an {n}-variate (real valued) polynomial of degree {\leq k}, and {X} is a {k}-wise independent distribution ranging over {\{0,1\}^n}, then

\displaystyle  {\mathbb E} p(X) = {\mathbb E} p(U_n)

Now if we could show that {p} approximates {C} both under {X} and under {U_n}, in the sense that {{\mathbb E} p(X) \approx {\mathbb E} C(X)}, and also {{\mathbb E} p(U_n) \approx {\mathbb E} C(U_n)}, then we would be done.

The Razborov-Smolenski lower bound technique gives a probabilistic construction of a polynomial {p} such that for every input {x} one has a high probability that {p(x) = C(x)}. In particular, one get one polynomial {p} such that both

\displaystyle   {\mathbb P}_{x\sim X} [p(x) = C(x) ] = 1-o(1) \ \ \ \ \ (1)

and

\displaystyle   {\mathbb P}_{x\sim U_n} [p(x) = C(x) ] = 1-o(1) \ \ \ \ \ (2)

Unfortunately this is not sufficient, because the polynomial {p} might be very large at a few points, and so even if {p} agrees with {C} with high probability there is no guarantee that the average of {p} is close to the average of {C}.

Using a result of Linial, Mansour and Nisan (developed in the context of learning theory), one can construct a different kind of low-degree approximating polynomial {p}, which is such that

\displaystyle   {\mathbb E}_{x\sim U_n} | C(x) - p(x)|^2 = o(1) \ \ \ \ \ (3)

The Linial-Mansour-Nisan approximation, however, says nothing about the relation between {p} and {C} under the distribution {X}.

Using ideas of Bazzi’s, however, if we had a single polynomial {p} such that properties (1), (2) and (3) are satisfied simultaneously, then we could construct another low-degree polynomial {p'} such that {{\mathbb E} p'(X) \approx {\mathbb E} C(X)}, and also {{\mathbb E} p'(U_n) \approx {\mathbb E} C(U_n)}, giving us that {C} is fooled by {X}.

As far as I understand, Mark constructs a polynomial satisfying properties (1), (2) and (3) by starting from the Razborov-Smolenski polynomial {p}, and then observing that the indicator function {E} of the points on which {p \neq C} is itself a boolean function admitting a Linial-Mansour-Nisan approximation {e}. Defining {p' := p\cdot (1-e)}, we have that {p'} has all the required properties, because multiplying by {1-e} “zeroes out” the points on which {p} is excessively large.

I have been interested in this problem for some time because of a connection with the complexity of 3SAT on random instances.

Read the rest of this entry »

Earlier, here and here, we discussed the following problem: we pick at random a k-CNF formula with $n$ variables and $m$ clauses; if $m$ is at least $c_k n$, for a constant $c_k$, then we know that with high probability the formula is unsatisfiable; is there an algorithmic way of certifying this unsatisfiability?

One approach we discussed is a reduction to 2SAT, which works provided $m$ is at least of the order of $n^{k-1}$. What about sparser formulas?

Here is another possible reduction. Starting from the formula, construct an hypergraph that has 2n vertices and m hyperedges as follows. For every variable $x_i$ we have the two vertices $[x_i=0]$ and $[x_i=1]$, and, for every clause with $k$ variables, we have the hyperedge that connects the $k$ vertices corresponding to the unique assignment to those $k$ variables that contradicts the clause. For example, the clause
$(x_3 \vee \neg x_5 \vee x_6)$
corresponds to the hyperedge
$([x_3=0],[x_5=1],[x_6=0])$.

Now, if the formula is random, we have a random hypergraph. Also, if the formula is satisfiable we have an independent set of size $n$; half as big as the total number of vertices: just take the vertices consistent with the assignment. (An independent set is a set of vertices such that no hyperedge is completely contained in the set.) Certifying unsatisfiability of a random formula now reduces to certifying that a given random hypergraph has no large independent set.

Unfortunately, we don’t know of any algorithm for this problem, except for the case of graphs. As I may discuss in a future post, spectral methods allow us to certify that a given random graph with $n$ vertices and average degree $d$ has no independent set larger than about $n/O(\sqrt{d})$. By this, I mean that there is a definition of certificate that, when existing, always correctly proves such an upper bound, and when we pick at random a graph of average degree $d$ there is a high probability that a certificate proving an upper bound of $n/O(sqrt{d})$ to the size of the largest independent set exists and can be found efficiently.

It is too bad that the above reduction produces a graph only when we start from 2SAT, a problem for which we already know how to decide (and hence certify) satisfiability in polynomial time.

But, and here is a great idea of Goerdt and Krivelevich from 2000, we can reduce the problem of certifying non-existence of large independent sets in random hypergraps to the problem of certifying non-existence of large independent sets in random graphs.

Suppose we have an hypergraph with n vertices and m hyperedges, each involving 4 vertices. Construct now a graph with $n^2$ vertices, one for every pairs of vertices in the hypergraph, and for every hyperedge $(a,b,c,d)$ in the hypergraph create the edge $([a,b],[c,d])$ in the graph. (Assume for now that we choose the ordering of vertices at random, even if this means that we only achieve a randomized reduction. There are ways to make the reduction deterministic.) Now, if the hypergraph has an independent set of size $\geq t$ then clearly the graph has an independent set of size $\geq t^2$. Furthermore, if we started from a random hypergraph then we are getting a random graph. So if $m$ is of the order of $n^2$ we are able to refute the claim that there is an independent set of size $n/2$ in the hypergraph (by refuting the claim that there is an independent of size $n^2 /4$ in the graph).

In general, for even $k$, these ideas give a way of refuting a random $k$-SAT instance with $n$ variables and $n^{k/2}$ clauses.

(The original paper of Goerdt and Kirvelevich had an extra polylog term needed to make the spectral techniques work. But later more sophisticated analyses have removed the polylog bound, either by using slightly different reductions or by directly improving the bounds on the sparsity of random graphs for which one can certify the non-existence of large independent sets. See this paper by Feige and Ofek for the latter approach.)

Instead of thinking in terms of reductions to graph and hypergraph problems, one may directly see the method as associating a matrix to the formula and proving that certain properties of the matrix imply the unsatisfiability of the formula.

A generalization of this way of seeing the argument has led to an algorithm by Friedman, Goerdt and Krivelevich that certifies unsatisfiability of random kSAT instances with about $n^{k/2}$ clauses even if $k$ is odd. I think it would be interesting to have a combinatorial view of what happens in that algorithm.

This is the state of the art for algorithms that find certificates of unsatisfiability.

There is also some intuition for why $n^{1.5}$ is a natural barrier. The algorithmic techniques described so far are “no more powerful” than semidefinite programming: the standard semidefinite relaxation of Max 2SAT proves that a given 2SAT formula is unsatisfiable, whenever it is the case, and a standard semidefinite programming relaxation of independent set (the Lovasz theta function) proves with high probability that a random graph has no large independent set. It is conjectured, however, that no “simple” reduction of random 3SAT to a semidefinite programming problem yelds a refutation if the number of clauses is less than $n^{1.5}$. This has been verified by Feige and Ofek for a natural reduction.

Recently, Feige, Kim and Ofek have defined a new type of witness of unsatisfiability that is verifiable in polynomial time and that exists with high probability for formulas with about $n^{1.4}$ clauses. (It is not known, however, how to construct such witnesses in polynomial time given a formula.) As could be expected, their witness-verification algorithm employs something that we know how to do in polynomial time but that is very hard for semidefinite programs: verifying the unsatisfiability of a given linear system over GF(2).

In the previous random kSAT post we saw that for every $k$ there is a constant $c_k$ such that

  1. A random kSAT formula with $n$ variables and $m$ clauses is conjectured to be almost surely satisfiable when $m/n c_k + \epsilon$;
  2. There is an algorithm that is conjectured to find satisfying assignments with high probability when given a random kSAT formula with $n$ variables and fewer than $(c_k – \epsilon) n$ clauses.

So, conjecturally, the probability of satisfiability of a random kSAT formula has a sudden jump at a certain threshold value of the ratio of clauses to variables, and in the regime where the formula is likely to be satisfiable, the kSAT problem is easy-on-average.

What about the regime where the formula is likely to be unsatisfiable? Is the problem still easy on average? And what would that exactly mean? The natural question about average-case complexity is: is there an efficient algorithm that, in the unsatisfiable regime, finds with high probability a certifiably correct answer? In other words, is there an algorithm that efficiently delivers a proof of unsatisfiability given a random formula with $m$ clauses and $n$ variables, $m> (c_k + \epsilon) n$?

Some non-trivial algorithms, that I am going to describe shortly, find such unsatisfiability proofs but only in regimes of fairly high density. It is also known that certain broad classes of algorithms fail for all constant densities. It is plausible that finding unsatisfiability proofs for random kSAT formulas with any constant density is an intractable problem. If so, its intractability has a number of interesting consequences, as shown by Feige.

A first observation is that if we have an unsatisfiable 2SAT formula then we can easily prove its unsatisfiability, and so we may try to come with some kind of reduction from 3SAT to 2SAT. In general, this is of course hopeless. But consider a random 3SAT formula $\phi$ with $n$ variables and $10 n^2$ clauses. Now, set $x_1 \leftarrow 0$ in $\phi$, and consider the resulting formula $\phi’$. The variable $x_1$ occurred in about $30 n$ clauses, positively in about $15 n$ of them (which have now become 2SAT clauses in $\phi’$) and negatively in about $15 n$ clauses, that have now disappeared in $\phi’$. Let’s look at the 2SAT clauses of $\phi’$: there are about $15 n$ such clauses, they are random, so they are extremely likely to be unsatisfiable, and, if so, we can easily prove that they are. If the 2SAT subset of $\phi’$ is unsatisfiable, then so is $\phi’$, and so we have a proof of unsatisfiability for $\phi’$.

Now set $x_1 \leftarrow 1$ in $\phi$, thus constructing a new formula $\phi”$. As before, the 2SAT part of $\phi”$ is likely to be unsatisfiable, and, if so, its unsatisfiability is easily provable in polynomial time.

Overall, we have that we can prove that $\phi$ is unsatisfiable when setting $x_1 \leftarrow 0$, and also unsatisfiable when setting $x_1\leftarrow 1$, and so $\phi$ is unsatisfiable.

This works when $m$ is about $n^2$ for 3SAT, and when $m$ is about $n^{k-1}$ for kSAT. By fixing $O(\log n)$ at a time it is possible to shave another polylog factor. These idea is due to Beame, Karp, Pitassi, and Saks.

A limitation of this approach is that it produces polynomial-size resolution proofs of unsatisfiability and, in fact tree-like resolution proofs. It is known that polynomial-size resolution proofs do not exist for random 3SAT formulas with fewer than $n^{1.5-\epsilon}$ clauses, and tree-like resolution proofs do not exist even when the number of clauses is just less than $n^{2-\epsilon}$. This is a limitation that afflicts all backtracking algorithms, and so all approaches of the form “let’s fix some variables, then apply the 2SAT algorithm.” So something really different is needed to make further progress.

Besides the 2SAT algorithm, what other algorithms do we have to prove that no solution exists for a given problem? There are algorithms for linear and semidefinite programming, and there is Gaussian elimination. We’ll see how they can be applied to random kSAT in the next theory post.

Pick a random instance of 3SAT by picking at random $m$ of the possible $8 {n\choose 3}$ clauses that can be constructed over $n$ variables. It is easy to see that if one sets $m=cn$, for a sufficiently large constant $c$, then the formula will be unsatisfiable with very high probability (at least $1-2^n \cdot (7/8)^m$), and it is also possible (but less easy) to see that if $c$ is a sufficiently small constant, then the formula is satisfiable with very high probability.

A number of questions come to mind:

  1. If I plot, for large $n$, the probability that a random 3SAT formula with $n$ variables and $cn$ clauses is satisfiable, against the density $c$, what does the graph look like? We just said the probability is going to be close to 1 for small $c$ and close to $0$ for large $c$, but does it go down smoothly or sharply?

    Here the conjecture, supported by experimental evidence, is that the graph looks like a step function: that there is a constant $c_3$ such that the probability of satisfiability is $1-o_n(1)$ for density $c_3$. A similar behavior is conjectured for kSAT for all $k$, with the threshold value $c_k$ being dependent on $k$.

    Friedgut proved a result that comes quite close to establishing the conjecture.

    For, say, 3SAT, the statement of the conjecture is that there is a value $c_3$ such that for every interval size $\epsilon$, every confidence $\delta$ and every sufficiently large $n$, if you pick a 3SAT formula with $(c_3+\epsilon)n$ clauses and $n$ variables, the probability of satisfiability is at most $\delta$, but if you pick a formula with $(c_3-\epsilon)n$ clauses then the probability of satisfiability is at least $1-\delta$.

    Friedgut proved that for every $n$ there is a density $c_{3,n}$, such that for every interval size $\epsilon$, every confidence $\delta$ and every sufficiently large $n$, if you pick a 3SAT formula with $(c_{3,n}+\epsilon)n$ clauses and $n$ variables, the probability of satisfiability is at most $\delta$, but if you pick a formula with $(c_{3,n}-\epsilon)n$ clauses then the probability of satisfiability is at least $1-\delta$.

    So, for larger and larger $n$, the graph of proability of satisfiability versus density does look more and more like a step function, but Friedgut’s proof does not guarantee that the location of the step stays the same. Of course the location is not going to move, but nobody has been able to prove that yet.

    Semi-rigorous methods (by which I mean, methods where you make things up as you go along) from statistical physics predict the truth of the conjecture and predict a specific value for $c_3$ (and for $c_k$ for each $k$) that agrees with experiments. It remains a long-term challenge to turn these arguments into a rigorous proof.

    For large $k$, work by Achlioptas, Moore, and Peres shows almost matching upper and lower bounds on $c_k$ by a second moment approach. They show that if you pick a random kSAT formula for large $k$ the variance of the number of satisfying assignments of the formula is quite small, and so the formula is likely to be unsatisfiable when the average number of assignments is close to zero (which actually just follows from Markov’s inequality), but also the formula is likely to be satisfiable when the average number of assignments is large. Their methods, however, do not improve previous results for 3SAT. Indeed, it is known that the variance is quite large for 3SAT, and the conjectured location of $c_3$ is not the place where the average number of assignments goes from being small to being large. (The conjectured value of $c_3$ is smaller.)

  2. Pick a random formula with a density that makes it very likely that the formula is satisfiable: is this a distribution of inputs that makes 3SAT hard-on-average?

    Before addressing the question we need to better specify what we mean by hard-on-average (and, complementarily, easy-on-average) in this case. For example, the algorithm that always says “satisfiable” works quite well; over the random choice of the formula, the error probability of the algorithm is extremely small. In such settings, however, what one would like from an algorithm is to produce an actual satisfying assignment. So far, all known lower bounds for $c_3$ are algorithmic, so in the density range in which we rigorously know that a random 3SAT formula is likely to be satisfiable we also know how to produce, with high probability, a satisfying assignment in polynomial time. The results for large $k$, however, are non-constructive and it remains an open question to match them with an algorithmic approach.

    The statistical physics methods that suggest the existence of sharp thresholds also inspired an algorithm (the survey propagation algorithm) that, in experiments, efficiently finds satisfying assignments in the full range of density in which 3SAT formulas are believed to be satisfiable with high probability. It is an exciting, but very difficult, question to rigorously analyze the behavior of this algorithm.

  3. Pick a random formula with a density that makes it very likely that the formula is unsatisfiable: is this a distribution of inputs that makes 3SAT hard-on-average?

    Again, an algorithm that simply says “unsatisfiable” works with high probability. The interesting question, however, is whether there is an algorithm that efficiently and with high probability delivers certificates of unsatisfiability. (Just like the survey propagation algorithm delivers certificates of satisfiability in the density range in which they exist, or so it is conjectured.) This will be the topic of the next post.

a

Follow

Get every new post delivered to your Inbox.

Join 290 other followers