Has there been any research on $k$-SAT above the satisfiability threshold?

Question

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

Answer 1

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

• Moshe Vardi, Phase transitions and computational complexity, 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 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.

Answer 2

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.

Answer 3

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

• The constrainedness knife edge 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).