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 but not in .
Consider the following parameterized decision problem, with parameter .
k-ISOLATED SAT | |
Input: | SAT instance with clauses and variables, of size bits |
Question: | is there a satisfying assignment , such that every assignment which has at most bits different from 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 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 is given as part of the input, and the question is whether there is a satisfying assignment at most Hamming distance from . For any given , Stefan’s problem is in and is FPT for bounded clause size.
k-FLIP SAT requires a solution within a specified -ball, while k-ISOLATED SAT needs to establish a -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
More precisely k-FLIP SAT is -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 unless W[1] = FPT. (-hardness follows immediately from Stefan’s proof of -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 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 . So for constant , it is in something like , 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 .
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 ?
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 are especially interesting in this context: they are hard for guess-and-verify, even if the number of solutions of an instance is large.
[…] 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 |