<p>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: </p>

<p>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:</p>

<p>$ + 1^{i} 0,- 1^{j} ,+ 1^{k} $</p>

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

<pre><code>+110-1110+11110
</code></pre>

<p>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.</p>

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

<ul>
<li>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;</li>
<li>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;</li>
<li>then the second head can return to the rightmost cell;</li>
<li>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.</li>
</ul>

<p>Example:</p>

<pre><code>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)
</code></pre>

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

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

<p>($\text{+++}$ marks the end of the formula)</p>

<p>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.</p>

CC BY-SA 3.0
2015-10-26T00:05:17.120Z
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
CC BY-SA 3.0
2015-10-26T00:08:09.750Z
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
CC BY-SA 3.0
2015-10-26T10:45:59.390Z
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
CC BY-SA 3.0
2015-10-26T11:56:25.530Z
@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
CC BY-SA 3.0
2015-10-26T15:46:53.830Z
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
CC BY-SA 4.0
2021-11-28T10:22:39.237Z
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
CC BY-SA 3.0
2015-10-23T09:39:25.823Z
2015-10-23T09:54:57.840Z
2015-10-23T09:54:57.840Z
Marzio De Biasi
<p>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.</p>

<p>According to <a href="http://www.sciencedirect.com/science/article/pii/S0304397509006264" rel="nofollow">this paper</a> (Theorem 4.1), the class of regular languages $REG$ <em>is exactly</em> 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.</p>

CC BY-SA 3.0
2015-10-22T22:57:59.507Z
This is great!  Thank you very much.  But, I am most interested in the two-tape case.  :)
Michael Wehar
CC BY-SA 3.0
2015-10-22T23:10:49.273Z
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
CC BY-SA 3.0
2015-10-22T21:38:53.420Z
2015-10-23T07:58:16.987Z
2015-10-23T07:58:16.987Z
Boson
<p>The decision problem CNF-SAT can be described as follows:</p>

<p><strong>Input:</strong> A boolean formula $\phi$ in conjunctive normal form.</p>

<p><strong>Question:</strong> Does there exist a variable assignment that satisfies $\phi$?</p>

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

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

<p><strong>Question:</strong> Is there an NTM that solves CNF-SAT in $O(n)$ steps?</p>

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

CC BY-SA 3.0
2015-10-22T11:00:06.357Z
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
CC BY-SA 3.0
2015-10-22T11:06:15.793Z
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
CC BY-SA 3.0
2015-10-22T15:00:44.580Z
@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
CC BY-SA 3.0
2015-10-22T15:31:34.840Z
@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
CC BY-SA 3.0
2015-10-22T15:36:38.400Z
@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
CC BY-SA 3.0
2015-10-22T19:37:02.897Z
@Kaveh Now I see what I was missing. Thanks for pointing that out.
Boson
CC BY-SA 3.0
2015-10-22T20:08:25.127Z
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
CC BY-SA 3.0
2015-10-22T20:36:43.907Z
@MarzioDeBiasi That's very interesting!!  Thank you very much for pointing that out.  :)
Michael Wehar
CC BY-SA 3.0
2015-10-23T05:01:59.473Z
@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
CC BY-SA 3.0
2015-10-23T08:03:48.457Z
@MarzioDeBiasi Your remark seems to be a legitimate answer to the question. Maybe make it a proper answer instead of comment?
Boson
CC BY-SA 3.0
2015-10-23T16:05:09.373Z
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 Steinke
CC BY-SA 3.0
2015-10-23T16:14:45.753Z
@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
CC BY-SA 3.0
2015-10-23T16:17:42.173Z
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 Steinke
CC BY-SA 3.0
2015-10-23T17:52:33.243Z
@Thomas: perhaps you can also add the constraint that each variable appears at most twice ... the problem shouldn't be easier.
Marzio De Biasi
CC BY-SA 3.0
2015-10-25T20:53:00.237Z
@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
CC BY-SA 3.0
2015-10-26T17:19:09.593Z
@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 Steinke
<time-complexity><sat><turing-machines><np><nondeterminism>
Is there a non-deterministic linear time algorithm for CNF-SAT?
Michael Wehar
# Is there a non-deterministic linear time algorithm for CNF-SAT?

(Asked by: username_0 on 2015-10-22)

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.

**Tags:** time-complexity, sat, turing-machines, np, nondeterminism

> **Comments:**
> **username_1**: 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.)  
> **username_2**: 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$?  
> **username_3**: @username_2, 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.  
> **username_0**: @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.  :)  
> **username_0**: @username_2 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.  :)  
> **username_2**: @username_3 Now I see what I was missing. Thanks for pointing that out.  
> **username_4**: 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  
> **username_0**: @MarzioDeBiasi That's very interesting!!  Thank you very much for pointing that out.  :)  
> **username_5**: @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.  
> **username_2**: @MarzioDeBiasi Your remark seems to be a legitimate answer to the question. Maybe make it a proper answer instead of comment?  
> **username_6**: 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?  
> **username_0**: @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.  :)  
> **username_6**: 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?  
> **username_4**: @Thomas: perhaps you can also add the constraint that each variable appears at most twice ... the problem shouldn't be easier.  
> **username_4**: @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$  
> **username_6**: @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.  

---

## 2 answers

### Answer by username_4 on 2015-10-23. Score: 7

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.

> **Comments:**
> **username_1**: 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.  
> **username_1**: 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.  
> **username_1**: 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.  
> **username_4**: @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.  
> **username_1**: 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).  
> **username_7**: 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$?  

---

### Answer by username_2 on 2015-10-22. Score: 3

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](http://www.sciencedirect.com/science/article/pii/S0304397509006264) (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.

> **Comments:**
> **username_0**: This is great!  Thank you very much.  But, I am most interested in the two-tape case.  :)  
> **username_3**: 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).  

---

