#Distinct Tautologies & generalization to boxes #Anthony Zaleski, 2017 print(`This Maple package accompanies the article`): print(`Boolean Function Analogs of Covering Systems`): print(`by Anthony Zaleski and Doron Zeilberger `): print(``): print(`dt.txt:`): print(`Distinct Tautologies & Box Coverings`): print(`By Anthony Zaleski, Summer 2017`): print(`NOTE: do not assign to the names x,y.`): print(`Enter Help(); to begin.`): print(`---`): with(combinat): with(Logic): with(ListTools): Help:=proc() local EG: EG:=`For example, try`: if nargs=0 then print(`dt.txt contains the following primary procedures.`): print(`Type Help(); for help on a specific procedure.`): print(`Type Help(1); for auxiliary procedures.`): print(`RandDT,Anm,An,Bn`): print(`FindDT,GreedyDT,GoodDT,GoodDTr,FindExact`): print(`DensityBound1 `): print(`TTB,GoodDTB, Paper1, Paper2 `): elif args[1]=1 then print(`dt.txt contains the following auxiliary procedures:`): print(`Taut,MapleTaut,RandNF,TT, GoodDT1 `): elif args[1]=FindExact then print(`FindExact(L,n): inputs a list L of subsets of [n]. Outputs an exact DNF`): print(`greedily constructed to cover the most points in 2^[n].`): print(EG): print(`FindExact([{1,2,3},{3,4},{1,4,5,6}],6);`): elif args[1]=DensityBound1 then print(`DensityBound1(S): given a list of sets S (signed or not),`): print(`gives an upper bound on the density of a DNF on S,`): print(`obtained by partitioning S into families of mutually independent clauses.`): print(EG): print(`DensityBound1([{1,2,3},{3,4,5},{6,7}]);`): elif args[1]=TTB then print(`TTB(f,B): Given f, a set of box clauses (convention:`): print(`{[1,2],[2,3]} means x1=2 and x2=3) and a list B specifying`): print(`the box (convention: 1<=xi<=B[i]), outputs the set`), print(`of points satisfying at least one of the clauses.`): print(EG): print(`TTB({{[1,2],[3,1]},{[2,2]}},[2,3,2]);`): elif args[1]=GoodDTB then print(`GoodDTB(B,m1,m2): given list B specifying the box`): print(`(convention: 1<=xi<=B[i]), greedily finds a generalized`): print(`distinct DNF f (convention: {[1,2],[2,3]} means x1=2 and x2=3)`): print(`with clause sizes in [m1,m2]`): print(EG): print(`GoodDTB([2$5],3,4);`): elif args[1]=GoodDTr then print(`GoodDTr(n,m1,m2):Tries to find a distinct tautology `): print(`in n variables with clauses of size between m1 and m2.`): print(`uses a randomized clause order.`): print(EG): print(`GoodDTr(5,3,4);`): elif args[1]=GoodDT then print(`GoodDT(n,m1,m2):Tries to find a distinct tautology `): print(`in n variables with clauses of size between m1 and m2.`): print(EG): print(`GoodDT(5,3,4);`): elif args[1]=GoodDT1 then print(`GoodDT1(n,S):Tries to find a distinct tautology with monomials with support S`): print(`in n variables `): print(EG): print(`GoodDT1({{1},{2},{3},{1,2,3}},3);`): elif args[1]=TT then print(`TT(S,n): the subset of the n-dimensional unit cube that satisfies the DNF S.`): print(EG): print(`TT({{1,2},{-2,3}},3);`): elif args[1]=GreedyDT then print(`GreedyDT(n,m1,m2): greedily looks for a distinct tautology`): print(`on n variables with clause sizes in [m1,m2].`): print(EG): print(`GreedyDT(5,3,5);`): elif args[1]=RandDT then print(`RandDT(n,m1,m2): outputs a random DNF supported on`): print(`the subsets of [n] with sizes in [m1,m2].`): print(EG): print(`RandDT(5,3,4);`): elif args[1]=Anm then print(`Anm(n,m): upper bound on the density of a distinct DNF in n variables,`): print(`with minimum clause size m.`): print(EG): print(`Anm(5,3);`): elif args[1]=An then print(`An(n): the largest m such that binomial(n,m)/2^m+ ... + binomial(n,n)/2^n>1,`): print(`a distinct tautology on n variables`): print(EG): print(`An(5);`): elif args[1]=Bn then print(`Bn(n): the largest m such that binomial(n,m)/2^m>1 `): print(EG): print(`Bn(5);`): elif args[1]=FindDT then print(`FindDT(n,m1,m2,K): searches randomly for a distinct tautology`): print(`supported on the subsets of [n] with sizes in [m1,m2]. If K random`): print(`candidates yield no winners, returns FAIL.`): print(EG): print(`FindDT(5,3,4,10000);`): elif args[1]=Taut then print(`Taut(S,K): using K-step inclusion-exclusion, outputs [ans,k]`): print(`where ans=true if the DNF S (a set of sets of ints) is a tautology, false if not,`): print(`and p=probability bound if inconclusive; and k is the number of`): print(`steps taken until it terminated.`): print(EG): print(`Taut({{-3, 1, 4}, {-2, -1, 4}}, 2); `): elif args[1]=RandNF then print(`RandNF(n,N,M:=3): Random normal form, as a set of sets of integers, with ~N clauses in n variables,`): print(`each clause having size ~M (3 by default).`): print(`RandNF(10,4);`): elif args[1]=Rand3SAT then print(`Rand3SAT(n,N): A random set of N sets of <=3 integers with absolute value between 1 and n.`): print(EG): print(`Rand3SAT(3,2); `): elif args[1]=Ar then print(`Ar(r,X): inputs a list of monomials in x[i],y[i], outputs sum all reduced r-products.`): print(EG): print(`Ar(3,[x[2]*y[2],x[1],y[1]*x[2],x[3]])`): elif args[1]=SAT1 then print(`SAT1(S,K): using Ar K times (potentially), outputs [ans,k]`): print(`where ans=true if S (a set of sets of ints) is a tautology, false if not,`): print(`and p=probability bound if inconclusive; and k is the number of`): print(`steps taken until it terminated.`): print(EG): print(`SAT1({{-3, 1, 4}, {-2, -1, 4}}, 2); `): elif args[1]=MapleTaut then print(`MapleTaut(S): using Maple's built in Tautology function, decides if the DNF`): print(`S (a set of sets of ints) is a tautology.`): print(`steps taken until it terminated.`): print(EG): print(`MapleTaut({{-3, 1, 4}, {-2, -1, 4}}); `): elif args[1]=MetaTaut then print(`MetaTaut(n,N,K,M): Runs Taut M times, with step limit K, on random 3-DNF`): print(`expressions with n variables and N clauses. Returns a list whose mth`): print(`entry is [time,output of Taut].`): print(EG): print(`MetaTaut(5,25,8,10);`): elif args[1]=MetaMapleTaut then print(`MetaTaut(n,N,M): Runs MapleTaut M times on random 3-DNF`): print(`expressions with n variables and N clauses. Returns a list whose mth`): print(`entry is [time,output of MapleTaut].`): print(EG): print(`MetaMapleTaut(5,25,10);`): #elif args[1]=PhaseShift then # print(`PhaseShift(n,k,M,p0): outputs a pair X,Y, where X is a list of`): # print('N values and Y is a list of probabilities elif args[1]=NFtoPG then print(`DNFtoPG(S): converts the DNF S to P,G where`): print(`P[i]=Pr[random assignment satisfies clause i in S] and`): print(`G[i]=set of j s.t. clause i,j are dependent in S`): print(EG): print(`DNFtoPG([{1,2,3},{4,5,6},{-2,4,5}]);`): elif args[1]=LLLs then print(`LLLs(P,G): checks if P,G satisfies the symmetric LLL`): print(`where P[i]=Pr[B_i] and G[i]={j<>i: B_i,B_j are dependent}`): print(`Note: the convention is B_i=event that clause i IS satisfied,`): print(`so if this returns true it means that the DNF is NOT a tautology.`): print(EG): print(`LLLs(DNFtoPG(RandNF(20,4)));`): elif args[1]=LLL then print(`LLL(P,G): checks if P,G satisfies the asymmetric LLL, with weights 1/(d+1),`): print(`where P[i]=Pr[B_i] and G[i]={j<>i: B_i,B_j are dependent}`): print(`Note: the convention is B_i=event that clause i IS satisfied,`): print(`so if this returns true it means that the DNF is NOT a tautology.`): print(EG): print(`LLL(DNFtoPG(RandNF(20,4)));`): elif args[1]=MetaLLL then print(`MetaLLL(n,N,M):`): print(`Runs LLL on M random DNFs generated`): print(`by RandNF(n,N) and returns A,B, where A is the proportion`): print(`of non-tautologies discovered by LLL, and B is the true proportion`): print(`of non-tautologies (found with MapleTaut).`): print(EG): print(`MetaLLL(20,5,100);`): elif args[1]=MetaLLLs then print(`MetaLLLs(n,N,M):`): print(`Runs LLLs on M random DNFs generated`): print(`by RandNF(n,N) and returns A,B, where A is the proportion`): print(`of non-tautologies discovered by LLL, and B is the true proportion`): print(`of non-tautologies (found with MapleTaut).`): print(EG): print(`MetaLLLs(20,5,100);`): elif args[1]=HowManyFinished then print(`HowManyFinished(n,N,k,M): runs Taut on RandNF(n,N)`): print(`M times, with threshold k, and outputs p,T, where p is`): print(`the proportion that finished, and T is the list`): print(`of the corresponding runtimes.`): print(EG): print(`HowManyFinished(20,15,4,100);`): elif args[1]=BestNei then print(`BestNei(S,n,r): inputs a distinct DNF of n variables, the pos. integer n, and a pos. integer r, outputs the`): print(`best neighbor distance <=r away from S, in the semse of covering greatest number of truth-vectors. Try: `): print(`BestNei({{1,2},{2,3}},3,2); `): elif args[1]=NiceDNF then print(`NiceDNF(S,x,y): inputs a set of sets of signed integers (representing a DNF) and transforms it into a monomial. Try:`): print(`NiceDNF({1,-2, 3},x,y);`): elif args[1]=NiceGDNF then print(`NiceGDNF(S,z): inputs a generalized DNF (from a box) and outputs it in nice notation as a polynomial, where`): print(`z[i1]^j1*z[i2]^j2... represents the subcube {x_i1=j1, x_i2=j2, ...}. Try: `): print(`NiceGDNF({[1,2]},x); `): elif args[1]=Paper1 then print(`Paper1(N): inputs a positive integer and outputs an article listing Distinct DNF tautologies, optimal in some sense`): print(`with all monomials of the SAME size. `): print(`for a number of variables from n=2 to n=N. Try:`): print(`Paper1(4);`): elif args[1]=Paper2 then print(`Paper2(N): inputs a positive integer and outputs an article listing Distinct DNF tautologies, optimal in some sense`): print(`with all monomials LARGER OR EQUAL than a certain size. `): print(`for a number of variables from n=2 to n=N. Try:`): print(`Paper2(4);`): elif args[1]=VeryGoodDTB then print(`VeryGoodDTB(B,W): inputs a list of integers B representing the dimensions of a box`): print(`and a set of subsets of {1, ..., nops(B)} tries to find a covering by sub-boxes with distinct supports`): print(`not using W. Try: `): print(`VeryGoodDTB([2,3,5,7,11],{{2}}):`): else print(`No such procedure exists.`): fi: end: #########SAT.txt Merge:=proc(s1,s2) local i,j: for i in s1 do for j in s2 do if i+j=0 then return false: fi: od: od: s1 union s2: end: Cleanup:=proc(S1) local S,s,pair: S:=S1: for s in S1 do for pair in choose(s,2) do if convert(pair,`+`)=0 then S:=S minus {s}: break: fi: od: od: S: end: Taut:=proc(S1,K) local S,n,N,Nset,T,T1,t,p,k,m: S:=Cleanup({op(S1)}): N:=nops(S): Nset:={seq(n,n=1..N)}: p:=0: T:={[[0],{}]}: for k from 1 to K do T1:={}: for t in T do for n from t[1][-1]+1 to N do m:=Merge(t[2],S[n]): if m<>false then T1:=T1 union {[[op(t[1]),n],m]}: fi: od: od: p:=p-(-1)^k*add(2^(-nops(t[2])),t in T1): T:=T1: if k mod 2=1 and p<1 then return [false,k]: fi: if k mod 2=0 and p=1 then return [true,k]: fi: od: [p,k]: end: DensityBound:=proc(S1,K) local S,n,N,Nset,T,T1,t,p,k,m: S:=Cleanup({op(S1)}): N:=nops(S): Nset:={seq(n,n=1..N)}: p:=0: T:={[[0],{}]}: for k from 1 to K do T1:={}: for t in T do for n from t[1][-1]+1 to N do m:=Merge(t[2],S[n]): if m<>false then T1:=T1 union {[[op(t[1]),n],m]}: fi: od: od: p:=p-(-1)^k*add(2^(-nops(t[2])),t in T1): T:=T1: if k mod 2=0 and p=1 then return [p,k]: fi: od: [p,K]: end: List2Pol:=proc(L) local i,j,L1,p: L1:=[]: for i from 1 to nops(L) do p:=1: for j from 1 to nops(L[i]) do if L[i][j]>0 then p:=p*x[L[i][j]]: else p:=p*y[-L[i][j]]: fi: od: L1:=[op(L1),p]: od: L1: end: Anti:=proc(X): subs({x=y,y=x},X): end: `&*`:=proc(p,q) local f,V,v: f:=expand(p*q): if nops(q)=1 then V:={q}: else V:={op(q)}: fi: applyrule([op({seq(v*Anti(v)=0,v in V)}),seq(v^2=v,v in V)],expand(p*q)): end: Ar:=proc(r,X) local n: option remember: n:=nops(X): if r=0 then return 1: fi: if nops(X)=0 then return 0: fi: expand(Ar(r,X[1..n-1])+Ar(r-1,X[1..n-1])&*X[n]): end: Rand3SAT:=proc(n,K) local i: randcomb(Cleanup(choose({seq(i,i=-n..n)} minus {0},3)),K): end: CleanupNF:=proc(S) local V,s,i: V:={seq(seq(abs(i),i in s),s in S)}: [seq({seq(sign(i)*Search(abs(i),V),i in s)},s in S)]: end: RandNF:=proc(n,K,M:=3) local k,m,ra1,ra2,s,S: S:=[]: ra1:=rand(1..n): ra2:=rand(0..1): for k from 1 to K do s:={}: for m from 1 to M do s:=s union {ra1()*(2*ra2()-1)}: od: S:=[op(S),s]: od: CleanupNF(S): end: PreSort:=proc(X) local L,i,j,P, output, permutation: L:=[0$nops(X)]: for i from 1 to nops(X) do for j from 1 to nops(X) do if X[i]&*X[j]=0 then L[i]:=L[i]+1: fi: od: od: P:=sort(L,output=permutation,`<`): X[P]: end: SAT1:=proc(S,K,ps:=false) local V,X,k,p,a,i,v: V:=applyrule([i::positive=x[i],i::negative=y[-i]],{seq(op(a),a in S)}): V:={seq(v=1/2,v in V)}: X:=List2Pol(S): if ps then X:=X[randperm(nops(X))]: fi: p:=0: for k from 1 to K do p:=p-(-1)^k*subs(V,Ar(k,X)): if k mod 2=1 and p<1 then return [false,k]: fi: if k mod 2=0 and p=1 then return [true,k]: fi: od: [p,k]: end: MetaTaut:=proc(n,N,K,M) local m,L,t,T,R: T:=[]: for m from 1 to M do R:=RandNF(n,N): t:=time(): L:=Taut(R,K): T:=[op(T),[time()-t,L]]: od: T: end: MetaMapleTaut:=proc(n,N,M) local m,L,t,T,R: T:=[]: for m from 1 to M do R:=RandNF(n,N): t:=time(): L:=MapleTaut(R): T:=[op(T),[time()-t,L]]: od: T: end: MapleTaut:=proc(S) local B,s,i: B:=&or(seq(&and(seq(applyrule([i::positive=x[i],i::negative=¬ x[-i]],i),i in s)),s in S)): Tautology(B): end: `&BPor`:=proc(a,b) #expand(1-(1-a)*(1-b)) mod 2: if nargs=1 then return args[1] else expand(1-(1-args[1])*(1-&BPor(args[2..nargs]))) mod 2: fi: end: `&BPand`:=proc() if nargs=1 then return args[1] else expand(args[1]*&BPand(args[2..nargs])) mod 2: fi: end: `&BPnot`:=proc(a) expand(1-a) mod 2: end: ToV:=proc(i) if i>0 then x[i]: else &BPnot(x[-i]): fi: end: SATtoBP:=proc(S) local s,i,V,a,p: V:=applyrule([i::positive=x[i],i::negative=x[-i]],{seq(op(a),a in S)}): applyrule([seq(v^(i::integer)=v,v in V)], &BPor(seq(&BPand(seq(ToV(i), i in s)),s in S)) ) mod 2: end: ################## DNFtoPG:=proc(S) local P,G,s,i,j,Nset: Nset:={seq(i,i=1..nops(S))}: P:=[seq(2^(-nops(s)), s in S)]: G:=Array([{}$nops(S)]): for i in Nset do for j in Nset minus {i} do if {seq(abs(s),s in S[i])} intersect {seq(abs(s),s in S[j])}<>{} then G[i]:=G[i] union {j}: fi: od: od: P,convert(G,list): end: #symmetric LLL #P[i]=Pr[B_i]; G[i]={neighbors of B_i in dependency graph}. LLLs:=proc(P,G) local p,d,e,g: e:=evalf(exp(1)): p:=max(P): d:=max(seq(nops(g),g in G)): evalb(e*p*(d+1)<=1): end: #asymmetric LLL LLL:=proc(P,G) local X,i: X:=[seq(1/(nops(G[i])+1),i=1..nops(G))]: for i from 1 to nops(P) do if P[i]>X[i]*mul(1-X[n],n in G[i]) then return false: fi: od: true: end: #run LLL and LLL on M DNFs with n variables, N clauses MetaLLL1:=proc(n,N,M) local L,l,m,PG,c,c0,j,S: L:=[]: c0:=0: c:=[0,0]: for m from 1 to M do S:=RandNF(n,N): PG:=DNFtoPG(S): l:=[MapleTaut(S), subs({true=false,false=FAIL},LLLs(PG)), subs({true=false,false=FAIL},LLL(PG))]: if not l[1] then c0:=c0+1: fi: for j from 1 to 2 do if l[j+1]=false then if l[1] then return FAIL: else c[j]:=c[j]+1: fi: fi: od: L:=[op(L),l]: od: L,evalf(c0/M),evalf(c[1]/c0),evalf(c[2]/c0): end: MetaLLL:=proc(n,N,M) local m,n1,n2,S: n1:=0: n2:=0: for m from 1 to M do S:=RandNF(n,N): if LLL(DNFtoPG(S))=true then n1:=n1+1: fi: if MapleTaut(S)=false then n2:=n2+1: fi: end: evalf(n1/M),evalf(n2/M): end: MetaLLLs:=proc(n,N,M) local m,n1,n2,S: n1:=0: n2:=0: for m from 1 to M do S:=RandNF(n,N): if LLLs(DNFtoPG(S))=true then n1:=n1+1: fi: if MapleTaut(S)=false then n2:=n2+1: fi: end: evalf(n1/M),evalf(n2/M): end: ############ HowManyFinished:=proc(n,N,k,M) local m,co,t,T,S: co:=0: T:=[]: for m from 1 to M do S:=RandNF(n,N): t:=time(): if member(Taut(S,k)[1],{true,false}) then T:=[op(T),time()-t]: co:=co+1: fi: od: evalf(convert(T,`+`)/M),T: end: AvgTime:=proc(n,N,k,M) local T: T:=HowManyFinished(n,N,k,M)[2]: T[1],convert(T,`+`)/nops(T): end: PhaseShift:=proc(n,k,M,p0) local N,Nlist,plist,p: plist:=[]: Nlist:=[]: for N from 1 while true do p:=HowManyFinished(n,N,k,M): if pp then p:=p1[1]: S3:=S2: fi: od: S:=S3: od: if not MapleTaut(S) then return FAIL: fi: S: end: An:=proc(n) local a,b,c: a:=1: b:=n: while b-a>1 do c:=floor((a+b)/2): if Anm(n,c)>=1 then a:=c: else b:=c: fi: od: a: end: #Bn(n): the largest m such binomial(n,m)/2^m>1 try: Bn(5); Bn:=proc(n) local m: for m from 1 while binomial(n,m)/2^m>1 do od: m-1: end: ###new code July 30, 2017 ez:=proc(): print(` TT1(C,n), TT(f,n), BestSign(f,n,C), BestSign(f,n,C), GoodDT1(L,n), GoodDT(n,m1,m2) `): end: #TT1(C,n): inputs a clause with n variables outputs the set of 2^(n-nops(C)) points that it contains TT1:=proc(C,n) local S,s: option remember: if n=0 then if C={} then RETURN({[]}): else RETURN({}): fi: fi: if (not member(n,C) and not member(-n,C)) then S:=TT1(C,n-1): RETURN({ seq([op(s),0],s in S), seq([op(s),1],s in S)}): elif member(n,C) then S:=TT1(C minus {n},n-1): RETURN({ seq([op(s),1],s in S)}): else S:=TT1(C minus {-n},n-1): RETURN({ seq([op(s),0],s in S)}): fi: end: #TT(f,n): the subset of the n-dim unit cube that satisfies f TT:=proc(f,n) local f1: {seq( op(TT1(f1,n)), f1 in f)}: end: #Veck(k): the set of {-1,1} vectors of length k Veck:=proc(k) local lu,lu1,i: lu:=TT1({},k): {seq([seq(2*lu1[i]-1,i=1..k)],lu1 in lu)}: end: #BestSign(f,n,C): inputs a Boolean function f of n variables (in DNF) and a clause C, finds the sign assignments that is best, and adds it to f BestSign:=proc(f,n,C) local gu,k,gu1,C1,i1,aluf,si,hal: k:=nops(C): gu:=Veck(k) minus {[1$k]}: aluf:=C: si:=nops(TT({aluf} union f,n)): for gu1 in gu do C1:={seq(C[i1]*gu1[i1],i1=1..k)}: hal:=nops(TT({C1} union f,n)): if hal>si then aluf:=C1: si:=hal: fi: od: f union {aluf}: end: #GoodDT1(L,n): inputs a list of clauses of n variables and outputs the sign assignments that makes it have as many points as possible. If it reaches 2^n #it stops GoodDT1:=proc(L,n) local f,i: f:={L[1]}: for i from 2 to nops(L) while nops(TT(f,n))<2^n do f:=BestSign(f,n,L[i]): od: f: end: #Neis1(S):all the neighbors of the DNF S obtained by changing one sign Neis1:=proc(S) local gu,i,j: gu:={}: for i from 1 to nops(S) do for j from 1 to nops(S[i]) do gu:=gu union { {op(1..i-1,S),{op(1..j-1,S[i]),-S[i][j],op(j+1..nops(S[i]), S[i])},op(i+1..nops(S),S)}}: od: od: gu: end: #Neis(S,r): all the neighbors of the DNF S obtained by changing at most r signs. Try: #Neis({{1,2},{2,3}},2); Neis:=proc(S,r) local gu,gu1: option remember: if r=0 then RETURN({S}): fi: gu:=Neis(S,r-1): {seq(op(Neis1(gu1)),gu1 in gu)}: end: #BestNei(S,n,r): inputs a distinct DNF of n variables, the pos. integer n, and a pos. integer r, outputs the #best neighbor distance <=r away from S, in the semse of covering greatest number of truth-vectors. Try #BestNei({{1,2},{2,3}},3,2); BestNei:=proc(S,n,r) local gu, aluf, si,gu1,hal: aluf:=S: si:=nops(TT(S,n)): gu:=Neis(S,r): for gu1 in gu do hal:=nops(TT(gu1,n)): if hal>si then aluf:=gu1: si:=hal: fi: od: aluf: end: #GoodDT(n,m1,m2): Tries to find a distinct tautology in n variables with clauses of size between m1 and m2. Try #GoodDT(5,3,4); GoodDT:=proc(n,m1,m2) local L,i,S,f: S:={seq(i,i=1..n)}: L:=[ seq( op(choose(S,i)),i=m1..m2)]: f:=GoodDT1(L,n): if nops(TT(f,n))<2^n then if n<7 then f:=BestNei(f,n,2): fi: fi: if nops(TT(f,n))<2^n then RETURN(FAIL,f): else RETURN(f): fi: end: GoodDTr:=proc(n,m1,m2) local L,i,S,f: S:={seq(i,i=1..n)}: L:=[ seq( op(choose(S,i)),i=m1..m2)]: L:=L[randperm(nops(L))]: f:=GoodDT1(L,n): if nops(TT(f,n))<2^n then RETURN(FAIL,f): else RETURN(f): fi: end: #########################ALMOST EXACT DISTINCT TAUTOLOGIES #does C conflict with all clauses in f? Exact1:=proc(f,C) local i,C1,ok: for C1 in f do ok:=false: if nops(C1) <= nops(C) then for i in C1 do if member(-i,C) then ok:=true: break: fi: od: else for i in C do if member(-i,C1) then ok:=true: break: fi: od: fi: if not ok then return false: fi: od: true: end: Exact:=proc(f) local i: for i from 2 to nops(f) do if not Exact1(f[1..i-1],f[i]) then return false: fi: od: true: end: BestSignE:=proc(f,n,C) local k,sgns,champ,score,bestScore,s,C1,i: k:=nops(C): sgns:=Veck(k): if not Exact1(f,C) then champ:=FAIL: else champ:=C: bestScore:=nops(TT({C} union f,n)): fi: for s in sgns do C1:={seq(s[i]*C[i],i=1..k)}: if not Exact1(f,C1) then next: fi: score:=nops(TT({C1} union f,n)): if champ=FAIL or score > bestScore then bestScore:=score: champ:=C1: fi: od: champ: end: FindExact:=proc(L,n) local f,C,C1: f:={}: for C in L do C1:=BestSignE(f,n,C): if C1<>FAIL then f:=f union {C1}: fi: od: f: end: #########################CLEVER DENSITY BOUNDS PartitionG:=proc(G) option remember: local P1,N,s: if nops(G)=1 then return {{1}}: fi: N:=nops(G): P1:=PartitionG(G[1..N-1]): for s in P1 do if G[N] intersect s = {} then return(P1 minus {s} union {s union {N}}): fi: od: P1 union {{N}}: end: PGbound:=proc(P,G) local i,s,S: S:=PartitionG(G): add(1-mul(1-P[i], i in s), s in S): end: DensityBound1:=proc(S) PGbound(DNFtoPG(S)): end: #########################GENERALIZING TO BOXES CD:=proc(C,B) local c: mul(1/B[c[1]],c in C): end: TT1B:=proc(C,B) local V,c,n,S,s,j: option remember: if nops(B)=0 then if C={} then return {[]}: else return {}: fi: fi: V:={seq(c[1],c in C)}: if nops(V)<>nops(C) then return {}: fi: n:=nops(B): if member(n,V) then for c in C while c[1]<>n do od: S:=TT1B(C minus {c},B[1..n-1]): return {seq([op(s),c[2]],s in S)}: else S:=TT1B(C minus {c},B[1..n-1]): return {seq(seq([op(s),j],s in S),j=1..B[n])}: fi: end: TTB:=proc(f,B) local C: {seq(op(TT1B(C,B)),C in f)}: end: #all clauses on box B and variables V VC:=proc(V,B) local S,v1,j,s: option remember: if V={} then return {{}}: fi: v1:=V[1]: S:=VC(V minus {v1},B): {seq(seq({op(s),[v1,j]},s in S),j=1..B[v1])}: end: #optimal clause with var set V to be added to f BestClause:=proc(f,B,V) local Tf,S,C,Cw,Nw,N: S:=VC(V,B): Nw:=-1: Tf:=TTB(f,B): for C in S do N:=nops(Tf union TT1B(C,B)): if N>Nw then Cw:=C: Nw:=N: fi: od: Cw: end: GoodDT1B:=proc(L,B) local N,i,f: N:=mul(B[i],i=1..nops(B)): f:={{seq([i,1],i in L[1])}}: for i from 2 to nops(L) while nops(TTB(f,B))Nw then Cw:=C: Nw:=N: Tcw:=Tc: fi: od: f:=f union {Cw}: Tf:=Tf union Tcw: od: f: end: GoodDTB:=proc(B,m1,m2) local L,i,S,f: S:={seq(i,i=1..nops(B))}: L:=[ seq( op(choose(S,i)),i=m1..m2)]: f:=GoodDT1B(L,B): if nops(TTB(f,B))FAIL then print(`Here is such a distinct DNF tautology with`, n, `variales, each of size`, m): print(NiceDNF(gu,X,NotX)): else gu:=gu[2]: print(`We were only able to cover`, nops(TT(gu,n)), `truth-vectors out of the total of`, 2^n, `here is such an almost-tautology that is distinct`): print(NiceDNF(gu,X,NotX)): fi: od: print(``): print(`------------------------------------------`): print(`This ends this article, that took`, time()-t0, `seconds to generate. `): end: #Paper2(N): inputs a positive integer and outputs an article listing Distinct DNF taugologies, optimal in some sense #for a number of variables from n=2 to n=N. Try: #Paper2(6); Paper2:=proc(N) local gu,n,X,NotX,t0,m: t0:=time(): print(`Distinct DNF Tautologies with as large as possible monomials`): print(``): print(`By Shalosh B. Ekhad`): print(``): for n from 2 to N do m:=An(n): print(``): print(`-----------------------------------------------`): print(``): print(`The largest minimial size of monomials in DNF tautologies with`,n, ` variables, all of whose terms`): print(` are least that size,that is feasible (on density grounds is)`, m): gu:=GoodDT(n,m,n): if gu[1]<>FAIL then print(`Here is such a distinct DNF tautology with`, n, `variales, with all the terms of size >=`, m): print(NiceDNF(gu,X,NotX)): else gu:=gu[2]: print(`We were only able to cover`, nops(TT(gu,n)), `truth-vectors out of the total of`, 2^n, `here is such an almost-tautology that is distinct`): print(NiceDNF(gu,X,NotX)): fi: od: print(``): print(`------------------------------------------`): print(`This ends this article, that took`, time()-t0, `seconds to generate. `): end: #NiceGDNF(S,z): inputs a generalized DNF (from a box) and outputs it in nice notation as a polynomial, where #z[i1]^j1*z[i2]^j2... represents the subcube {x_i1=j1, x_i2=j2, ...}. Try #NiceGDNF({[1,2],x); NiceGDNF:=proc(S,z) local s1,s: add(mul(z[s1[1]]^s1[2],s1 in s), s in S): end: #VeryGoodDTB(B,W): inputs a list of integers B representing the dimensions of a box #and a set of subsets of {1, ..., nops(B)} tries to find a covering by sub-boxes with distinct supports #not using W. Try: #VeryGoodDTB([2,3,5,7,11],{{2}}): VeryGoodDTB:=proc(B,W) local L,i,S,f,L1: S:={seq(i,i=1..nops(B))}: L:=[ seq( op(choose(S,i)),i=1..nops(B))]: L1:=[]: for i from 1 to nops(L) do if not member(L[i],W) then L1:=[op(L1),L[i]]: fi: od: L:=L1: f:=GoodDT1B(L,B): if nops(TTB(f,B))