There are 4 different constraints we can have when defining Random K-SAT.
1)Total number of literals in a given clauses is exactly K or AT most K
2)A given literal can be used with or without replacement in the same clause (A or A or A)
3)A given variable can be used with or without replacement in the same clause (A or ~A or ~A)
4)A given clauses can be used with or without replacement in a given formula
What would be the most "correct" definition? What are the cons and pros of using these different definitions?

  • 17
    $\begingroup$ I do not think that there is a single universally accepted definition. $\endgroup$ – Tsuyoshi Ito Jan 30 '11 at 15:29
  • 5
    $\begingroup$ Yet another different choice you can make is whether to choose a fixed number of clauses (with or without replacement) or to choosee a Poisson sample (each clause is included independently with a fixed probability). $\endgroup$ – David Eppstein Jan 30 '11 at 17:10
  • 4
    $\begingroup$ @Tsuyoshi, Geekster: I agree with Tsuyoshi, as far as I know SAT Solvers don't need any definition of Random k-SAT, whatever technique they use (DPLL, local search, survey propagation). I'm 100% sure that any serious SAT Solver will remove duplicated clauses, tautological clauses, and duplicated literals before starting the search. Some solvers also remove subsumed clauses. $\endgroup$ – Giorgio Camerani Jan 30 '11 at 22:30
  • 4
    $\begingroup$ I do not think that there is an answer to the question in the current form because no definitions seem “more correct” than others and “cons and pros” presumably depend on what you want to use results on random k-SAT for. I voted to close it as not a real question. $\endgroup$ – Tsuyoshi Ito Jan 30 '11 at 22:35
  • 4
    $\begingroup$ I guess the question can be restated, removed the "most correct" part, and concentrate on the cons and pros under some specific results. (Or the answer may go through each possible result.) Since this question is somehow similar to a question about sparest cut which seems to be within scope with no argument, personally I would like to see the question remains open. $\endgroup$ – Hsien-Chih Chang 張顯之 Feb 1 '11 at 1:52

As was pointed out at the beginning of this discussion in the comments, there is not necessarily a single "right" definition for random $k$-SAT.

That said, the two most common variants of random $k$-SAT are both fixed clause length (FCL) models, meaning that exactly $k$ literals appear in each clause. These variants both disallow repeated variables and literals within a clause, but differ in whether they allow repeated clauses within a formula. Nevertheless, they are essentially the same as will be discussed below.

Two main models:

The Selman random model - Repeated clause are allowed. Kyle gave this nice reference in the comments to his answer, but incorrectly assumed that the model disallowed repeated clauses. The linked (slightly different) version of the paper contains a more detailed discussion of the random model in Section 3: "This method of generation allows duplicate clauses in a formula... However, as N gets large duplicates will become rare because we generally select only a linear number of clauses."

The Achlioptas random model - Repeated clauses are disallowed. We treat generating a random formula as selecting $m$ clauses u.a.r. from the $2^k {n \choose k}$ total possible clauses without replacement. See Ch.8 of the Handbook of Satisfiability [1] (Random SAT by Achlioptas) as a reference. This model seems more prevalent in the theoretical literature, possibly because so much of it was written by Achlioptas himself.

Equivalence of phase transition locations:

However, the phase transition (50% satisfiability threshold) occurs at the same clause-to-variable ratio regardless of which of these models is chosen for essentially the reason that Selman et al. noted in their paper.

Let $A(n,m,k)$ denote the expected number of identical pairs of clauses in a Selman random $(n,m,k)$-SAT instance. The probability of a given pair of clauses being identical is $p = 1/(2^k {n \choose k})$, whereas the total number of pairs of clauses is $N = {m \choose 2}$. By the linearity of expectation, $A(n,m,k) = p \cdot N = {m \choose 2}/{2^k {n \choose k}}$.

By Theorem 3 in [1], the provable upper bound on the location of the $k$-SAT phase transition, using the Achlioptas model occurs when $m = O(2^k n)$. Fixing $k \geq 3$ and setting $m = O(2^k n)$ we get

$A(n,m,k) = {m \choose 2}/{2^k {n \choose k}} = O(m^2)/O(n^k) = O(n^2)/O(n^k)$.

Then, because $k \geq 3$, $\displaystyle \lim_{n \rightarrow \infty} O(n^2)/O(n^k) = 0$, meaning that in expectation there will be zero repeated clauses around the $k$-SAT phase transition when generating random SAT formulas using the Selman model.

Shameless self promotion - I discuss these topics briefly in Section 4.1 of my master's thesis.

Random QBF

As it turns out, the situation is much more interesting for random QBF. What are AFAIK the first three papers on random QBF each proposed a new random model, critiquing their predecessor.

See the following papers:

  • Cadoli et al. "Experimental Analysis of the Computational Cost of Evaluating Quantified Boolean Formulae." AI*IA 1997
  • Gent + Walsh "Beyond NP: the QSAT phase transition." AAAI/IAAI 1999
  • Chen + Interian "A Model for Generating Random Quantified Boolean Formulas." IJCAI 2005
| cite | improve this answer | |

[Edited for clarity]

The most widely used definition in the research literature is the one that requires exactly k distinct variables per clause, and no duplicate clauses. If you relax the distinct variables restriction, much of the existing research won't make sense to you because your results will not match their results. The well known sat/unsat phase transition will occur at a different clause-to-variable ratio (if the transition exists at all) and you won't find the hard SAT instances where you'd expect from the literature.

| cite | improve this answer | |
  • 3
    $\begingroup$ Generating Hard Satisfiability Problems by Mitchell, Selman and Levesque. Section 4 describes what they call "Random K-SAT." The paper doesn't talk about relaxing the restrictions; that comes from my modifying a random 3SAT generator and feeding many instances into a typical DPLL-based SAT solver. $\endgroup$ – Kyle Jones Dec 21 '11 at 22:20
  • 5
    $\begingroup$ “The most correct definition is the one that produces the sat/unsat phase transition at around 4.26 clauses per variable for random 3SAT.” You must be kidding. $\endgroup$ – Tsuyoshi Ito Dec 22 '11 at 2:50
  • 1
    $\begingroup$ @Tsuyoshi: While "most correct" is definitely a stretch, I think the argument is that this version is standard and one of the best studied. $\endgroup$ – Huck Bennett Dec 22 '11 at 6:45
  • 2
    $\begingroup$ You are making a bizarre claim that 4.26 is the magic number which distinguishes a particular definition of term “random k-SAT” as the most correct one. If this is not a joke, I do not know what to say. $\endgroup$ – Tsuyoshi Ito Dec 24 '11 at 22:00
  • 4
    $\begingroup$ No, I'm making the claim that the discovery of the phase transition and all the subsequent research and papers that followed agree on the default definition of random k-SAT, which is the definition I gave. If you use a different definition a lot of papers aren't going to make sense to you because your results won't match their results. If you're working on a SAT solver, you'll find easy instances where every related paper I've read says you should find hard ones. There's nothing magical about it, just established convention at this point. If you want to cite counterexamples, then do that. $\endgroup$ – Kyle Jones Dec 25 '11 at 1:45

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.