A109457 Number of Krom functions on n variables (or 2SAT instances): conjunctions of clauses with two literals per clause.

2, 4, 16, 166, 4170, 224716, 24445368, 5167757614, 2061662323954

Offset: 0

Author

Don Knuth, Aug 24 2005

Keywords

• nonn
• hard
• more

Comments

A Krom function is equivalent to a Boolean function with the property that, if f(x)=f(y)=f(z)=1, then f()=1, where denotes the bitwise median of the three Boolean vectors x, y, z.

Also related to number of retracts of an n-cube (see Feder).

References

• Tomas Feder, Stable Networks and Product Graphs, Memoirs of the American Mathematical Society, 555 (1995), Section 3.2.
• D. E. Knuth, The Art of Computer Programming, Vol. 4A, Section 7.1.1, p. 79.
• Knuth, Donald E., Satisfiability, Fascicle 6, volume 4 of The Art of Computer Programming. Addison-Wesley, 2015, pages 148 and 220, Problem 191.
• M. R. Krom, The decision problem for a class of first-order formulas in which all disjunctions are binary, Zeitschrift f. mathematische Logik und Grundlagen der Mathematik, 13 (1967), 15-20.
• Thomas J. Schaefer, The complexity of satisfiability problems, ACM Symposium on Theory of Computing, 10 (1978), 216-226.

Crossrefs

Cf. A109458, A109459, A102897.

Cf. A112535.