Is there a non-deterministic linear time algorithm for CNF-SAT?

Question

The decision problem CNF-SAT can be described as follows:

Input: A boolean formula $\phi$ in conjunctive normal form.

Question: Does there exist a variable assignment that satisfies $\phi$?

I'm considering several different approaches for solving CNF-SAT with a non-deterministic two-tape Turing machine.

I believe that there is an NTM that solves CNF-SAT in $n \cdot \texttt{poly}(\log(n))$ steps.

Question: Is there an NTM that solves CNF-SAT in $O(n)$ steps?

Any relevant references are appreciated even if they only provide near linear time non-deterministic approaches.

Santhanam in 2001 wrote: "SAT $\in$ NTIME($n$ polylog$(n)$), a result that follows from the facts that SAT can be accepted in $n$polylog$(n)$ time on an NRAM and that there is an efficient simulation of NRAMs by NTMs, due to Gurevich and Shelah." So it seems unlikely to me that SAT $\in$ NTIME($n$) is known. (The reference is to LNCS 363 from 1989.) — András Salamon, Oct 22 '15 at 11:00
I do not understand your question. By non-deterministically guessing a satisfying assignment and checking it, an NTM solves CNF-SAT. The guessing and checking are both in linear time wrt to the size of the input formula. What am I missing? Is not $n$ the size of $\phi$? — Boson, Oct 22 '15 at 11:06
@Boson, assume that you are given not just a satisfying assignment but also a complete computation of the formula. How would you check if it is a valid computation in linear time? It is not clear even you can do it for 3CNF-SAT because you have to jump around to look up the assignment to the variables. — Kaveh, Oct 22 '15 at 15:00
@AndrásSalamon Very interesting!! Also, there is an approach where you guess one literal from each clause and then sort all of the guessed literals. Then, you scan through the literals and make sure that no positive and negative literals for the same variable are next to each other in the sorted list. :) — Michael Wehar, Oct 22 '15 at 15:31
@Boson It's not clear if you can verify that the assignment satisfies the formula in linear time with a two-tape TM. You would likely have to move the tape head back and forth many times. If you have an efficient approach for this verification, please let me know. :) — Michael Wehar, Oct 22 '15 at 15:36
@Kaveh Now I see what I was missing. Thanks for pointing that out. — Boson, Oct 22 '15 at 19:37
Just a note: if variables are represented in unary (SAT is still NPC), then there is a two-tapes NTM that recognizes an unary satisfiable formula $\varphi$ in $2|\varphi|$ steps — Marzio De Biasi, Oct 22 '15 at 20:08
@MarzioDeBiasi That's very interesting!! Thank you very much for pointing that out. :) — Michael Wehar, Oct 22 '15 at 20:36
@MichaelWehar if you use a counting sort, you can sort n keys in the range [0,k] in time O(n+k) in a reasonable random access model (e.g. Random access Turing machine, where you can take O(log n) time to write down an index, then can jump to that index of the tape in 1 step). If you encode each literal as an (log n+1) bit string, then the total number of clauses and variables is at most O(n/log n), in which case O(log n)-time operations on all the literals are fine. Extending to two tape TM is not straightforward, at least with counting sort. — Ryan Williams, Oct 23 '15 at 05:01
@MarzioDeBiasi Your remark seems to be a legitimate answer to the question. Maybe make it a proper answer instead of comment? — Boson, Oct 23 '15 at 08:03
I can construct a 3-tape NTM that solves CNF-SAT in $O(|\varphi| \log |\varphi|)$-time. It "feels like" it would be impossible to do better than this.
Note that the representation is important. I'm assuming that a $m$-literal $n$-variable CNF $\varphi$ is represented in the obvious way using $|\varphi|=\Theta(m \log n)$ bits. Is that the representation you had in mind? — Thomas, Oct 23 '15 at 16:05
@Thomas Yep, that's the representation that I originally had in mind. You might be able to do $O(\vert \phi \vert \log(\vert \phi \vert))$ with a 2-tape, but I'm not totally sure. Thanks for the comment. :) — Michael Wehar, Oct 23 '15 at 16:14
Here's a simpler question that is equivalent to your question: Given a conjunction $\phi$ with $m$ literals on $n$ variables (represented in the natural way using $|\phi|=\Theta(m \log n)$ bits), is there a $O(|\phi|)$-time NTM that accepts iff $\phi$ is satisfiable? — Thomas, Oct 23 '15 at 16:17
@Thomas: perhaps you can also add the constraint that each variable appears at most twice ... the problem shouldn't be easier. — Marzio De Biasi, Oct 23 '15 at 17:52
@Thomas: notice that a simple conjunction $\phi$ falls in $co$-$NTIME(n)$: in order to decide that it is unsatisfiable just guess the position of $x_i$ and $\neg x_i$ — Marzio De Biasi, Oct 25 '15 at 20:53
@MarzioDeBiasi Yes so we have a linear-time $\Sigma_2$-TM. Next question: Can we come up with a linear-time randomized verifier i.e. linear-time $MA$? Perhaps some sort of hashing can be used to determine whether a conjunction contains both $x_i$ and $\overline{x_i}$ in linear time. — Thomas, Oct 26 '15 at 17:19

