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 K2)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 formulaWhat would be the most correct definition? What are the cons and pros of using these different definitions? 
What is the precise definition of Random K-SAT?
cc.complexity theory;sat;randomness;phase transition
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 QBFAs 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 1997Gent + Walsh Beyond NP: the QSAT phase transition. AAAI/IAAI 1999Chen + Interian A Model for Generating Random Quantified Boolean Formulas. IJCAI 2005