cp's OEIS Frontend

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.

%I A380518 #93 Feb 26 2025 06:31:50
%S A380518 1,1,1,3,3,1,1,6,21,47,69,69,47,21,6,1,1,10,82,573,3176,14066,50646,
%T A380518 150508,374266,787691,1415279,2184842,2911290,3358258,3358258,2911290,
%U A380518 2184842,1415279,787691,374266,150508,50646,14066,3176,573,82,10,1
%N 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.
%C A380518 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 A380518 In total there are 3^n distinct clauses. This sequence counts sets of clauses up to permutation of the variables.
%C A380518 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.
%H A380518 Andrew Howroyd, <a href="/A380518/b380518.txt">Table of n, a(n) for n = 0..1099</a> (rows 0..6)
%H A380518 Frank Schwidom, <a href="https://github.com/schwidom/research/blob/master/cnf_enumeration/swi-prolog_001/cnf_enumeration_A380518.pl">Prolog code to prove the sequence</a>.
%H A380518 Wikipedia, <a href="https://en.wikipedia.org/wiki/Conjunctive_normal_form">Conjunctive normal form</a>.
%F A380518 T(n,0) = T(n,3^n) = 1.
%F A380518 T(n,k) = T(n,3^n-k).
%F A380518 T(n,k) = A380610(n,k-1) + A380610(n,k) for 0 < k < 3^n.
%e A380518 Triangle begins:
%e A380518  0 | 1,  1;
%e A380518  1 | 1,  3,  3,   1;
%e A380518  2 | 1,  6, 21,  47,   69,    69,    47,     21,      6,      1;
%e A380518  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;
%e A380518      ...
%e A380518 The enumeration scheme:
%e A380518 The positions of the numbers 0, 1, 2 represent the literals.
%e A380518 The numbers represent: 0 for an inverted literal, 1 for a set literal and 2 for a not used literal.
%e A380518 A list of lists written in brackets ([]) represents a conjunction of disjunctions.
%e A380518 Let's treat the first and second position as literal a and b.
%e A380518 The empty clause is denoted false, prefix operator ~ is not, infix operator \/ is or , infix operator /\ is and.
%e A380518 The T(2,1) = 6 representative formulas with 2 variables and 1 clause are:
%e A380518 [[2,2]] => false
%e A380518 [[1,2]] => (a)
%e A380518 [[1,1]] => (a \/ b)
%e A380518 [[0,2]] => (~a)
%e A380518 [[0,1]] => (~a \/ b)
%e A380518 [[0,0]] => (~a \/ ~b)
%e A380518 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 A380518 The T(2,2) = 21 representative formulas with 2 variables and 2 clauses are:
%e A380518 [[1,2],[2,2]] => (a) /\ false
%e A380518 [[1,2],[2,1]] => (a) /\ (b)
%e A380518 [[1,1],[2,2]] => (a \/ b) /\ false
%e A380518 [[1,1],[1,2]] => (a \/ b) /\ (a)
%e A380518 [[0,2],[2,2]] => (~a) /\ false
%e A380518 [[0,2],[2,1]] => (~a) /\ (b)
%e A380518 [[0,2],[2,0]] => (~a) /\ (~b)
%e A380518 [[0,2],[1,2]] => (~a) /\ (a)
%e A380518 [[0,2],[1,1]] => (~a) /\ (a \/ b)
%e A380518 [[0,1],[2,2]] => (~a \/ b) /\ false
%e A380518 [[0,1],[2,1]] => (~a \/ b) /\ (b)
%e A380518 [[0,1],[2,0]] => (~a \/ b) /\ (~b)
%e A380518 [[0,1],[1,2]] => (~a \/ b) /\ (a)
%e A380518 [[0,1],[1,1]] => (~a \/ b) /\ (a \/ b)
%e A380518 [[0,1],[1,0]] => (~a \/ b) /\ (a \/ ~b)
%e A380518 [[0,1],[0,2]] => (~a \/ b) /\ (~a)
%e A380518 [[0,0],[2,2]] => (~a \/ ~b) /\ false
%e A380518 [[0,0],[1,2]] => (~a \/ ~b) /\ (a)
%e A380518 [[0,0],[1,1]] => (~a \/ ~b) /\ (a \/ b)
%e A380518 [[0,0],[0,2]] => (~a \/ ~b) /\ (~a)
%e A380518 [[0,0],[0,1]] => (~a \/ ~b) /\ (~a \/ b)
%o A380518 (PARI) \\ compare A052265.
%o A380518 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 A380518 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 A380518 Row(n)={my(s=0); forpart(q=n, s+=permcount(q)*Fix(q, x)); Vecrev(s/n!)}
%o A380518 { for(n=0, 4, print(Row(n))) } \\ _Andrew Howroyd_, Jan 26 2025
%Y A380518 Row sums are 2*A380630.
%Y A380518 Row lengths give A034472.
%Y A380518 Column k=1 gives the nonzero terms of A000217.
%Y A380518 Cf. A052265, A380610.
%K A380518 nonn,tabf
%O A380518 0,4
%A A380518 _Frank Schwidom_, Jan 26 2025