<p>Paul Beame has two papers (with various coauthors) where the resolution complexity of certain distributions of random formulas are studied. These formulas arise by expressing properties, such as k-colorability or having independent sets of size k, of random graphs from the usual distribution $G(n,p)$. Here are the links:</p>

<p><a href="http://www.springerlink.com/content/x2128h4432881310/" rel="noreferrer">Paul Beame, Russell Impagliazzo, and Ashish Sabharwal. The resolution complexity of independent sets and vertex covers in random graphs. Computational Complexity, 16(3):245-297, 2007.</a></p>

<p><a href="http://www.sciencedirect.com/science/article/pii/S0166218X0500168X" rel="noreferrer">Paul Beame, Joe Culberson, David Mitchell, and Cristopher Moore. The resolution complexity of random graph k-colorability. Discrete Applied Mathematics, 153:25-47, 2005.</a></p>

CC BY-SA 3.0
2011-09-23T12:58:09.340Z
2011-09-23T12:58:09.340Z
Jan Johannsen
<p>There is a recent preprint that studies the satisfiability properties of a family of distributions of 3-CNF formulas, where the clauses are not independent, but only <span class="math-container">$k$</span>-wise independent:</p>
<p><a href="https://arxiv.org/abs/2411.03813" rel="nofollow noreferrer">On the satisfiability of random 3-SAT formulas with k-wise independent clauses</a></p>

CC BY-SA 4.0
2024-11-08T10:58:25.787Z
2024-11-08T10:58:25.787Z
Jan Johannsen
<p>It is well known that random $ k $-CNF formulas over $ n $ variables with $ cn $ clauses are unsatisfiable (i.e. they are contradictions) with high probability, for sufficiently large constant $ c $. Thus, random $ k $-CNF formulas (for $ c $ large enough) constitute a natural distribution over unsatisfiable Boolean formulas (or dually, over tautologies, i.e. negations of contradictions). This distribution has been studied extensively.</p>

<p><strong>My question is the following</strong>: <em>are there any other established distributions over propositional tautologies or contradictions, that can be considered as capturing the "average-case" of tautologies or unsatisfiable formulas? Have these distributions been intensively studied?</em></p>

CC BY-SA 2.5
2011-03-08T03:55:55.683Z
@Tayfun Pay, CNF-TAUT is trivial to solve (as is DNF-SAT). See Massimo's comment above. (A refutation for a CNF means a proof of its negation which is a DNF, the complete phrase is "refutation proof" but "proof" is also quite common in the literature.)
Kaveh
CC BY-SA 2.5
2011-03-02T19:00:27.033Z
@Iddo Tautologies do not exists in a "true" CNF model because otherwise you would need to have a literal and its complement in the same clause.... Tautologies are not interesting to study in CNF.
Tayfun Pay
CC BY-SA 2.5
2011-03-03T06:41:06.890Z
@Pay, the negation of an unsatisfiable formula is obviously a tautology. Hence, we can consider random k-CNF's as a distribution over tautologies (when the clause-to-variable ratio is large enough, and where there is an o(1) probability for a k-CNF to be satisfiable).
Iddo Tzameret
CC BY-SA 2.5
2011-03-03T23:18:43.447Z
I think that Tayfun is right.  You should speak of either CNF formulas being unsatisfiable or DNF formulas being tautologies.  In the current question, you are mixing the two.
Tsuyoshi Ito
CC BY-SA 2.5
2011-03-04T01:30:19.900Z
I added the term "contradiction" to avoid 
the confusion.
Iddo Tzameret
CC BY-SA 2.5
2011-03-04T02:49:09.130Z
This is my last comment on this matter: I do not know why you insist to keep the word “tautologies,” which is clearly wrong as Tayfun explained.  But I am fine if you do not want to incorporate other people’s comments to improve the wording of your question.
Tsuyoshi Ito
CC BY-SA 2.5
2011-03-04T03:52:14.053Z
I prefer to keep the term 'tautologies'
 in the title because I'm asking about distributions on either tautologies or contradictions, and the question is phrased accordingly.
