cp's OEIS Frontend

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.

%I A380610 #44 Feb 26 2025 06:32:22
%S A380610 1,1,2,1,1,5,16,31,38,31,16,5,1,1,9,73,500,2676,11390,39256,111252,
%T A380610 263014,524677,890602,1294240,1617050,1741208,1617050,1294240,890602,
%U A380610 524677,263014,111252,39256,11390,2676,500,73,9,1,1,14,238,4320,72225,1039086,12712546,133231940,1211353657
%N 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.
%C A380610 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.
%C A380610 In total there are 3^n-1 distinct nonempty clauses. This sequence counts sets of clauses up to permutations of the variables.
%C A380610 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.
%H A380610 Andrew Howroyd, <a href="/A380610/b380610.txt">Table of n, a(n) for n = 0..1092</a> (rows 0..6)
%H A380610 Frank Schwidom, <a href="https://github.com/schwidom/research/blob/master/cnf_enumeration/swi-prolog_001/cnf_enumeration_A380610.pl">Prolog code to prove the sequence</a>.
%e A380610 Triangle begins:
%e A380610   0 | 1;
%e A380610   1 | 1, 2,  1;
%e A380610   2 | 1, 5, 16,  31,   38,    31,    16,  5,  1;
%e A380610   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;
%e A380610   ...
%e A380610 The T(2,1) = 5 representative formulas with 2 variables and 1 clause are:
%e A380610   [[1,2]] => (a)
%e A380610   [[1,1]] => (a \/ b)
%e A380610   [[0,2]] => (~a)
%e A380610   [[0,1]] => (~a \/ b)
%e A380610   [[0,0]] => (~a \/ ~b).
%e A380610 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.
%e A380610 The T(2,2) = 16 representative formulas with 2 variables and 2 clauses are:
%e A380610   [[1,2],[2,1]] => (a) /\ (b)
%e A380610   [[1,1],[1,2]] => (a \/ b) /\ (a)
%e A380610   [[0,2],[2,1]] => (~a) /\ (b)
%e A380610   [[0,2],[2,0]] => (~a) /\ (~b)
%e A380610   [[0,2],[1,2]] => (~a) /\ (a)
%e A380610   [[0,2],[1,1]] => (~a) /\ (a \/ b)
%e A380610   [[0,1],[2,1]] => (~a \/ b) /\ (b)
%e A380610   [[0,1],[2,0]] => (~a \/ b) /\ (~b)
%e A380610   [[0,1],[1,2]] => (~a \/ b) /\ (a)
%e A380610   [[0,1],[1,1]] => (~a \/ b) /\ (a \/ b)
%e A380610   [[0,1],[1,0]] => (~a \/ b) /\ (a \/ ~b)
%e A380610   [[0,1],[0,2]] => (~a \/ b) /\ (~a)
%e A380610   [[0,0],[1,2]] => (~a \/ ~b) /\ (a)
%e A380610   [[0,0],[1,1]] => (~a \/ ~b) /\ (a \/ b)
%e A380610   [[0,0],[0,2]] => (~a \/ ~b) /\ (~a)
%e A380610   [[0,0],[0,1]] => (~a \/ ~b) /\ (~a \/ b).
%o A380610 (PARI)
%o A380610 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}
%o A380610 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))}
%o A380610 Row(n)={my(s=0); forpart(q=n, s+=permcount(q)*Fix(q, x)); Vecrev(s/n!/(1 + x))}
%o A380610 { for(n=0, 4, print(Row(n))) } \\ _Andrew Howroyd_, Jan 30 2025
%Y A380610 Cf. A000244 (row lengths), A371830, A380518, A380630 (row sums).
%K A380610 nonn,tabf
%O A380610 0,3
%A A380610 _Frank Schwidom_, Jan 28 2025
%E A380610 More terms from _Andrew Howroyd_, Jan 30 2025