×

The maximum length of prime implicates for instances of 3-SAT. (English) Zbl 1017.68512

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)
PDFBibTeX XMLCite
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.