#SAT.txt
#SAT solver using inclusion-exclusion; distinct tautologies
#Anthony Zaleski, 2017

print(`sat.txt:`):
print(`SAT algorithms using inclusion-exclusion`):
print(`By Anthony Zaleski, Spring 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(`sat.txt contains the following procedures.`):
	print(`Type Help(<procedure name>); for help on a specific procedure.`):
	print(`Taut, MapleTaut`):
	print(`MetaTaut, MetaMapleTaut, HowManyFinished`):
	print(`RandNF `):
	print(`DNFtoPG, LLL, LLLs, MetaLLL, MetaLLLs `):
	print(`RandDT,Anm,FindDT`):
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]=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);`):
else
	print(`No such procedure exists.`):
fi:
end:


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:



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:
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:
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=&not 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,s1,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:
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,t1,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 p<p0 then return Nlist,plist:
	else Nlist:=[op(Nlist),N]: plist:=[op(plist),p]: fi:
od:
end:

############
#DISTINCT TAUTOLOGIES


RandDT:=proc(n,m1,m2) local S,S1,ra,s,s1,ss,k:
S:={}:
S1:=`union`(seq(choose({seq(i,i=1..n)},k),k=m1..m2)): 
ra:=rand(0..1):
for s in S1  do
	ss:={}:
	for s1 in s do
		ss:=ss union {s1*(ra()*2-1)}:
	od:
	S:=S union {ss}:
od:
S:
end:


Anm:=proc(n,m)
add(binomial(n,k)/2^k,k=m..n):
end:


FindDT:=proc(n,m1,m2,K) local k,S:
for k from 1 to K do
	S:=RandDT(n,m1,m2):
	if MapleTaut(S) then return S: fi:
od:
FAIL:
end: