#C20.txt: 4/4/16 The BIG ONE: P vs. NOP, SAT
Help:=proc(): print(` RC(x,n,r) , RCNF(x,n,r,K), SAT(F,x,n) , OurSimp(F) , SAT1(F) `): 
print(` RD(x,y,n,r) `):
end:

with(Logic):

#Import(F,form=boolean):

#RC(x,n,r): inputs a letter x, a pos. integer n, and another positive
#integer r<n and outputs a random OR clause in x[1], ..., x[n]
RC:=proc(x,n,r) local S,i,ra1,ra2,s,C:

 if r>n then
    print(`Stupid, you can't make a party with 6 people if you only have 5 friends`):
     RETURN(FAIL):
 fi:

ra1:=rand(1..n):

ra2:=rand(0..1):

S:={}:

while nops(S)<r do
  S:=S union {ra1()}:
od:
 
S:

C:=false:

for s in S do
 if ra2()=1 then
   C:=C or x[s]:
   else
    C:= C or (not x[s]) :
 fi:
od:

C:

end:

#RCNF(x,n,r,K): inputs the same as RC(x,n,r) and a pos. integer K
#outpouts a random (r-CNF) with (<=K) clauses
RCNF:=proc(x,n,r,K) local F,i:
 
F:=true:

for i from 1 to K do
  F:=  F and RC(x,n,r):
od:

F:
end:

#SAT(F,x,n): inputs a Boolean formula and outputs true iff it is satistiable
#(in other words there exist at least ONE assigment of {true,false}^n to
#x[1], ..., x[n] that makes it true 
SAT:=proc(F,x,n)

if n=1 then
 if subs(x[1]=true,F) or subs(x[1]=false,F) then
   RETURN(true):
 else
  RETURN(false):
 fi:
fi:

   evalb(SAT(subs(x[n]=true,F),x,n-1) or SAT(subs(x[n]=false,F),x,n-1)): 

  end:

#OurSimp(F): simplifies a Boolean formula
OurSimp:=proc(F)
Logic[BooleanSimplify](Import(F,form=boolean)):
end:

SAT1:=proc(F)

if OurSimp(F)=false then
  false:
else
 true:
fi:

end:



#RD(x,y,n,r): inputs letters x and y, a pos. integer n, and another positive
#integer r<n and outputs a random AND clause in x[1], ..., x[n]
#y[1], ..., y[n],where y[i] is not x[i] and=* and or=+
RD:=proc(x,y,n,r) local S,i,ra1,ra2,s,C:

 if r>n then
    print(`Stupid, you can't make a party with 6 people if you only have 5 friends`):
     RETURN(FAIL):
 fi:

ra1:=rand(1..n):

ra2:=rand(0..1):

S:={}:

while nops(S)<r do
  S:=S union {ra1()}:
od:
 
S:

C:=1:

for s in S do
 if ra2()=1 then
   C:=C*x[s]:
   else
    C:= C*y[s] :
 fi:
od:

C:

end: