26

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


19

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


17

Notwithstanding Friedgut's theorem about $k$-SAT, while we lack techniques to get to negligible $\epsilon$ for small $k$, it seems more useful to talk about the satisfiability threshold ($\alpha - \epsilon$) and the unsatisfiability threshold ($\alpha + \epsilon$) as separate entities. The unsatisfiability threshold is known to be at most 4.4898, a slight ...


10

Not really an answer but the closest references I am aware of. There are results available for branch-width. Also, there is at least one empirical study of treewidth of industrial instances. Discovering treewidth, H. Bodlaender, 2005. Gives algorithms to compute bounds on treewidth. Treewidth in Industrial SAT Benchmarks, R. Mateescu, 2011. Uses variations ...


10

In light of the Ding--Sly--Sun verification of the 1-step Replica Symmetry Breaking picture for kSAT (when k is large enough) I think experts would now be pretty surprised if the MPZ/MMZ-conjectured formula for the 3SAT satisfiability threshold (approximate value: 4.2667) is incorrect.


7

In general one would not expect random instances of SAT to have bounded treewidth, even if they are easy. Here is an example: A random k-SAT instance on $n$ variables where each variable occurs in $3$ clauses will be an expander graph, and therefore have treewidth $\theta(n)$ with high probability. This holds in the model where we fix an n and an m (with ...


6

There is a new 58 page paper (32 refs) accepted to STOC 2013, Going after the k-SAT threshold by Coja-Oghlan and Konstantinos Panagiotou that surveys and advances the area of determining the precise k-SAT threshhold, building especially from results borrowed from statistical physics. From the abstract: Here we develop a new asymmetric second moment ...


5

I am not aware of any collections of 2CNF benchmark instances. However, one practical way of constructing #2-SAT instances that are provably hard for state-of-the-art model counters is as follows: generate a $d$-regular expander for some constant $d$ (so in practice a random $d$-regular graph), then, as holf suggested, construct the 2CNF-formula that has ...


4

see eg sec 4.7.4 p103 of this thesis where a finite-size scaling formula based on a power law is applied and coefficients fit with experimental data. PHASE TRANSITIONS OF BOOLEAN SATISFIABILITY VARIANTS, Bailey 2004


2

It sounds like what you want are universal factor graphs. Such graphs exist for every NP-hard boolean CSP and in many cases are optimally inapproximable.


2

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


Only top voted, non community-wiki answers of a minimum length are eligible