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,1

Comments

A Krom function is equivalent to a Boolean function with the property that, if f(x)=f(y)=f(z)=1, then f(<xyz>)=1, where <xyz> 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.

Links

Table of n, a(n) for n=0..8.

Crossrefs

Cf. A109458, A109459, A102897.

Cf. A112535.

Sequence in context: A061588 A202360 A050472 * A352801 A105788 A217727

Adjacent sequences: A109454 A109455 A109456 * A109458 A109459 A109460

Keyword

nonn,hard,more

Author

Don Knuth, Aug 24 2005

Status

approved