# # Maple code for alternation-trading proofs of SAT time-space lower bounds # (c) Ryan Williams 2010 # with(simplex): with(Optimization): with(StringTools): # # # printproof: takes the output of an LP solver and the number of proof steps # and prints a readable proof # printproof := proc(varis,k) local A, aa, curra, i, j, y, L::List, item, str, star; # process the set of equalities A := Matrix(k,k): curra := Vector(k): for i from 1 to k do for j from 1 to k do curra[j] := cat("a",i,"_",j," "); od; for item in varis[2] do str := convert(item,string); if searchtext("a0_1 ",str) > 0 then y := FirstFromLeft("=",str); aa := convert(parse(substring(str,(y+1)..length(str))), float); fi: for j from 1 to k do if searchtext(curra[j],str) > 0 then y := FirstFromLeft("=",str); A[i,j] := convert(parse(substring(str,(y+1)..length(str))), float); fi: od: od: od: printf("0 %s\n",cat("DTS[n^",convert(aa,string),"]")); for i from 1 to k do L:=[]; star:=0; for j from k to 2 by -1 do if A[i,j] > 0.00001 then L := [[A[i,j],1,(-1)^(star)], op(L)]; star:=star+1; #lprint(i,j,A[i,j]); fi; od: L := [[A[i,1],1,0], op(L)]; printf("%d %s\n",i,translate(L)); od: return 0; end proc; # # translate: take a list of triples and output a string representing # the corresponding complexity class # translate := proc(L) local x, expr1, ex1, str; if (L = []) then str := ""; else x := L[1]; # compute a string corresponding to the runtime of the class ex1 := n^(x[1]); expr1 := convert(ex1,string); # remove the first tuple on the list str:= translate(subsop(1=NULL, L)); # print the class according to cases if (x[3] = 1) then str := cat(str,"(E ",expr1,")"); elif (x[3] = -1) then str := cat(str,"(A ",expr1,")"); else str := cat(str,"DTS[",expr1,"]"); fi; fi; return str; end proc; # # proofproduce: takes a proof annotation as input, and outputs # a readable proof, if one is possible. # proofproduce := proc(g) local S, varis; S:=list2LP(g,nops(g)): try varis := LPSolve(0,S): printproof(varis,nops(g)); print(g); catch: end try; end proc; # # tryall : try all proofs of a given number of lines for a given exponent. # in particular, generate strings of well-balanced parentheses and # convert to proofs # procedure for generating strings of well-balanced parentheses taken # from Knuth Vol 4, Pre-Fascicle 4a, p.3, which was taken from I. Semba # IPL 12, 188-192, 1981 # tryall := proc(li, low) local a, toggle, i, j, k, g, n, m, st, best; st := time(); if ((li mod 2)=0) then print("odd only"); return false; fi; a := array(0..li); #initialize n := (li-1)/2; if (n <=1) then binarysearch2([1,0,0],low); return true; fi; for k from 1 to n do a[2*k-1] := 1; a[2*k] := 0; od; a[0] := 0; j := 1; toggle := false; while (j <> 0) do if not(toggle) then a[j] := 1; m := 2*n - 1; else toggle := false; fi; #try current annotation g := []; for k from 1 to 2*n do g := [op(g),a[k]]; od; g := [op(g),0]; #print(j); print(g); binarysearch2(g,low); a[m] := 0; if (a[m-1] = 0) then toggle := true; a[m-1] := 1; m := m - 1; else j := m - 1; k := 2*n - 1; while (a[j] = 1) do a[j] := 0; a[k] := 1; j := j-1; k := k-2; od; fi; od: print(time()-st); end proc; # # # # listcheck: takes a list of bits and checks if it is a valid annotation # (discards those with more than six consecutive zeros) # # listcheck := proc(L::list) local sum1, sum0, i, bla, Size; Size := nops(L); # a legitimate sequence must begin with a speedup and end with a slowdown. if (L[1] <> 1 or L[Size-1] <> 0 or L[Size] <> 0) then return false; fi; sum1 := 1; sum0 := 0; zeros := 0; for i from 2 to Size-1 do if L[i] = 1 then sum1 := sum1 + 1; zeros:=0; else sum0 := sum0 + 1; zeros := zeros+1; fi; # a legitimate sequence never has more slowdowns than speedups at any point within it # also, rule out sequences with more than six consecutive 0's if (sum0 > sum1) or (zeros > 6) then return false; fi; od; # and it has an equal number prior to the last slowdown. if (sum1 = sum0) then return true else return false; fi; end proc; # # # list2LPc: takes a list and a prospective LB exponent # generates an LP for it (in sparse format, as a set of inequalities) # # list2LPc := proc(L::list,cc::float) local S, maxalts, count, i, j, k; k := nops(L); # analyze the list to see the maximum number of alternations used, then add one. maxalts := 2; count := 2; for i from 2 to k-1 do if L[i] = 1 then count := count + 1; if count > maxalts then maxalts := count; fi; else count := count - 1; fi; od; maxalts := maxalts + 1; # first add the constraints for the 0th step (initial stuff) # the first is very important (it establishes the contradiction). S := {a0_1 >= cat(`a`,k,_,1), b0_1 = 1}: # also add the constraints for the 1st step (it's a bit different from the others) S := S union {a1_1 >= 1, a1_1 = a0_1 - x1, b1_1 = b0_1, a1_2 = 1, b1_2 >= x1, b1_2 >= b0_1, a1_3 = x1, b1_3 = b0_1}: for j from 2 to maxalts do S := S union {cat(`a`,0,_,j) = 0, cat(`b`,0,_,j) = 0}: if j >= 4 then S := S union {cat(`a`,1,_,j) = 0, cat(`b`,1,_,j) = 0}; fi; od: # now add constraints for each step in turn. for i from 2 to k do if (L[i] = 1) then # # speedup constraints # S := S union {cat(`a`,i,_,1) >= 0.001, cat(`a`,i,_,1) >= cat(`a`,i-1,_,1) - cat(`x`,i), cat(`b`,i,_,1) >= cat(`b`,i-1,_,1), cat(`a`,i,_,2) = 0.001, cat(`b`,i,_,2) >= cat(`x`,i), cat(`b`,i,_,2) >= cat(`b`,i-1,_,1), cat(`a`,i,_,3) >= cat(`a`,i-1,_,2), cat(`a`,i,_,3) >= cat(`x`,i), cat(`b`,i,_,3) = cat(`b`,i-1,_,2)}; # also: the input to the "middle" quant is at least the runtime of the first quant # b2 (E n^a2) b1 DTS[n^a1] is in # b3=b2 (E n^a2) b1 (E n^x) b2=max{x,b1} (A log n) b1=max{b1,1} DTS[n^{a1-x}]... # the claim is that b2 is at least x and b1, but not necessarily >= a3. # it doesn't really seem to matter, though. S := S union {cat(`b`,i,_,2) >= cat(`a`,i,_,3)}; for j from 4 to maxalts do S := S union {cat(`a`,i,_,j) = cat(`a`,i-1,_,j-1), cat(`b`,i,_,j) = cat(`b`,i-1,_,j-1)}: od: else # L[i] = 0, i.e. slowdown constraints # the last quantifier block is definitely zeros. S := S union {cat(`a`,i,_,maxalts) = 0, cat(`b`,i,_,maxalts) = 0}; # shift all quantifiers 'over' by one for j from 2 to maxalts-1 do S := S union {cat(`a`,i,_,j) = cat(`a`,i-1,_,j+1), cat(`b`,i,_,j) = cat(`b`,i-1,_,j+1)}: od: # S := S union {cat(`a`,i,_,1) >= eval(cc)*cat(`a`,i-1,_,1), cat(`a`,i,_,1) >= eval(cc)*cat(`a`,i-1,_,2), cat(`a`,i,_,1) >= eval(cc)*cat(`b`,i-1,_,2), cat(`a`,i,_,1) >= eval(cc)*cat(`b`,i-1,_,1), cat(`b`,i,_,1) = cat(`b`,i-1,_,2)}; fi; od; end proc; # # # binarysearch: given an annotation and lower bound exponent # search for a good proof! # binarysearch2 := proc(L,ce,verbosity) local low, i, high, errors, S, T, cc; low:= ce: high := 1.804; try S := list2LPc(L,low): T := LPSolve(a0_1,S): printf("Trying %a\n", L); for i from 1 to 6 do if (high <= low) then break; fi; cc := (low + high)/2; try S := list2LPc(L,cc): T:=LPSolve(a0_1,S); low := cc; cc := (low + high)/2; catch: high := cc; cc := (low + high)/2; end try; od; if (verbosity=1) then printproof(T,nops(L)); fi; print(low,high); return low; catch: return 0; end try; end proc; # # heuristic search: given an annotation, lower bound exponent, and verbosity in {0,1}, # start a local search for better lower bound proofs # # (if verbosity = 1 then print the proofs when found) # maxlength := 70; heuristicsearch := proc(L, low, verbosity) local hd, hdcount, Qcount, i, j, k, k2, a1, a2, a3, a4, a5, b5, k3, b1, b2, b3, b4, i2, L2, oldL2, theQ, newc, best, cleartabu, tabu, item, minlength, addedtoQ; # make a queue with L in it. # repeat while the queue is nonempty: # take the head of the queue off. Call it L. # Over all possible ways to insert at most five bits in L, # Check if L' is a valid list, # if so check if it gets at least low, # if so, add L' to the end of the queue. Print L'. # end repeat. best := Vector(maxlength); newc := Vector(maxlength); for i from 1 to maxlength do best[i] := low; od; #don't check what's already on the list tabu := {op(L)}; #prune the list of duplicates, make that the queue theQ := [op(tabu)]; while (nops(theQ) > 0) do hd := theQ[1]; addedtoQ := false; hdcount := nops(hd); Qcount := nops(theQ); theQ := theQ[2..nops(theQ)]; #print("hd=",hd,"theQ=", theQ); for i from 1 to hdcount-1 do # insert a 1 in the position after i. for j from i to hdcount-1 do for k from j to hdcount-1 do for k2 from k to hdcount-1 do for b1 from 0 to 2 do for b2 from 0 to 2 do for b3 from 0 to 2 do for b4 from 0 to 2 do if (b1 = 2) then a1 := NULL else a1 := b1; fi; if (b2 = 2) then a2 := NULL else a2 := b2; fi; if (b3 = 2) then a3 := NULL else a3 := b3; fi; if (b4 = 2) then a4 := NULL else a4 := b4; fi; oldL2 := [op(hd[1..i]), a1, op(hd[i+1..j]), a2, op(hd[j+1..k]), a3, op(hd[k+1..k2]), a4, op(hd[k2+1..hdcount])]; if ((listcheck(oldL2)) and not(member(oldL2,tabu))) then L2 := oldL2; #print(trying, L2); newc[nops(L2)] := binarysearch2(L2, best[nops(L2)]-.03,verbosity); #print(newc,best); if (newc[nops(L2)] >= best[nops(L2)]) then for i2 from nops(L2) to maxlength do best[i2] := newc[nops(L2)]; od; theQ := [op(theQ), L2]; addedtoQ := true; elif (newc[nops(L2)] >= best[nops(L2)]-.03) then theQ := [op(theQ), L2]; addedtoQ := true; fi; tabu := tabu union {L2}; fi; od; od; od; od; od; od; od; od; if addedtoQ then printf("Current queue of annotations = %a\n", theQ) else printf("Searching next on queue...\n"); fi; # keep the size of the tabu list as small as possible # if the list just removed from the queue was smaller than all the others on the queue, # then clear the tabu list of small lists. #cleartabu := true; #for item in theQ do if nops(item) <= hdcount then cleartabu := false; fi; od; #if (cleartabu) then # remove anything on the tabu list of length at most hdcount. # for item in tabu do if nops(item) < hdcount then tabu := tabu minus {item}; fi; od; #fi; od; end proc;