Constraints

15 April 2010

k-ISOLATED SAT

Filed under: Commentary,Question — András Salamon @ 13:29
Tags:

How fast can one decide if a SAT instance has an isolated solution?

A while back I asked whether there are any natural problems that are in {NTIME(N^{k+1})} but not in {NTIME(N^k)}.

Consider the following parameterized decision problem, with parameter {k}.

k-ISOLATED SAT
Input: SAT instance with {m} clauses and {n} variables, of size {N} bits
Question: is there a satisfying assignment {x}, such that every assignment {x' \ne x} which has at most {k} bits different from {x} is a falsifying assignment?

If you prefer problems with a logical flavour, think of the SAT instance as a propositional formula in CNF. k-ISOLATED SAT then requires deciding if there is a solution to the formula that is isolated, with any other solution being Hamming distance more than {k} away.

This is a modification of k-FLIP SAT defined in Stefan Szeider‘s paper The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT. For k-FLIP SAT, an initial assignment {x} is given as part of the input, and the question is whether there is a satisfying assignment {x'} at most Hamming distance {k} from {x}. For any given {k}, Stefan’s problem is in {DTIME(N.n^k),} and is FPT for bounded clause size.

k-FLIP SAT requires a solution within a specified {k}-ball, while k-ISOLATED SAT needs to establish a {k}-ball centred on some solution but otherwise clear of solutions.

k-FLIP SAT is not hard enough for the purpose of investigating the nondeterministic time hierarchy. But while it may not be hard enough overall, it does have the useful property that its polynomial runtime bound probably has degree at least {\Omega(k).}

More precisely k-FLIP SAT is {W_l[2]}-hard in general, so by Theorems 5.2 and 5.4 of Chen, Huang, Kanj, and Xia’s paper Strong computational lower bounds via parameterized complexity it is not in {DTIME(n^{o(k)}N^{O(1)})} unless W[1] = FPT. ({W_l[2]}-hardness follows immediately from Stefan’s proof of {W[2]}-hardness, since the reduction is linear.) W[1] = FPT is regarded as unlikely, at least according to current fashion, as this would imply that the Exponential Time Hypothesis fails.

From a descriptive complexity perspective, k-ISOLATED SAT seems harder than k-FLIP SAT. The initial guess amounts to the presence of an additional existential quantifier, and the requirement for a ball of non-solutions seems to force a subformula that requires at least {k} variables to express. Both these conditions are associated with increased complexity.

Here is the first question:

Question 1 Is k-ISOLATED SAT W[2]-hard?

A guess for k-ISOLATED SAT can clearly be verified in time that is polynomial in the input size but with the degree of the polynomial depending on {k}. So for constant {k}, it is in something like {NTIME(N.n^k)}, and hence also in NP. As 0-ISOLATED SAT is just SAT, k-ISOLATED SAT is NP-complete.

On the other hand, there doesn’t seem to be any simple way to verify faster than the obvious procedure. k-ISOLATED SAT then seems like a candidate for a problem in {NTIME(N^{k+1}) \setminus NTIME(N^k)}.

Can one do better than guessing an assignment, then exhaustively checking its neighbourhood? This leads to another question.

Question 2 Is k-ISOLATED SAT in {NTIME(N^k)}?

In the guess-and-verify paradigm, the idea is to guess a candidate solution and then to verify that it is actually a solution, repeating until a solution is found. When the density of solutions in an instance is reasonably high, then this method can work well even for problems with extremely high worst-case complexity, such as problems that are 2-EXPTIME-hard. Problems not in {NTIME(N^k)} are especially interesting in this context: they are hard for guess-and-verify, even if the number of solutions of an instance is large.

Advertisements

1 Comment »

  1. […] I discussed k-ISOLATED SAT, the decision problem which attempts to ramp up the hardness of SAT by requiring not only a […]

    Pingback by A simple reduction « Constraints — 15 August 2010 @ 3:01 | Reply


RSS feed for comments on this post. TrackBack URI

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Blog at WordPress.com.

%d bloggers like this: