The maximum length of prime implicates for instances of 3-SAT

Autor: Trevor J. M. Bench-Capon, Paul E. Dunne
Rok vydání: 1997
Předmět:
Zdroj: Artificial Intelligence. 92(1-2):317-329
ISSN: 0004-3702
DOI: 10.1016/s0004-3702(97)00018-0
Popis: Schrag and Crawford (1996) present strong experimental evidence that the occurrence of prime implicates of varying lengths in random instances of 3-SAT exhibits behaviour similar to the well-known phase transition phenomenon associated with satisfiability. Thus, as the ratio of number of clauses ( m ) to number of prepositional variables ( n ) increases, random instances of 3-SAT progress from formulae which are generally satisfiable through to formulae which are generally not satisfiable, with an apparent sharp threshold being crossed when m/n ∼ 4.2. For instances of 3-SAT, Schrag and Crawford (1996) examine with what probability the longest prime implicate has length k (for k ⩾ 0)—unsatisfiable formulae correspond to those having only a prime implicate of length 0—demonstrating that similar behaviour arises. It is observed by Schrag and Crawford (1996) that experiments failed to identify any instance of 3-SAT over nine propositional variables having a prime implicate of length 7 or greater, and it is conjectured that no such instances are possible. In this note we present a combinatorial argument establishing that no 3-SAT instance on n variables can have a prime implicate whose length exceeds max {[n/2] + 1, [2n/3]}, validating this conjecture for the case n = 9. We further show that these bounds are the best possible. An easy corollary of the latter constructions is that for all k > 3, instances of k -SAT on n variables can be formed, that have prime implicates of length n − o(n).
Databáze: OpenAIRE