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).

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$?

  • 11
    $\begingroup$ It's worth noting that $\alpha$ is a function of $k$. $\endgroup$ – Huck Bennett Apr 9 '14 at 3:55
  • $\begingroup$ 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... $\endgroup$ – vzn Apr 9 '14 at 15:01

Yes, there has been. Moshe Vardi recently gave a survey talk at BIRS Theoretical Foundations of Applied SAT Solving workshop:

(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 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.
  • 2
    $\begingroup$ 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})$. $\endgroup$ – Iddo Tzameret Dec 21 '15 at 23:23

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" 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.
  • 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.
  • $\begingroup$ 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. $\endgroup$ – András Salamon Apr 17 '14 at 10:35

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

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).

  • $\begingroup$ 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. $\endgroup$ – vzn Apr 9 '14 at 22:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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