A380610 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 nonempty clauses up to permutations of the variables and clauses, 0 <= k < 3^n.

1, 1, 2, 1, 1, 5, 16, 31, 38, 31, 16, 5, 1, 1, 9, 73, 500, 2676, 11390, 39256, 111252, 263014, 524677, 890602, 1294240, 1617050, 1741208, 1617050, 1294240, 890602, 524677, 263014, 111252, 39256, 11390, 2676, 500, 73, 9, 1, 1, 14, 238, 4320, 72225, 1039086, 12712546, 133231940, 1211353657

Offset: 0

Author

Frank Schwidom, Jan 28 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-1 distinct nonempty clauses. This sequence counts sets of clauses up to permutations of the variables.

Equivalently, T(n,k) is the number of k X n matrices with distinct rows, entries in 0..2 and no all zero row 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, 2,  1;
  2 | 1, 5, 16,  31,   38,    31,    16,  5,  1;
  3 | 1, 9, 73, 500, 2676, 11390, 39256, 111252, 263014, 524677, 890602, 1294240, 1617050, 1741208, 1617050, 1294240, 890602, 524677, 263014, 111252, 39256, 11390, 2676, 500, 73, 9, 1;
  ...
The T(2,1) = 5 representative formulas with 2 variables and 1 clause are:
  [[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) = 16 representative formulas with 2 variables and 2 clauses are:
  [[1,2],[2,1]] => (a) /\ (b)
  [[1,1],[1,2]] => (a \/ b) /\ (a)
  [[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,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],[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..1092 (rows 0..6)
• Frank Schwidom, Prolog code to prove the sequence.

Crossrefs

Cf. A000244 (row lengths), A371830, A380518, A380630 (row sums).

Programs

PARI

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!/(1 + x))}
{ for(n=0, 4, print(Row(n))) } \\ Andrew Howroyd, Jan 30 2025

Extensions

More terms from Andrew Howroyd, Jan 30 2025