Iddo Tzameret
CC BY-SA 2.5
2011-03-04T10:54:53.917Z
I guess Iddo is using the canonical terminology of Proof Complexity, where often the terms 'proof' and 'refutation' are used as synonymous with no ambiguity. This also happens with the corresponding languages TAUT and UNSAT, usually restricted to DNF and CNF respectively.  Saying 'proof for a CNF' of course  means 'refutation'.
MassimoLauria
CC BY-SA 2.5
2011-03-04T16:04:22.903Z
@Iddo I do not think anyone has studied tautologies in CNF formulas. Perhaps in DNF formulas. I think you should word it accordingly as well.
Tayfun Pay
<cc.complexity-theory><reference-request><lo.logic><sat><random-k-sat>
Average-case tautologies/contradictions, beyond the random k-CNF model
Iddo Tzameret
# Average-case tautologies/contradictions, beyond the random k-CNF model

(Asked by: username_0 on 2011-03-02)

It is well known that random $ k $-CNF formulas over $ n $ variables with $ cn $ clauses are unsatisfiable (i.e. they are contradictions) with high probability, for sufficiently large constant $ c $. Thus, random $ k $-CNF formulas (for $ c $ large enough) constitute a natural distribution over unsatisfiable Boolean formulas (or dually, over tautologies, i.e. negations of contradictions). This distribution has been studied extensively.

**My question is the following**: *are there any other established distributions over propositional tautologies or contradictions, that can be considered as capturing the "average-case" of tautologies or unsatisfiable formulas? Have these distributions been intensively studied?*

**Tags:** cc.complexity-theory, reference-request, lo.logic, sat, random-k-sat
> **Comments:**
> **username_2**: @Iddo Tautologies do not exists in a "true" CNF model because otherwise you would need to have a literal and its complement in the same clause.... Tautologies are not interesting to study in CNF.  
> **username_0**: @Pay, the negation of an unsatisfiable formula is obviously a tautology. Hence, we can consider random k-CNF's as a distribution over tautologies (when the clause-to-variable ratio is large enough, and where there is an o(1) probability for a k-CNF to be satisfiable).  
> **username_3**: I think that Tayfun is right.  You should speak of either CNF formulas being unsatisfiable or DNF formulas being tautologies.  In the current question, you are mixing the two.  
> **username_0**: I added the term "contradiction" to avoid  the confusion.  
> **username_3**: This is my last comment on this matter: I do not know why you insist to keep the word “tautologies,” which is clearly wrong as Tayfun explained.  But I am fine if you do not want to incorporate other people’s comments to improve the wording of your question.  
> **username_0**: I prefer to keep the term 'tautologies'  in the title because I'm asking about distributions on either tautologies or contradictions, and the question is phrased accordingly.  
> **username_4**: I guess Iddo is using the canonical terminology of Proof Complexity, where often the terms 'proof' and 'refutation' are used as synonymous with no ambiguity. This also happens with the corresponding languages TAUT and UNSAT, usually restricted to DNF and CNF respectively.  Saying 'proof for a CNF' of course  means 'refutation'.  
> **username_2**: @Iddo I do not think anyone has studied tautologies in CNF formulas. Perhaps in DNF formulas. I think you should word it accordingly as well.  
> **username_1**: @Tayfun Pay, CNF-TAUT is trivial to solve (as is DNF-SAT). See Massimo's comment above. (A refutation for a CNF means a proof of its negation which is a DNF, the complete phrase is "refutation proof" but "proof" is also quite common in the literature.)  

---

## 2 answers

### Answer by username_5 on 2011-09-23. Score: 5

Paul Beame has two papers (with various coauthors) where the resolution complexity of certain distributions of random formulas are studied. These formulas arise by expressing properties, such as k-colorability or having independent sets of size k, of random graphs from the usual distribution $G(n,p)$. Here are the links:

[Paul Beame, Russell Impagliazzo, and Ashish Sabharwal. The resolution complexity of independent sets and vertex covers in random graphs. Computational Complexity, 16(3):245-297, 2007.](http://www.springerlink.com/content/x2128h4432881310/)

[Paul Beame, Joe Culberson, David Mitchell, and Cristopher Moore. The resolution complexity of random graph k-colorability. Discrete Applied Mathematics, 153:25-47, 2005.](http://www.sciencedirect.com/science/article/pii/S0166218X0500168X)


---

### Answer by username_5 on 2024-11-08. Score: 1

There is a recent preprint that studies the satisfiability properties of a family of distributions of 3-CNF formulas, where the clauses are not independent, but only $k$-wise independent:

[On the satisfiability of random 3-SAT formulas with k-wise independent clauses](https://arxiv.org/abs/2411.03813)


---