Marzio De Biasi · Answer 1 · 2015-10-23T09:54:57.840

This is only an extended comment. A few times ago I asked (myself :-) how fast a multitape NTM that accepts a (reasonably encoded) NP-complete language can be. I came up with this idea:

3-SAT remains NP-complete even if variables are represented in unary. In particular we can convert a clause - suppose $(x_i \lor \neg x_j \lor x_k)$ - of an arbitrary 3-SAT formula $\varphi$ on $n$ variables and $m$ clauses in a sequence of characters over alphabet $\Sigma = \{ +, -, 1 \}$ in which every variable occurrence is represented in unary:

$ + 1^{i} 0,- 1^{j} ,+ 1^{k} $

For example, $(x_2 \lor -x3 \lor +4)$ can be converted to:

+110-1110+11110

So we can convert a 3-SAT formula $\varphi_i$ in an equivalent string $U(\varphi_i)$ concatenating its clauses. The language $L_U = \{ U(\varphi_i) \mid \varphi_i \in 3-SAT \}$ is NP-complete.

A 2-tape NTM can decide if a string $x \in L_U$ in time $2|x|$ in this way.

the first head scans the input from left to right and with the internal logic it keeps track when it enters or exit a clause or reach the end of the formula. Whenever it finds a $+$ or $-$, the second head starts moving right with it on the $1^i$ that represents $x_i$. At the end of $1^i$, if the second head is on a $0$ then it guesses a truth value $+$ or $-$ (it makes an assignment) and writes it on the second tape; if it finds a $+$ or $-$ then that variable has already been assigned a value;
in both cases, using the internal logic, the NTM matches the truth value under the second head (the assignment) with the last seen $+$ or $-$; if they match then the clause is satisfied;
then the second head can return to the rightmost cell;
with the internal logic the NTM can keep track if all clauses are satisfied while the first head moves towards the end of the input.

Example:

Tape 1 (formula)    Tape 2 (variable assignments)
+110-1110+11110...  0000000000000...
^                   ^
+110-1110+11110...  0000000000000...
 ^                  ^
+110-1110+11110...  0000000000000...
  ^                  ^
+110-1110+11110...  0+00000000000... first guess set x2=T; matches +
  ^                  ^               so remember that current clause is satisfied
+110-1110+11110...  0+00000000000... 
  ^                  ^
...
+110-1110+11110...  0+00000000000... 
    ^               ^
...
+110-1110+11110...  0++0000000000... second guess set x3=T
       ^              ^              don't reject because current
                                     clause is satisfied (and in every
                                     case another literal must be parsed)

The time can be reduced to $|x|$ if we add some redundant symbols to the clause representation:

