A380518 Irregular triangle read by rows: T(n,k) is the number of non-isomorphic formulas in conjunctive normal form (CNF) with n variables and k distinct clauses up to permutations of the variables and clauses, 0 <= k <= 3^n.

1, 1, 1, 3, 3, 1, 1, 6, 21, 47, 69, 69, 47, 21, 6, 1, 1, 10, 82, 573, 3176, 14066, 50646, 150508, 374266, 787691, 1415279, 2184842, 2911290, 3358258, 3358258, 2911290, 2184842, 1415279, 787691, 374266, 150508, 50646, 14066, 3176, 573, 82, 10, 1

Offset: 0

Author

Frank Schwidom, Jan 26 2025

Keywords

• nonn
• tabf

Comments

Each clause is a disjunction of zero or more literals where each literal is a variable or its negation. A variable and its negation cannot appear in the same clause.

In total there are 3^n distinct clauses. This sequence counts sets of clauses up to permutation of the variables.

Equivalently, T(n,k) is the number of k X n matrices with distinct rows and entries in 0..2 up to permutations of rows and columns. Each row of the matrix corresponds with a clause and columns correspond with variables.

Examples

			Triangle begins:
 0 | 1,  1;
 1 | 1,  3,  3,   1;
 2 | 1,  6, 21,  47,   69,    69,    47,     21,      6,      1;
 3 | 1, 10, 82, 573, 3176, 14066, 50646, 150508, 374266, 787691, 1415279, 2184842,  2911290, 3358258, 3358258, 2911290, 2184842, 1415279, 787691, 374266, 150508, 50646, 14066, 3176, 573, 82, 10, 1;
     ...
The enumeration scheme:
The positions of the numbers 0, 1, 2 represent the literals.
The numbers represent: 0 for an inverted literal, 1 for a set literal and 2 for a not used literal.
A list of lists written in brackets ([]) represents a conjunction of disjunctions.
Let's treat the first and second position as literal a and b.
The empty clause is denoted false, prefix operator ~ is not, infix operator \/ is or , infix operator /\ is and.
The T(2,1) = 6 representative formulas with 2 variables and 1 clause are:
[[2,2]] => false
[[1,2]] => (a)
[[1,1]] => (a \/ b)
[[0,2]] => (~a)
[[0,1]] => (~a \/ b)
[[0,0]] => (~a \/ ~b)
In the above, (b), (~b) and (a \/ ~b) do not appear because they are essentially the same as another after swapping the a and b variables.
The T(2,2) = 21 representative formulas with 2 variables and 2 clauses are:
[[1,2],[2,2]] => (a) /\ false
[[1,2],[2,1]] => (a) /\ (b)
[[1,1],[2,2]] => (a \/ b) /\ false
[[1,1],[1,2]] => (a \/ b) /\ (a)
[[0,2],[2,2]] => (~a) /\ false
[[0,2],[2,1]] => (~a) /\ (b)
[[0,2],[2,0]] => (~a) /\ (~b)
[[0,2],[1,2]] => (~a) /\ (a)
[[0,2],[1,1]] => (~a) /\ (a \/ b)
[[0,1],[2,2]] => (~a \/ b) /\ false
[[0,1],[2,1]] => (~a \/ b) /\ (b)
[[0,1],[2,0]] => (~a \/ b) /\ (~b)
[[0,1],[1,2]] => (~a \/ b) /\ (a)
[[0,1],[1,1]] => (~a \/ b) /\ (a \/ b)
[[0,1],[1,0]] => (~a \/ b) /\ (a \/ ~b)
[[0,1],[0,2]] => (~a \/ b) /\ (~a)
[[0,0],[2,2]] => (~a \/ ~b) /\ false
[[0,0],[1,2]] => (~a \/ ~b) /\ (a)
[[0,0],[1,1]] => (~a \/ ~b) /\ (a \/ b)
[[0,0],[0,2]] => (~a \/ ~b) /\ (~a)
[[0,0],[0,1]] => (~a \/ ~b) /\ (~a \/ b)
		

Links

• Andrew Howroyd, Table of n, a(n) for n = 0..1099 (rows 0..6)
• Frank Schwidom, Prolog code to prove the sequence.
• Wikipedia, Conjunctive normal form.

Crossrefs

Row sums are 2*A380630.

Row lengths give A034472.

Column k=1 gives the nonzero terms of A000217.

Cf. A052265, A380610.

Programs

PARI

\\ compare A052265.
permcount(v) = {my(m=1, s=0, k=0, t); for(i=1, #v, t=v[i]; k=if(i>1&&t==v[i-1], k+1, 1); m*=t*k; s+=t); s!/m}
Fix(q, x)={my(v=divisors(lcm(Vec(q))), u=apply(t->3^sum(j=1, #q, gcd(t, q[j])), v)); prod(i=1, #v, my(t=v[i]); (1+x^t)^(sum(j=1, i, my(d=t/v[j]); if(!frac(d), moebius(d)*u[j]))/t))}
Row(n)={my(s=0); forpart(q=n, s+=permcount(q)*Fix(q, x)); Vecrev(s/n!)}
{ for(n=0, 4, print(Row(n))) } \\ Andrew Howroyd, Jan 26 2025

Formula

T(n,0) = T(n,3^n) = 1.

T(n,k) = T(n,3^n-k).

T(n,k) = A380610(n,k-1) + A380610(n,k) for 0 < k < 3^n.