Search

The PPSZ algorithm by Paturi, Pudlak, Saks, and Zane [J. ACM, 52 (2005), pp. 337--364] is the fastest known algorithm for Unique $k$-SAT, where the input formula does not have more than one satisfying assignment. For $k\geq 5$ the same bounds hold for general $k$-SAT. We show that this is also the case for k=3,4, using a slightly modified PPSZ algorithm. We do the analysis by defining a cost for satisfiable conjunctive normal form formulas, which we prove to decrease in each PPSZ step by a certain amount. This improves our previous best bounds with Moser and Scheder [Proceedings of STACS, 2011, pp. 237--248] for 3-SAT to $O(1.308^n)$ and for 4-SAT to $O(1.469^n)$. Furthermore, our analysis is much simpler than the existing analysis of PPSZ for general $k$-SAT.

Given the prime conjunctive normal form (CNF) representation $\phi$ of a monotone Boolean function $f:\{0,1\}^n\to\{0,1\}$, the dualization problem calls for finding the corresponding prime disjunctive normal form representation $\psi$ of $f$. A very simple method works by multiplying out the clauses of $\phi$ from left to right in some order, simplifying whenever possible by using the absorption law. We show that for any monotone CNF $\phi$, left-to-right multiplication can be done in subexponential time, and for many interesting subclasses of monotone CNFs such as those with bounded size, bounded degree, bounded intersection, bounded conformality, and read-once formula, it can be done in polynomial or quasi-polynomial time.

The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of clauses kept in memory simultaneously if the proof is only allowed to infer new clauses from clauses currently in memory. Both of these measures have previously been studied and related to the resolution refutation size of unsatisfiable conjunctive normal form (CNF) formulas. Also, the minimum refutation space of a formula has been proven to be at least as large as the minimum refutation width, but it has been open whether space can be separated from width or the two measures coincide asymptotically. We prove that there is a family of $k$-CNF formulas for which the refutation width in resolution is constant but the refutation space is nonconstant, thus solving a problem mentioned in several previous papers.

We show that any $k$-wise independent probability distribution on $\{0,1\}^n$ $O(m^{2.2}$ $2^{-\sqrt{k}/10})$-fools any boolean function computable by an $m$-clause disjunctive normal form (DNF) (or conjunctive normal form (CNF)) formula on $n$ variables. Thus, for each constant $e>0$, there is a constant $c>0$ such that any boolean function computable by an $m$-clause DNF (or CNF) formula is $m^{-e}$-fooled by any $c\log^2m$-wise probability distribution. This resolves up to an $O(\log m)$ factor the depth-2 circuit case of a conjecture due to Linial and Nisan [Combinatorica, 10 (1990), pp. 349-365]. The result is equivalent to a new characterization of DNF (or CNF) formulas by low degree polynomials. It implies a similar statement for probability distributions with the small bias property. Using known explicit constructions of small probability spaces having the limited independence property or the small bias property, we directly obtain a large class of explicit pseudorandom generators of $O(\log^2m\log n)$-seed length for $m$-clause DNF (or CNF) formulas on $n$ variables, improving previously known seed lengths.

We prove that an $\omega(\log^4 n)$ lower bound for the three-party number-on-the-forehead (NOF) communication complexity of the set-disjointness function implies an $n^{\omega(1)}$ size lower bound for treelike Lovasz-Schrijver systems that refute unsatisfiable formulas in conjunctive normal form (CNFs). More generally, we prove that an $n^{\Omega(1)}$ lower bound for the $(k+1)$-party NOF communication complexity of set disjointness implies a $2^{n^{\Omega(1)}}$ size lower bound for all treelike proof systems whose formulas are degree $k$ polynomial inequalities.

We consider several problems related to the use of resolution-based methods for determining whether a given boolean formula in conjunctive normal form is satisfiable. First, building on the work of Clegg, Edmonds, and Impagliazzo in [Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, Philadelphia, PA, 1996, ACM, New York, 1996, pp. 174--183], we give an algorithm for unsatisfiability that when given an unsatisfiable formula of F finds a resolution proof of F. The runtime of our algorithm is subexponential in the size of the shortest resolution proof of F. Next, we investigate a class of backtrack search algorithms for producing resolution refutations of unsatisfiability, commonly known as Davis--Putnam procedures, and provide the first asymptotically tight average-case complexity analysis for their behavior on random formulas. In particular, for a simple algorithm in this class, called ordered DLL, we prove that the running time of the algorithm on a randomly generated k-CNF formula with n variables and m clauses is $2^{\Theta(n(n/m)^{1/(k-2)})}$ with probability $1-o(1)$. Finally, we give new lower bounds on $\mbox{res}(F)$, the size of the smallest resolution refutation of F, for a class of formulas representing the pigeonhole principle and for randomly generated formulas. For random formulas, Chvatal and Szemeredi [J. ACM, 35 (1988), pp. 759--768] had shown that random 3-CNF formulas with a linear number of clauses require exponential size resolution proofs, and Fu [On the Complexity of Proof Systems, Ph. D. thesis, University of Toronto, Toronto, ON, Canada, 1995] extended their results to k-CNF formulas. These proofs apply only when the number of clauses is $\Omega(n \log n)$. We show that a lower bound of the form $2^{n^{\gamma}}$ holds with high probability even when the number of clauses is $n^{(k+2)/4-\epsilon}$.

