Dunne, Paul E.; Bench-Capon, Trevor J. M. The maximum length of prime implicates for instances of 3-SAT. (English) Zbl 1017.68512 Artif. Intell. 92, No. 1-2, 317-329 (1997). Summary: 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 propositional 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 \sim 4.2\). For instances of 3-SAT, Schrag and Crawford (1996) examine with what probability the longest prime implicate has length \(k\) (for \(k \geq 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 \{{\lceil} n/2{\rceil}+1, {\lfloor} 2n/3{\rfloor}\}\), 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)\). MSC: 68Q25 Analysis of algorithms and problem complexity 03B05 Classical propositional logic 03D15 Complexity of computation (including implicit computational complexity) Keywords:3-CNF formulae; Prime implicates; Satisfiability PDFBibTeX XMLCite \textit{P. E. Dunne} and \textit{T. J. M. Bench-Capon}, Artif. Intell. 92, No. 1--2, 317--329 (1997; Zbl 1017.68512) Full Text: DOI References: [1] Aspvall, B.; Plass, M. F.; Tarjan, R. E., A linear-time algorithm for testing the truth of certain quantified boolean formulas, Inform. Process. Lett., 8, 121-123 (1979) · Zbl 0398.68042 [2] Goerdt, A., A threshold for unsatisfiability, (Havel, J.; Krbec, V., Proceedings 17th Symposium on Mathematical Foundations of Computer Science. Proceedings 17th Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, 629 (1992), Springer: Springer Berlin), 264-274 · Zbl 1494.68095 [3] Schrag, R.; Crawford, J. M., Implicates and prime implicates in random 3-SAT, Artif. Intell, 81, 199-222 (1996) · Zbl 1508.68345 This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.