6
$\begingroup$

CNF-SAT refers to the following problem:

Given a boolean formula $\phi$ in conjunctive normal form, does there exist an assignment to the variables that satisfies $\phi$.

There are several parameters that one can associate with $\phi$:

  • $n$ will denote the number of variables in $\phi$.
  • $m$ will denote the number of clauses in $\phi$.
  • $N$ will denote the number of variable occurrences in $\phi$.

Claim: For every fixed $k$, we can reduce an arbitrary instance $\phi$ of CNF-SAT to an instance $G$ of $k$-Clique with roughly $2^{\frac{N}{k}}$ vertices and $2^{\frac{2 N}{k}}$ edges.

Proof Idea: Any clause in $\phi$ can be split into two clauses by adding an additional variable. The positive literal gets added to one of the new clauses and the negative literal gets added to the other new clause.

We make at most $k$ splits to the clauses of $\phi$ to get a new formula $\phi'$ such that:

  • $\phi'$ has at most $N+2k$ variable occurrences.
  • $\phi'$ can be expressed as $\bigwedge_{i\in[k]} \phi_{i}'$ where each $\phi_{i}'$ is a CNF formula with at most $\frac{N}{k} + 2$ variable occurrences.
  • $\phi$ is satisfiable if and only if $\phi'$ is satisfiable.

We can look at each $\phi_{i}'$ independently and build up a list of all the satisfying assignments. There are at most $2^{\frac{N}{k}+2}$ satisfying assignments for each $\phi_{i}'$.

The satisfying assignments for the $\phi_i'$'s will represent the vertices of the graph $G$. In total, $G$ will have at most $k \cdot 2^{\frac{N}{k}+2}$ vertices.

Vertices $v$ and $u$ are adjacent in $G$ if the following are true:

  • $v$ and $u$ represent assignments for $\phi_i'$ and $\phi_j'$ respectively where $i \neq j$.
  • For the variables that are in both $\phi_i'$ and $\phi_j'$, the assignments for $v$ and $u$ agree on their respective bit values.

Now, if a $k$-Clique exists in $G$, then we get an assignment for each $\phi_i'$ where no two assignments disagree on bit values for the same variables. As a result, these assignments can be joined to form a satisfying assignment for $\phi'$.

Conversely, if a satisfying assignment exists for $\phi'$, then we can remove variables from this assignment to get a satsfying assignment for each of the $\phi_i'$'s where no two assignments have any bit mismatches making them form a $k$-Clique in $G$. $\square$

Using fast matrix multiplication, we can solve $k$-Clique in $O(n^{.792 k})$ time. Therefore, we can solve CNF-SAT in $2^{.792 N}$ time. In fact, there is a trivial algorithm for solving CNF-SAT in $2^{.5 N}$ time.

However, it is not known if we can solve CNF-SAT in $poly(N) \cdot 2^{(1-\epsilon) \cdot n}$ time.

Question: Does there exist a constant $c$ such that for every fixed $k$, we can reduce an arbitrary instance $\phi$ of CNF-SAT to an instance $G$ of $k$-Clique with roughly $2^{\frac{c \cdot n}{k}}$ vertices and $2^{\frac{2 \cdot c \cdot n}{k}}$ edges.

Relevant Links:

$\endgroup$
  • 3
    $\begingroup$ What and where is the quantifier on $\alpha$ in questions 2 and 3? ​ ​ $\endgroup$ – user6973 Mar 19 '16 at 15:15
  • $\begingroup$ @RickyDemer Thanks for the question. The quantifiers are as follows: $\exists c \, \forall k \, \forall \alpha$ $\endgroup$ – Michael Wehar Mar 19 '16 at 15:26
  • 1
    $\begingroup$ If "roughly" is at least as rough as "within a O(k) factor of", then the number of edges is without loss of generality, since one can do disconnected union with a Turán graph. ​ ​ $\endgroup$ – user6973 Mar 20 '16 at 9:52
  • 1
    $\begingroup$ Is N the quantity that is usually referred to as the number of literals? $\endgroup$ – András Salamon Mar 20 '16 at 22:10
  • 1
    $\begingroup$ Note that if you are parameterizing by $n$ rather than instance size, then there is a trivial $n.2^n$ time lower bound, since the $n$-variable instances containing only non-repeated full clauses (in which every variable occurs once) require at least this much time just to read the input, in the worst case of the unique unsatisfiable such formula. So some care is required in the precise formulation. $\endgroup$ – András Salamon Mar 23 '16 at 19:44
10
$\begingroup$

I don't know the answer to your specific question (it seems related to the question of whether W1=W[2]).

But the algorithm you give in your question is subsumed by several other results. Using your definition of $N$, CNF-SAT is basically solvable in $O(1.1279^N)$ time, as in the paper by Wahlstrom (link goes to a google scholar page of papers that cite it). In particular, Wahlstrom shows that if $d$ is the average number of occurrences of a variable in the CNF, and no variable appears at most once, then CNF-SAT can be solved in $O(1.1279^{n(d - 2)})$ time. (There are other references with similarly strong running times.)

Update: Another reference is:

Hirsch, E.A.: New worst-case upper bounds for SAT. J. Autom. Reason. 24(4), 397–420 (2000)

This gives faster algorithms in terms of $m$ and your $N$ (which is typically called $\ell$). Namely, Hirsch gets $2^{0.30897m}$ and $2^{0.10299\ell}$ time.

$\endgroup$
  • $\begingroup$ Thank you very much for the link. I appreciate it! Also, I think your suggestion that it may be related to W[1] vs W[2] is a good insight. By the way, can we solve CNF-SAT in $poly(N) \cdot 2^{(1-\epsilon) \cdot m}$ time? $\endgroup$ – Michael Wehar Mar 21 '16 at 1:34
  • 4
    $\begingroup$ Yes, you can combine backtracking and dynamic programming to solve the problem in about $1.8^m$ time. $\endgroup$ – Ryan Williams Mar 21 '16 at 6:54
  • $\begingroup$ After reading more, it seems that this question is related to M[1] vs W[2]. I'm still trying to learn more about the M hierarchy, but it's worth noting that M[1] $\subseteq$ W[1]. One relevant source to look at is "A Basic Parameterized Complexity Primer". Please feel free to suggest more references that discuss the M hierarchy. $\endgroup$ – Michael Wehar Apr 9 '16 at 17:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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