15

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?

Iddo Tzameret
  • 1,899
  • 1
  • 19
  • 27
  • 1
    @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 Mar 02 '11 at 19:00
  • 1
    @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 Mar 03 '11 at 06:41
  • 1
    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 Mar 03 '11 at 23:18
  • I added the term "contradiction" to avoid the confusion. – Iddo Tzameret Mar 04 '11 at 01:30
  • 1
    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 Mar 04 '11 at 02:49
  • 3
    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 Mar 04 '11 at 03:52
  • 1
    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 Mar 04 '11 at 10:54
  • @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 Mar 04 '11 at 16:04
  • 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.) – Kaveh Mar 08 '11 at 03:55

1 Answers1

4

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.

Paul Beame, Joe Culberson, David Mitchell, and Cristopher Moore. The resolution complexity of random graph k-colorability. Discrete Applied Mathematics, 153:25-47, 2005.

Jan Johannsen
  • 4,630
  • 2
  • 33
  • 50