Given a partially defined Boolean function (pdBf) (T,F), we investigate in this paper how to find a Horn extension $f: \{0,1\}^n \mapsto \{0,1\}$, which is consistent with (T,F), where $T \subseteq \{0,1\}^n$ denotes a set of true Boolean vectors (or positive examples) and $F \subseteq \{0,1\}^n$ denotes a set of false Boolean vectors (or negative examples). Given a pdBf (T,F), it is known that the existence of a Horn extension can be checked in polynomial time. As there are many Horn extensions, however, we consider those extensions f which have maximal and minimal sets T(f) of the true vectors of f, respectively. For a pdBf (T,F), there always exists the unique maximal (i.e., maximum) Horn extension, but there are in general many minimal Horn extensions. We first show that a polynomial time membership oracle can be constructed for the maximum extension, even if its disjunctive normal form (DNF) can be very long. Our main contribution is to show that checking if a given Horn DNF represents a minimal extension and generating a Horn DNF of a minimal Horn extension can both be done in polynomial time. We also can check in polynomial time if a pdBf (T,F) has the unique minimal Horn extension. However, the problems of finding a Horn extension f with the smallest |T(f)| and of obtaining a Horn DNF, whose number of literals is smallest, are both NP-hard.

We study the complexity of telling whether a set of bit-vectors represents the set of all satisfying truth assignments of a Boolean expression of a certain type. We show that the problem is coNP-complete when the expression is required to be in conjunctive normal form with three literals per clause (3CNF). We also prove a dichotomy theorem analogous to the classical one by Schaefer, stating that, unless P=NP, the problem can be solved in polynomial time if and only if the clauses allowed are all Horn, or all anti-Horn, or all 2CNF, or all equivalent to equations modulo two.

This paper associates a linear programming problem (LP) to any conjunctive normal form $\gf$, and shows that the optimum value $Z(\gf)$ of this LP measures the complexity of the corresponding SAT (Boolean satisfiability) problem. More precisely, there is an algorithm for SAT that runs in polynomial time on the class of satisfiability problems satisfying $Z(\gf)\leq 1+\frac{c\log n}{n}$ for a fixed constant $c$, where $n$ is the number of variables. In contrast, for any fixed $\beta

Let I be an algebraic integer ring. The decision problem of the solvability of diophantine equations with parameters in I is proved to be co-NP-complete. However, the decision problem of the solvability of diophantine equations with parameters in all algebraic integer rings is in P. Let $\varphi (x.y)$ be a quantifier-free arithmetical formula in conjunctive normal form or disjunctive normal form. The decision problem of the sentences of the form $\exists x\forall y\varphi (x,y)$, true in I, is NP-complete. Then the decision problem of the sentences of the form $\forall x\exists y\varphi (x,y)$, true in I, is co-NP-complete, whereas the decision problem of the sentences of the form $\forall x\exists y\varphi (x,y)$, true in all algebraic integer rings, is in P. Some other related decision problems are also proven to be in P.

For a simple parameterized model of conjunctive normal form predicates, we show that a simplified version of the Davis–Putnam procedure can, for many values of the parameters, solve the satisfiability problem in polynomial average time. Let v be the number of variables, $t(v)$ the number of clauses in a predicate, and $p(v)$ the probability that a given literal appears in a clause ($p(v)$ is the same for all literals). Let $\varepsilon $ be any small positive constant and n any large positive integer. Then a version of the Davis–Putnam procedure that uses only backtracking and the pure literal rule uses average time that is polynomial in the problem size when any of the following conditions are true for large v. (1) $t(v) \leqq n\ln v$; (2) $t(v) \geqq \exp (\varepsilon v)$; (3) $p(v) \geqq \varepsilon $; or (4) $p(v) \leqq n (\ln v/ v)^{3/2} $. Until recently the best previous bounds for cases (1) and (4) were $t(v) \leqq (\ln\ln v)/(\ln3)$ and $p(v) \leqq \exp ( - v\ln \ln v)$. These results show that t...