What is the precise definition of Random K-SAT?

Question

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?

Answer 1

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

Answer 2

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