$ + 1^{i} 0^i,- 1^{j} 0^j ,+ 1^{k} 0^k \; ... \; \text{+++}$

($\text{+++}$ marks the end of the formula)

In this way the second head can return to the leftmost cell while the first scans the $0^i$ part. Using $\text{++}$ as a clause delimiter and $\text{+++}$ as a marker for the end of the formula we can use same representation for CNF formulas with an arbitrary number of literals per clause.

The unary representation is unambiguous, so one can use 0/1 for +/-, giving 011011110111110 for your first example. 00 then serves as end-of-clause marker, as 000 cannot otherwise occur (if 00 occurs, then it is the end marker of a variable and the next sign, so the next symbol must be 1). The single worktape contains the guessed $v$-bit assignment to the $v$ variables. When a variable is read the worktape head moves forward and is then moved back to the beginning when the 0 is seen, so at most $2$ steps for each bit of the input. — András Salamon, Oct 26 '15 at 00:05
In other words, even an NDTM with a one-way input tape and a single worktape uses at most $2n$ steps for Unary SAT encoded with a Boolean alphabet. — András Salamon, Oct 26 '15 at 00:08
To make things even tidier, one can further require that the input first contains a prefix with the number of variables $v$ specified in unary. This allows the guess to be built while reading the prefix. This is then a kind of "unary SATLIB" encoding, of size at most quadratic in a standard SAT instance, as long as each variable appears at least once in the formula and the variables are numbered 0 to $v-1$. These seem to be reasonable requirements. — András Salamon, Oct 26 '15 at 10:45
@AndrásSalamon: good! Fixing the encoding and the model (one way read tape + 2-way work tape) we get a worst runtime of $2n - c$ on inputs of size $n$, where $c$ can be made arbitrarily large embedding some fixed storage in the TM internal logic. It could be interesting to investigate if something can be proved using the one-wayness of the input-tape and a crossing-section argument. — Marzio De Biasi, Oct 26 '15 at 11:56
Yes, as far as I can tell the time-space product for Unary SAT is something like $\Theta(n\sqrt{n})$ by a standard argument. The unary representation of variables avoids the gap between the best known $\Omega(n^2/(\log n)^{1+\varepsilon})$ lower bound and a straightforward $O(n^3/(\log n)^{\varepsilon'})$ upper bound for CNF-SAT (although a better algorithm in that case might then also reduce the gap). — András Salamon, Oct 26 '15 at 15:46
Hello. If we have NTM $M$ that decide $SAT$, as an black box, how it possible use it to decide $CNF$ with $n$ variable such that we use a most $2n+1$ times $M$? — ErroR, Nov 28 '21 at 10:22

Boson · Answer 2 · 2015-10-23T07:58:16.987

2

Not exactly what your looking for, but for 1-tape NTM, the answer seems to be negative: SAT is not solvable by a 1-tape NTM in non-deterministic linear time.

According to this paper (Theorem 4.1), the class of regular languages $REG$ is exactly the class of languages recognized by a 1-tape NTM in time $o(n \log(n))$. Thus, if there existed a 1-tape NTM solving SAT in time $o(n \log(n))$, then SAT (more precisely, the set of satisfiable formulae in CNF) would be a regular language, hence solvable in deterministic constant space.

edited Oct 23 '15 at 07:58

answered Oct 22 '15 at 21:38

Boson

560
3
9

5

That theorem is only about one-head Turing machines. $:$ (For example, two-head Turing machines can easily decide the palindrome language in linear time and constant space.) $;;;;$ – Oct 22 '15 at 21:49
This is great! Thank you very much. But, I am most interested in the two-tape case. :) – Michael Wehar Oct 22 '15 at 22:57
2

As @Ricky wrote. AFAIK it is still consistent with what we know that SAT is in deterministic linear time. To prove otherwise you would need a superlinear time lower bound for SAT and we don't have one (don't seem to be close to one). – Kaveh Oct 22 '15 at 23:10

Is there a non-deterministic linear time algorithm for CNF-SAT?

2 Answers2