<p>There are at least two lines of research concerning random $k\text-\mathsf{SAT}$ for formulas with a clause/variable-ratio larger than the satisfiability threshold:</p>

<ul>
<li>For such formulas lower bounds on the length of refutations in resolution and stronger propositional proof systems have been shown, starting with the paper "<a href="http://dx.doi.org/10.1145/48014.48016">Many hard examples for resolution</a>" by Chvátal and Szemerédi. These resolution lower bounds imply lower bounds on the runtime of DPLL- and CDCL-based SAT-solvers. The strongest lower bounds are for Polynomial Calculus, due to <a href="http://dx.doi.org/10.1109/SFFCS.1999.814613">Ben-Sasson and Impagliazzo</a>.</li>
<li>For such formulas there are efficient deterministic algorithms for certifying unsatisfiability, i.e., algorithms that either output "UNSAT" or "Don't Know", where the answer "UNSAT" is required to be correct, and it has to output "UNSAT" on unsatisfiable formulas with high probability. The strongest results in that direction are due to <a href="http://dx.doi.org/10.4086/toc.2007.v003a002">Feige and Ofek</a>.</li>
</ul>

CC BY-SA 3.0
2014-04-17T10:35:52.293Z
It is perhaps worth noting that Chvátal/Szemerédi show that w.h.p. a random $k$-SAT formula with $m/n \ge c_1$ is unsatisfiable.  Feige and Ofek give a spectral algorithm when $m/n \ge c_2n^{1/2}$.  So there remains a $\sqrt{n}$ gap between $c_1n$ and $c_2n^{3/2}$ where almost every formula is unsatisfiable, but we don't know how to decide that this is so.
András Salamon
CC BY-SA 3.0
2014-04-09T15:08:48.107Z
2014-04-09T15:36:23.870Z
2014-04-09T15:36:23.870Z
Jan Johannsen
<p>Yes, there has been. Moshe Vardi recently gave a survey talk at <a href="http://www.birs.ca/events/2014/5-day-workshops/14w5101" rel="nofollow">BIRS Theoretical Foundations of Applied SAT Solving workshop</a>:</p>

<ul>
<li>Moshe Vardi, <a href="http://www.birs.ca/events/2014/5-day-workshops/14w5101/videos/watch/201401231116-Vardi.mp4" rel="nofollow">Phase transitions and computational complexity</a>, 2014.</li>
</ul>

<p>(Moshe presents the graph of their experiment a bit after minute 14:30 in his talk linked above.)</p>

<p>Let $\rho$ denote the clause ratio.
As the value of $\rho$ increases beyond the threshold 
the problem becomes easier for existing SAT solvers, 
but not as easy as it was before reaching the threshold. 
There is a very steep increase in difficulty as we approach the threshold from below. 
After the threshold the problem becomes easier compared to the threshold but 
the decrease in difficulty is much less steep.</p>

<p>Let $T_\rho(n)$ denote the difficulty of the problem w.r.t. to $n$
(in their experiment $T_\rho(n)$ is the median running-time of <a href="http://vlsicad.eecs.umich.edu/BK/Slots/cache/sat.inesc.pt/~jpms/grasp/" rel="nofollow">GRASP</a> on random 3SAT instances with the clause ratio $\rho$).
Moshe suggests that $T_\rho(n)$ changes as follows:</p>

<ul>
<li>$\rho \ll$ the threshold: $T_\rho(n)$ is polynomial in $n$,</li>
<li>$\rho$ is near the threshold: $T_\rho(n)$ is exponential in $n$,</li>
<li>$\rho \gg$ the threshold: $T_\rho(n)$ remains exponential in $n$ but 
the exponent decreases as $\rho$ increases.</li>
</ul>

CC BY-SA 3.0
2015-12-21T23:23:00.230Z
It should be noted that the above results are experimental results (from about 2000) using a specific SAT-solver (GRASP). But, theoretically, it is known that for large enough $\rho$ (say, $\Omega(n)$) even resolution has small refutations of unsatisfiability. And, as Jan Johannsem wrote before, *refuting* 3-SAT is easy (in the average-case) already when $\rho=\Omega(\sqrt{n})$.
Iddo Tzameret
CC BY-SA 3.0
2014-04-09T02:26:37.270Z
2015-12-17T09:47:20.607Z
2015-12-17T09:47:20.607Z
Kaveh
<p>here is an older but relevant study/angle by a leading expert. </p>

<ul>
<li><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.3267" rel="nofollow">The constrainedness knife edge</a> Walsh 1998</li>
</ul>

<p>he shows the parameter $\kappa$ estimates number of solutions and measures "constrainedness" and correlates/trends roughly with the clause-to-variable ratio. see p3 fig 4 in particular</p>

<blockquote>
  <p>In figure 4, we plot the estimated constrainedness down the heuristic branch for random 3-SAT problems. For L/N &lt; 4.3, problems are under-constrained and soluble. As search progresses, $\kappa$ decreases as problems become more under-constrained and obviously soluble. For L/N > 4.3, problems are over-constrained and insoluble. As search progresses, $\kappa$ increases as problems become more over-constrained and obviously insoluble.</p>
</blockquote>

<p>the question asks about $m/n \gg\alpha$. but this is known from empirical analysis to be highly overconstrained and therefore basically approaching P-time instances (a solver "quickly" discovers they are unsolvable) and therefore not as theoretically interesting (because they do not "elicit/exercise" the exponential-time-behavior of solvers on average). however, have not personally seen papers/ transformations/ theory that prove this more theoretically/rigorously (other than this paper as a start on that).</p>

CC BY-SA 3.0
2014-04-09T22:41:30.663Z
on the other hand is presumably possible to generate individual "hard" instances of any m/n "dimension", its just they are less statistically likely outside of the "P-NP-P" phase transition.
vzn
CC BY-SA 3.0
2014-04-09T15:35:42.953Z
2014-04-09T15:35:42.953Z
vzn
<p>A well known characteristic of $k$-SAT instances is the ratio of the number of clauses $m$ over the number of variables $n$, i.e., the quotient $\rho = m/n$.  For every $k$, there is a threshold value $\alpha$ s.t.\ for $\rho \ll \alpha$, most instances are satisfiable, and for $\rho \gg \alpha$ most instances are unsatisfiable. There has been a lot of research done for problems where $\rho \ll \alpha$, and for problems with sufficiently small $\rho$, $k$-SAT becomes solvable in polynomial time.  See, for instance, Dimitris Achlioptas's survey article from the Handbook of Satisfiability (<a href="http://users.soe.ucsc.edu/~optas/papers/handbook.pdf">PDF</a>).</p>

<p>I am wondering if any work has been done in the other direction (where $\rho \gg \alpha$), e.g., if we can somehow transform the problem from CNF to DNF in this case to solve it quickly.</p>

<p>So, essentially, <strong>What is known regarding SAT where $\rho = m/n \gg \alpha$?</strong></p>

CC BY-SA 3.0
2014-04-09T03:55:07.040Z
It's worth noting that $\alpha$ is a function of $k$.
Huck Bennett
CC BY-SA 3.0
2014-04-09T15:01:33.173Z
could there be some transformation that shows some kind of symmetry between the two regions on both "sides" of the transition point? seems plausible. anyway the question is rather broad in the sense there is much empirical/theoretical study of the transition point which does not focus so much on one "side" or the other...
vzn
<cc.complexity-theory><sat><random-k-sat><phase-transition>
Has there been any research on $k$-SAT above the satisfiability threshold?
Matt Groff
# Has there been any research on $k$-SAT above the satisfiability threshold?

(Asked by: username_0 on 2014-04-09)

A well known characteristic of $k$-SAT instances is the ratio of the number of clauses $m$ over the number of variables $n$, i.e., the quotient $\rho = m/n$. For every $k$, there is a threshold value $\alpha$ s.t.\ for $\rho \ll \alpha$, most instances are satisfiable, and for $\rho \gg \alpha$ most instances are unsatisfiable. There has been a lot of research done for problems where $\rho \ll \alpha$, and for problems with sufficiently small $\rho$, $k$-SAT becomes solvable in polynomial time. See, for instance, Dimitris Achlioptas's survey article from the Handbook of Satisfiability ([PDF](http://users.soe.ucsc.edu/~optas/papers/handbook.pdf)).

I am wondering if any work has been done in the other direction (where $\rho \gg \alpha$), e.g., if we can somehow transform the problem from CNF to DNF in this case to solve it quickly.

So, essentially, **What is known regarding SAT where $\rho = m/n \gg \alpha$?**

**Tags:** cc.complexity-theory, sat, random-k-sat, phase-transition
> **Comments:**
> **username_1**: It's worth noting that $\alpha$ is a function of $k$.  
> **username_2**: could there be some transformation that shows some kind of symmetry between the two regions on both "sides" of the transition point? seems plausible. anyway the question is rather broad in the sense there is much empirical/theoretical study of the transition point which does not focus so much on one "side" or the other...  

---

## 3 answers

### Answer by username_5 on 2014-04-09. Score: 26

Yes, there has been. Moshe Vardi recently gave a survey talk at [BIRS Theoretical Foundations of Applied SAT Solving workshop](http://www.birs.ca/events/2014/5-day-workshops/14w5101):

* Moshe Vardi, [Phase transitions and computational complexity](http://www.birs.ca/events/2014/5-day-workshops/14w5101/videos/watch/201401231116-Vardi.mp4), 2014.

(Moshe presents the graph of their experiment a bit after minute 14:30 in his talk linked above.)

Let $\rho$ denote the clause ratio.
As the value of $\rho$ increases beyond the threshold
the problem becomes easier for existing SAT solvers,
but not as easy as it was before reaching the threshold.
There is a very steep increase in difficulty as we approach the threshold from below.
After the threshold the problem becomes easier compared to the threshold but
the decrease in difficulty is much less steep.

Let $T\_\rho(n)$ denote the difficulty of the problem w.r.t. to $n$
(in their experiment $T\_\rho(n)$ is the median running-time of [GRASP](http://vlsicad.eecs.umich.edu/BK/Slots/cache/sat.inesc.pt/~jpms/grasp/) on random 3SAT instances with the clause ratio $\rho$).
Moshe suggests that $T\_\rho(n)$ changes as follows:

* $\rho \ll$ the threshold: $T\_\rho(n)$ is polynomial in $n$,
* $\rho$ is near the threshold: $T\_\rho(n)$ is exponential in $n$,
* $\rho \gg$ the threshold: $T\_\rho(n)$ remains exponential in $n$ but
  the exponent decreases as $\rho$ increases.

> **Comments:**
> **username_6**: It should be noted that the above results are experimental results (from about 2000) using a specific SAT-solver (GRASP). But, theoretically, it is known that for large enough $\rho$ (say, $\Omega(n)$) even resolution has small refutations of unsatisfiability. And, as Jan Johannsem wrote before, *refuting* 3-SAT is easy (in the average-case) already when $\rho=\Omega(\sqrt{n})$.  

---

### Answer by username_3 on 2014-04-09. Score: 20

There are at least two lines of research concerning random $k\text-\mathsf{SAT}$ for formulas with a clause/variable-ratio larger than the satisfiability threshold:

* For such formulas lower bounds on the length of refutations in resolution and stronger propositional proof systems have been shown, starting with the paper "[Many hard examples for resolution](http://dx.doi.org/10.1145/48014.48016)" by Chvátal and Szemerédi. These resolution lower bounds imply lower bounds on the runtime of DPLL- and CDCL-based SAT-solvers. The strongest lower bounds are for Polynomial Calculus, due to [Ben-Sasson and Impagliazzo](http://dx.doi.org/10.1109/SFFCS.1999.814613).
* For such formulas there are efficient deterministic algorithms for certifying unsatisfiability, i.e., algorithms that either output "UNSAT" or "Don't Know", where the answer "UNSAT" is required to be correct, and it has to output "UNSAT" on unsatisfiable formulas with high probability. The strongest results in that direction are due to [Feige and Ofek](http://dx.doi.org/10.4086/toc.2007.v003a002).

> **Comments:**
> **username_4**: It is perhaps worth noting that Chvátal/Szemerédi show that w.h.p. a random $k$-SAT formula with $m/n \ge c_1$ is unsatisfiable.  Feige and Ofek give a spectral algorithm when $m/n \ge c_2n^{1/2}$.  So there remains a $\sqrt{n}$ gap between $c_1n$ and $c_2n^{3/2}$ where almost every formula is unsatisfiable, but we don't know how to decide that this is so.  

---

### Answer by username_2 on 2014-04-09. Score: 2

here is an older but relevant study/angle by a leading expert.

* [The constrainedness knife edge](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.3267) Walsh 1998

he shows the parameter $\kappa$ estimates number of solutions and measures "constrainedness" and correlates/trends roughly with the clause-to-variable ratio. see p3 fig 4 in particular

> In figure 4, we plot the estimated constrainedness down the heuristic branch for random 3-SAT problems. For L/N < 4.3, problems are under-constrained and soluble. As search progresses, $\kappa$ decreases as problems become more under-constrained and obviously soluble. For L/N > 4.3, problems are over-constrained and insoluble. As search progresses, $\kappa$ increases as problems become more over-constrained and obviously insoluble.

the question asks about $m/n \gg\alpha$. but this is known from empirical analysis to be highly overconstrained and therefore basically approaching P-time instances (a solver "quickly" discovers they are unsolvable) and therefore not as theoretically interesting (because they do not "elicit/exercise" the exponential-time-behavior of solvers on average). however, have not personally seen papers/ transformations/ theory that prove this more theoretically/rigorously (other than this paper as a start on that).

> **Comments:**
> **username_2**: on the other hand is presumably possible to generate individual "hard" instances of any m/n "dimension", its just they are less statistically likely outside of the "P-NP-P" phase transition.  

---

