<p>If I correctly understand the very core of your question, you want to take a relatively easy instance (since you put yourself in an area where $\frac{m}{n}> 4.3$), and transform it into a hard one by embedding a solution. I doubt that this would work.</p>

<p>Experimental data suggest that, when constructing a random instance "around" a predefined solution $x$, such instance will be easier than usual (compared to similar instances having the same $n$ and $m$). It's like if the hidden solution helps the SAT solver, guiding it through the search space. Normally, to construct such an instance, we generate random clauses as usual (e.g. choosing $k$ literals at random and negating each of them with probability $p = \frac{1}{2}$) but we discard those clauses which are not satisfied by our hidden solution $x$. For what concerns your approach of constructing $\phi|x$ from and hard instance $\phi$: I've never tried that, but I "feel" that $\phi|x$ will become easier, if not trivial. I believe that doing that would augment the hit count of $x$'s literals (the hit count of a literal $l$ is the number of occurrences of $l$ in a given formula), and that this would drive the SAT solver to the target. Maybe the solution spaces of $\phi$ and $\phi|x$ would be similar (if not almost identical), as happens in Ryan Williams' example of SAT0 (almost identical solution spaces, but completely different hardness). Did you try your approach in practice? It would be interesting to see how the same SAT solver behaves on $\phi$ and on $\phi|x$.</p>

<p>EDIT 1 (23rd Sep 2010):
After thinking a little bit more, I feel that actually $\phi|x$ solution space would be very different than $\phi$'s. You are adding a literal to each clause, so you're giving more degree of freedom to such clauses (i.e. each clause has more chance to be satisfied): probably the resulting solution space would be massively transformed.</p>

<p>EDIT 2 (1st Oct 2010):
I've thought about the following very simple and not original idea. Given an initial instance $\phi$ and an assignment $x$:</p>

<ol>
<li><p>Remove from $\phi$ all those clauses unsatisfied by $x$. This will enlarge the solution space, and <em>should</em> embed $x$ in it.</p></li>
<li><p>Suppose you removed $m_x$ clauses. Now randomly add $m_x$ new clauses, taking care that they are not unsatisfied by $x$ (this will narrow the solution space again, but without pushing $x$ out of it).</p></li>
</ol>

<p>I don't know if this will work or not. I didn't try it, yet. More precisely, I'm not sure if Step 1 always manages to embed $x$ in the solution space (maybe $x$ is ruled out by some combination of clauses, even if each of them is not unsatisfied by $x$?).</p>

CC BY-SA 2.5
2010-09-17T12:57:30.970Z
Thanks for the comments, I agree that the solution space would be changed.  As indicated in the question, I want to know whether there is _a_ way to modify the formula to hide a solution.  Adding the literals to each clause is meant as an existence proof that one can add the solution to the formula.  I did not mean to suggest that this is the only, best, or even a good method.
András Salamon
CC BY-SA 2.5
2010-09-17T14:10:26.887Z
You're welcome, Andras. Yes, solution $x$ can certainly be added using your method. If you want that $\phi|x$'s solution space is exactly equal to $\phi$ solution space plus just that solution $x$, I think this is hard to obtain. On the other hand, if you're willing to accept that many other solutions will be added, your strategy is OK.
Giorgio Camerani
CC BY-SA 2.5
2010-09-18T11:15:42.433Z
Ideally one wants a polytime-computable method that doesn't change the solution space "too much"...
András Salamon
CC BY-SA 2.5
2010-10-02T22:46:07.457Z
It would be interesting to check whether the $n^{3\log\ n}$ algorithm mentioned by Feige for planted cliques still works for any of these planted solutions.
András Salamon
CC BY-SA 2.5
2010-10-03T15:30:54.357Z
@Walter: The reason I say it would be interesting to investigate the simple "find a $3 \log n$-clique" algorithm, is that the easiest reduction of SAT to CLIQUE requires an $n$-clique in a graph with $2n$ vertices.  Either bridging this gap between $n$ and $3\log n$, or showing it can't be bridged, would be interesting.
András Salamon
CC BY-SA 2.5
2010-10-04T07:27:51.330Z
@Andràs: Very interesting. Let me see if I correctly understood: if you manage to bridge the gap betweeen $n$ and $3logn$, would this mean that SAT is doable in sub-exponential time (although still superpolynomial)?
Giorgio Camerani
CC BY-SA 2.5
2010-10-04T11:04:18.937Z
@Walter: essentially yes, it would show that there is a randomized algorithm to solve SAT in subexponential time.  I think it is more likely that one could show that this can't work; this would be interesting too.  If one could actually show that a stronger Feige-style approach doesn't work either, then that would mean embedding a solution might be a feasible method of constructing one-way functions.  See Boaz Barak's comment; I think the idea of embedding solutions as one-way functions is a standard idea.
András Salamon
CC BY-SA 2.5
2010-09-17T12:09:54.253Z
2010-10-01T12:25:03.780Z
2010-10-01T12:25:03.780Z
Giorgio Camerani
<p>You can take any formula $\varphi$ and change it to the formula $\varphi \vee \psi_x$ where $\psi_x$ is a "hard" SAT instance whose only solution is $x$. One way to construct such a formula is using cryptography:  if $f:\{0,1\}^n\rightarrow \{0,1\}^n$ is a one-way permutation and we choose $x$ at random and set $y=f(x)$, then one can convert $y$ into a SAT formula such that $x$ is its only solution and thus finding $x$ corresponds to inverting $f$. (We need for this $x$ to be random, but this something similar is anyway assumed if we think finding $x$ should be hard.)</p>

CC BY-SA 2.5
2010-09-19T22:54:37.207Z
Ah, $\phi \lor \psi_x$ has polynomial size in $\phi$ and $\psi_x$.  Thanks!
András Salamon
CC BY-SA 2.5
2010-09-19T00:40:33.273Z
2010-10-02T02:51:04.873Z
2010-10-02T02:51:04.873Z
Boaz Barak
<p>I am interested in "hard" individual instances of NP-complete problems.</p>

<p>Ryan Williams <a href="http://rjlipton.wordpress.com/2010/09/15/an-update-on-vinay-deolalikars-proof/#comment-6757">discussed the SAT0 problem at Richard Lipton's blog</a>.  SAT0 asks whether a SAT instance has the specific solution consisting of all 0's.  This got me thinking about constructing SAT instances that are likely to be "hard".</p>

<p>Consider a SAT instance $\phi$ with $m$ clauses and $n$ variables, where $\alpha = m/n$ is "large enough", in the sense that it falls into the region beyond the phase transition, where nearly all instances are unsatisfiable.  Let $x$ be a random assignment to the values of $\phi$.</p>

<blockquote>
  <p>Is it possible to modify $\phi$ to obtain a new instance $\phi|x$, so that $\phi|x$ is "largely similar" to $\phi$, but so that $x$ is a satisfying assigment for $\phi|x$?</p>
</blockquote>

<p>For instance, one could try to add to each clause a randomly chosen literal from the solution, that does not already occur in the clause.  This will guarantee that $x$ is a solution.</p>

<p>Or is this hopeless, leading to a fast algorithm for finding the "hidden" solution, along the lines of the following recent paper?</p>

<ul>
<li>Uriel Feige and Dorit Ron, <em>Finding hidden cliques in linear time</em>, <a href="http://www.dmtcs.org/dmtcs-ojs/index.php/proceedings/article/viewArticle/dmAM0114">DMTCS proc. AM, 2010, 189–204.</a></li>
</ul>

<p>I am aware of the discussion by Cook and Mitchell and work they reference.  However, I couldn't find anything about what happens to the structure of a formula when one tries to explicitly embed a satisfying assignment into it.  If this is folklore, pointers would be very welcome!</p>

<ul>
<li>Stephen A. Cook and David G. Mitchell, <em>Finding Hard Instances of the Satisfiability Problem: A Survey</em>, DIMACS Series in Discrete Mathematics and Theoretical Computer Science <strong>35</strong> 1–17, AMS, ISBN 0-8218-0479-0, 1997. (<a href="http://www.cs.toronto.edu/~sacook/homepage/SAT.ps">PS</a>)</li>
</ul>

<cc.complexity-theory><sat><hard-instances>
Is embedding a solution feasible for SAT?
András Salamon
# Is embedding a solution feasible for SAT?

(Asked by: username_0 on 2010-09-17)

I am interested in "hard" individual instances of NP-complete problems.

Ryan Williams [discussed the SAT0 problem at Richard Lipton's blog](http://rjlipton.wordpress.com/2010/09/15/an-update-on-vinay-deolalikars-proof/#comment-6757). SAT0 asks whether a SAT instance has the specific solution consisting of all 0's. This got me thinking about constructing SAT instances that are likely to be "hard".

Consider a SAT instance $\phi$ with $m$ clauses and $n$ variables, where $\alpha = m/n$ is "large enough", in the sense that it falls into the region beyond the phase transition, where nearly all instances are unsatisfiable. Let $x$ be a random assignment to the values of $\phi$.

> Is it possible to modify $\phi$ to obtain a new instance $\phi|x$, so that $\phi|x$ is "largely similar" to $\phi$, but so that $x$ is a satisfying assigment for $\phi|x$?

For instance, one could try to add to each clause a randomly chosen literal from the solution, that does not already occur in the clause. This will guarantee that $x$ is a solution.

Or is this hopeless, leading to a fast algorithm for finding the "hidden" solution, along the lines of the following recent paper?

* Uriel Feige and Dorit Ron, *Finding hidden cliques in linear time*, [DMTCS proc. AM, 2010, 189–204.](http://www.dmtcs.org/dmtcs-ojs/index.php/proceedings/article/viewArticle/dmAM0114)

I am aware of the discussion by Cook and Mitchell and work they reference. However, I couldn't find anything about what happens to the structure of a formula when one tries to explicitly embed a satisfying assignment into it. If this is folklore, pointers would be very welcome!

* Stephen A. Cook and David G. Mitchell, *Finding Hard Instances of the Satisfiability Problem: A Survey*, DIMACS Series in Discrete Mathematics and Theoretical Computer Science **35** 1–17, AMS, ISBN 0-8218-0479-0, 1997. ([PS](http://www.cs.toronto.edu/~sacook/homepage/SAT.ps))

**Tags:** cc.complexity-theory, sat, hard-instances


---

## 2 answers

### Answer by username_2 on 2010-09-19. Score: 13 | Accepted answer

You can take any formula $\varphi$ and change it to the formula $\varphi \vee \psi\_x$ where $\psi\_x$ is a "hard" SAT instance whose only solution is $x$. One way to construct such a formula is using cryptography: if $f:\{0,1\}^n\rightarrow \{0,1\}^n$ is a one-way permutation and we choose $x$ at random and set $y=f(x)$, then one can convert $y$ into a SAT formula such that $x$ is its only solution and thus finding $x$ corresponds to inverting $f$. (We need for this $x$ to be random, but this something similar is anyway assumed if we think finding $x$ should be hard.)

> **Comments:**
> **username_0**: Ah, $\phi \lor \psi_x$ has polynomial size in $\phi$ and $\psi_x$.  Thanks!  

---

### Answer by username_1 on 2010-09-17. Score: 6

If I correctly understand the very core of your question, you want to take a relatively easy instance (since you put yourself in an area where $\frac{m}{n}> 4.3$), and transform it into a hard one by embedding a solution. I doubt that this would work.

Experimental data suggest that, when constructing a random instance "around" a predefined solution $x$, such instance will be easier than usual (compared to similar instances having the same $n$ and $m$). It's like if the hidden solution helps the SAT solver, guiding it through the search space. Normally, to construct such an instance, we generate random clauses as usual (e.g. choosing $k$ literals at random and negating each of them with probability $p = \frac{1}{2}$) but we discard those clauses which are not satisfied by our hidden solution $x$. For what concerns your approach of constructing $\phi|x$ from and hard instance $\phi$: I've never tried that, but I "feel" that $\phi|x$ will become easier, if not trivial. I believe that doing that would augment the hit count of $x$'s literals (the hit count of a literal $l$ is the number of occurrences of $l$ in a given formula), and that this would drive the SAT solver to the target. Maybe the solution spaces of $\phi$ and $\phi|x$ would be similar (if not almost identical), as happens in Ryan Williams' example of SAT0 (almost identical solution spaces, but completely different hardness). Did you try your approach in practice? It would be interesting to see how the same SAT solver behaves on $\phi$ and on $\phi|x$.

EDIT 1 (23rd Sep 2010):
After thinking a little bit more, I feel that actually $\phi|x$ solution space would be very different than $\phi$'s. You are adding a literal to each clause, so you're giving more degree of freedom to such clauses (i.e. each clause has more chance to be satisfied): probably the resulting solution space would be massively transformed.

EDIT 2 (1st Oct 2010):
I've thought about the following very simple and not original idea. Given an initial instance $\phi$ and an assignment $x$:

1. Remove from $\phi$ all those clauses unsatisfied by $x$. This will enlarge the solution space, and *should* embed $x$ in it.
2. Suppose you removed $m\_x$ clauses. Now randomly add $m\_x$ new clauses, taking care that they are not unsatisfied by $x$ (this will narrow the solution space again, but without pushing $x$ out of it).

I don't know if this will work or not. I didn't try it, yet. More precisely, I'm not sure if Step 1 always manages to embed $x$ in the solution space (maybe $x$ is ruled out by some combination of clauses, even if each of them is not unsatisfied by $x$?).

> **Comments:**
> **username_0**: Thanks for the comments, I agree that the solution space would be changed.  As indicated in the question, I want to know whether there is _a_ way to modify the formula to hide a solution.  Adding the literals to each clause is meant as an existence proof that one can add the solution to the formula.  I did not mean to suggest that this is the only, best, or even a good method.  
> **username_1**: You're welcome, Andras. Yes, solution $x$ can certainly be added using your method. If you want that $\phi|x$'s solution space is exactly equal to $\phi$ solution space plus just that solution $x$, I think this is hard to obtain. On the other hand, if you're willing to accept that many other solutions will be added, your strategy is OK.  
> **username_0**: Ideally one wants a polytime-computable method that doesn't change the solution space "too much"...  
> **username_0**: It would be interesting to check whether the $n^{3\log\ n}$ algorithm mentioned by Feige for planted cliques still works for any of these planted solutions.  
> **username_0**: @Walter: The reason I say it would be interesting to investigate the simple "find a $3 \log n$-clique" algorithm, is that the easiest reduction of SAT to CLIQUE requires an $n$-clique in a graph with $2n$ vertices.  Either bridging this gap between $n$ and $3\log n$, or showing it can't be bridged, would be interesting.  
> **username_1**: @Andràs: Very interesting. Let me see if I correctly understood: if you manage to bridge the gap betweeen $n$ and $3logn$, would this mean that SAT is doable in sub-exponential time (although still superpolynomial)?  
> **username_0**: @Walter: essentially yes, it would show that there is a randomized algorithm to solve SAT in subexponential time.  I think it is more likely that one could show that this can't work; this would be interesting too.  If one could actually show that a stronger Feige-style approach doesn't work either, then that would mean embedding a solution might be a feasible method of constructing one-way functions.  See username_2's comment; I think the idea of embedding solutions as one-way functions is a standard idea.  

---

