19
$\begingroup$

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.

Improve this question
$\endgroup$
16
  • 5
    $\begingroup$ 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.) $\endgroup$
    – András Salamon
    Oct 22, 2015 at 11:00
  • 5
    $\begingroup$ @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. $\endgroup$
    – Kaveh
    Oct 22, 2015 at 15:00
  • 4
    $\begingroup$ @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. :) $\endgroup$
    – Michael Wehar
    Oct 22, 2015 at 15:36
  • 5
    $\begingroup$ 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 $\endgroup$
    – Marzio De Biasi
    Oct 22, 2015 at 20:08
  • 3
    $\begingroup$ @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. $\endgroup$
    – Ryan Williams
    Oct 23, 2015 at 5:01

2 Answers 2

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
6
  • 1
    $\begingroup$ 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. $\endgroup$
    – András Salamon
    Oct 26, 2015 at 0:05
  • 2
    $\begingroup$ 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. $\endgroup$
    – András Salamon
    Oct 26, 2015 at 0:08
  • 1
    $\begingroup$ 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. $\endgroup$
    – András Salamon
    Oct 26, 2015 at 10:45
  • 1
    $\begingroup$ @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. $\endgroup$
    – Marzio De Biasi
    Oct 26, 2015 at 11:56
  • 1
    $\begingroup$ 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). $\endgroup$
    – András Salamon
    Oct 26, 2015 at 15:46
2
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 5
    $\begingroup$ 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.) $\;\;\;\;$ $\endgroup$
    – user6973
    Oct 22, 2015 at 21:49
  • $\begingroup$ This is great! Thank you very much. But, I am most interested in the two-tape case. :) $\endgroup$
    – Michael Wehar
    Oct 22, 2015 at 22:57
  • 2
    $\begingroup$ 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). $\endgroup$
    – Kaveh
    Oct 22, 2015 at 23:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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