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


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

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

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


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.


1

See Jan Krajicek, "A note on SAT algorithms and proof complexity", 2012 I am not sure if we have any result for random unsat instances (how do you define a random unsat instance?).


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