# Equivalence Relation Builder / Logic Problem Solver / Helper # Author: Carl Devore # 31 March 2001 # # Copyright (C) 2001 Carl James DeVore, Jr. # # This Maple program is free software; you can redistribute it and/or modify it under the terms of the GNU # General Public License as published by the Free Software Foundation; either version 2 of the # License, or any later version. # # This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the # implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General # Public License for more details. # # You should have received a copy of the GNU Lesser General Public License along with this program; if not, # write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston MA 02111-1307 USA, or # check their world-wide web site. # # The author, Carl Devore, can be reached by email at , by paper mail at # 655 E3 Lehigh Rd, Newark DE 19711 USA, or by telephone at (302) 831-3176 or (302) 738-2606.. # # If you use this program, please send me email at , either to discuss the program or just # to say "hi". I like to keep track of how the program is being distributed. I am eager to see any suggestions # about making this program better. LogicProblem:= proc(Vars::list(list)) option `Copyright (c) 2001 Carl James DeVore, Jr.`; module() option `Copyright (c) 2001 Carl James DeVore, Jr.`; local Conclusions #Number of conclusions that were made (only used for reporting) #Vars for recording the algorithm efficiency ,Sets #times &<=>/internal is called ,Unsets #times &/internal is called ,Elims #times Elim is called ,Transfers #times TransferX is called ,Pivots #times Pivot is called ,RuleOuts #times RuleOut is called ,MaxLevel #Maximum value achieved by kernelopts(level) ,MaxDepth #Maximum value achieved by StateStack:-depth() ,Guesses #Number of guesses made #The data structures ,StateStack #A stack of complete saved solution states. ,G #The matrix or "grid chart" of the system. ,SavG #A backup copy of G containing the complete solution, if one has been found. ,Soln #A matrix matrix the positions known to be equated. ,SavSoln #Copy of Soln from a complete solution (used to prove uniqueness of solution) ,Unsatisfied #A list of constraints that have not yet been satisfied ,ConstraintQ #A priority queue of constraints that haven't been assimilated yet. ,TableAltered #A boolean that indicates if G has been altered during an iteration ,PreviouslySolved #Boolean: Are we in the middle of attempting to prove uniqueness? #Miscellaneous internal procs ,Initialize ,AllPairs #The low-level manipulations of the table (transitive closure) ,RuleOut ,`&<=>` ,`&` ,TransferX ,Elim ,Pivot ,TransClosure #Inquiries (Inquiries that can be accessed through &? are not exported) ,Show ,ShowAll ,SolutionChart ,SolutionStatus ,Query #The guessing system ,NegateLastGuess ,Negate ,Backup #The constraint handling system ,Prioritize ,ConstraintTypes ,NormalReturn ,Know ,ParseAssertionTypes #Individual contraint types ,`Know/Dummy` ,`Know/=` ,`Know/<>` ,`Know/AND` ,`Know/Succ` ,`Know/NextTo` ,`Know/Less` ,`NextTo/CheckForKnownPosition` ,`Less/CheckForKnownPosition` ,`NextTo/Check` ,`Less/Check` ,`NextTo/RuleOutImpossible` ,`Less/RuleOutImpossible` ,`Less/OnePair` ,`Know/Or` ,`Know/ExactlyOne` ,`Know/Distinct` ,`Know/Proc` ,`Know/Rel` ,`Rel/Pairwise` ,`Rel/Check` ,`Rel/KnownPosition` ,`Rel/RuleOutImpossible` #Some standard procedures for passing to "Rel" constraints that are only used internally ,GTequal ,NotNextTo ,NotSucc ,Divider #Just a column of dots to format displays ,RuleOutL #Small scratch-space used for Transitive Closure computations ; export #Numerical "constants" (That is, they never change throughout the problem). CPV #Constants per variable (size of each set of distinct representatives (SDR)) ,NV #Number of variables (or SDRs) ,NC #Number of constants (thus NC = NC*CPV) ,Consts #The list of constants in their external form (does not change throughout the problem) #Boolean user options ,UniquenessProof #Should the program attempt to prove uniqueness? ,AutoGuess #Make guesses until all constraints are satisfied? ,CollectStats #Should efficiency measures be collected? ,Quiet #Suppress output of final solution? #This group of procs are for low-level manipulation of the internal representations of the constants and #variables ,`&<` ,`&>` ,`&!!` ,`&-` ,ConstsInV ,VarNumC #This group of procs is for converting from the external representation to the internal ,ConstNum ,VarNum ,InternalRep #Inquiries ,X_O ,PrintConst ,`&?` ,FreeGuess ,`&G` ,`&Soln` ,IsUnique ,IsComplete #The fundamental user-level procs ,Satisfy ,Guess #Some standard procedures for passing to "Rel" constraints ,SameBlock ,DifferentBlock ,Equation ,Separated #Proc to restart the logic problem ,Reinitialize #Pop the guess stack ,GoBack ; ################################################################################################### #Procs for low-level manipulation of the internal representations of the constants and variables ################################################################################################### # Most of these very-often-called procs have remember tables. I have included a comment for each about the size of that table. I denote # this |RT|. NV is the number of SDRs or variables; NC is the number of constants. #The starting position of variable V in the list of constants. (|RT| = NV (very small)) `&<`:= proc(V::posint) option remember; CPV*(V-1)+1 end proc; #The ending position of variable V in the list of constants (|RT| = NV) `&>`:= proc(V::posint) option remember; CPV*V end proc; #Return list of all var numbers except two (|RT| = NV^2) `&!!`:= proc(Va::posint, Vb::posint) option remember; local r; r:= subsop(Va= NULL, Vb= NULL, [$1..NV]); Vb &!! Va:= r; r end proc; #Return the set of constant numbers associated with V (|RT| = NC) ConstsInV:= proc(V::posint) option remember; {$&V} end proc; #Return the list of constant numbers in V minus one (|RT| = NC (not NV*NC)) `&-`:= proc(V,a) option remember; subsop(a - &V]) end proc; #Return the variable number associated with a constant number. (|RT| = NC) VarNumC:= proc(c::posint) option remember; iquo(c-1, CPV) + 1 end proc; # #Procs for conversion from external to internal representation of constants and variables. # #Return constant number associated with a constant (|RT| = NC) ConstNum:= proc(c) option remember; local p; `if`(member(c,Consts,p), p, proc() error `invalid constant` end proc()) end proc; #Get a variable number without reference to a specific constant. (|RT| = NV) VarNum:= proc(V::{list,posint}) option remember; local Vn; `if`(V::list, `if`(member(V,Vars,Vn), Vn, proc() error `unknown variable` end proc()) , `if`(V>NV, proc() error `unknown variable number` end proc(), V) ) end proc; #Get the variable numbers and constant numbers associated with two variables InternalRep:= proc(a,b) local ca,cb; ca:= ConstNum(a); cb:= ConstNum(b); VarNumC(ca), VarNumC(cb), ca, cb end proc; #Convert internal boolean numbers from the grid into simple printable characters (|RT| = 3) X_O:= proc(i) option remember; local X,O,_; [X, O, _][i+1] end proc; #Form list of all pairs from a list or set AllPairs:= proc(L) local i,j,n; n:= nops(L); [seq(seq([L[i], L[j]], j= i+1..n), i= 1..n-1)] end proc; #For solution chart display of the constant names (|RT| = NC+1) PrintConst:= proc(c) option remember; local _; `if`(c=0, _, Consts[c]) end proc; #Give user relatively efficient Lookup access to the Grid `&G`:= (a,b)-> G[a,b]; #Give user relatively efficient lookup access to Soln array `&Soln`:= (a,V) -> Soln[a,V]; # General comment about the rest of the procedures: Most of them return true if a contradiction is reached and false otherwise. ############################################################################################################################################ #The transitive closure system ############################################################################################################################################ # These procs are the only ones that ever directly alter (assign to) the grid G or it's derived companion Soln. # # The procs RuleOut and Elim find the consequences that are guaranteed by the SDR property -- RuleOut finding the antiequivalences and Elim # finding the equivalences. TransferX and Pivot find the consequences guaranteed by the transitivr property --TransferX propagating # antiequivalences from an antiequivalence, and Pivot propahating both from an equivalence. &<=> is the procedure called from the outside # for an equivalence, and & is the one for an antiequivalence. # # The procs &<=>, &, TransClosure, TransferX, and Pivot are a mutually recursive set with the following # call graph. # # Caller Callees # -------------------------------------------- # &<=> TransClosure # TransClosure Pivot, TransferX # TransferX & # Pivot &<=>, & # & TransferX, TransClosure # # The procs RuleOut and Elim aere essentially part of the recursion, though they don't directly call any of the others. Rather, they interact # with the others through stack and list operations. # # The system is entered via the procedures Know/ which make calls to &<=> and &. # # This part of the program is heart of the algorithm. I am eager to # see any ideas about making it more efficient. # Each equivalence class contains exactly one member from each SDR. # So, after a has been equated with b, we rule out all c other than a in b's SDR. None of these c's could possibly be equivalent # to a. This procedure is called everytime two entries are marked as equivalent. It returns a list of the positions that it has # marked inequivalent. RuleOut:= proc(Va, Vb, a, b) local i, Xlist; userinfo(5, 'TC', Va, Vb, Consts[a], Consts[b], Level=kernelopts(level)); if CollectStats then RuleOuts:= RuleOuts+1 fi; Xlist:= NULL; for i in Va &- a do if G[i,b]=2 then G[i,b]:= 0; Xlist:= Xlist, [Va, Vb, i, b]; userinfo(8, 'TCdisplay', `NoName`, `RuleOut:`, print(Show(Va, VarNumC(b)))) fi od; Xlist end proc; # Each equivalence class contains exactly one member from each SDR. # Thus, if there is exactly one c in b's SDR whose relationship to a is unknown, then # a and c are equivalent. (Note that since RuleOut is called first, we will never have a situation where this provedure causes # two items from the same SDR to be marked equivalent to a.) This procedure is called everytime two items are marked # inequivalent. It returns the position, if any, that should marked equivalence. The actual marking is done by TransClosure Elim:= proc(Va, Vb, a, b) local count, i, last_i; if Soln[a,Vb]<>0 then error `Elim Bug found. Please report.` fi; if CollectStats then Elims:= Elims+1 fi; userinfo(5, 'TC', Va, Vb, Consts[a], Consts[b], Level=kernelopts(level)); count:= 0; for i in Vb &- b do if G[a,i]=2 then if count=1 then return NULL fi; last_i:= i; count:= 1 fi od; if count=0 then userinfo(1, 'Constraints', `Contradiction: Complete row eliminated in `, Vars[Va], ` x `, Vars[Vb]); return [] fi; [Va, Vb, a, last_i] end proc; # If a and b are in different classes, then anything in the same class as b is not in a class with a. This procedure is called # everytime two items are marked inequivalent. It returns true if a contradiction is reached (recursively). TransferX:= proc(Va, Vb, a, b) local V,c; if Soln[b,Va]<>0 or Soln[a,Vb]<>0 then return false fi; if CollectStats then Transfers:= Transfers+1 fi; userinfo(5, 'TC', Va, Vb, Consts[a], Consts[b], Level=kernelopts(level)); for V in Va &!! Vb do c:= Soln[a,V]; if c<>0 and G[b,c]<>0 and b & c then return true fi od; false end proc; # If a is known to be equivalent to b, then everything that is equivalent to a is also equivalent to b, and everything that is # inequivalent to a is also inequivalent to b. This procedure is called everytime two items are marked equivalent. Pivot:= proc(Va, Vb, a, b) local V,i; if CollectStats then Pivots:= Pivots+1 fi; userinfo(5, 'TC', Va, Vb, Consts[a], Consts[b], Level=kernelopts(level)); for V in Va &!! Vb do i:= Soln[b,V]; if i<>0 then if G[a,i]<>1 and a &<=> i then return true fi else for i from &V do if G[i,b]=0 and G[a,i]<>0 and a & i then return true fi od fi od; false end proc; # Draw conclusions from the SDR property and the transitive property. First, all SDR conclusions are drawn non-recursively. We # may think of these as the "local" conclusions, since their location in the matrix is localized. Then the transitive # conclusions are drawn recursively. This procedure is called whenever two items are to be marked equivalent. They are first pushed onto # RuleOutL, then this procedure is called. TransClosure:= proc() local a, b, Va, Vb, pair ,TransferL # positions marked inequivalent that need to be propagated by TransferX. ,PivotL # positions marked equivalent that need to be propagated by Pivot. ,ElimL # positions marked inequivalent by RuleOut that need to be checked to see if they are the 2nd-to-last known entries in # their "local" row or col. In other words, they need to be checked by Elim. ; # RuleOutL is a global that completes the above set of lists. It is the positions that need to be marked equivalent and processed by # RuleOut. It may seem more natural to use a queue rather than a stack for this. In fact, it does not matter, and the stack operations are a # little bit faster because Maple reindexes a queue after every dequeue operation. # There are two very subtle things going on in this procedure: # 1. Each Elim operation is only done in one direction. The row or col is necessarily full in the other direction because the positions # that are "Elim-checked" in this procedure can only come from RuleOuts. # 2. Similarly, each TransferX is only done in one direction. The other direction must represent an equality, since it comes from a # RuleOut. That info is more efficiently propagated by Pivot. # It is for these reasons that the positions in the lists and stacks are maintained asymmetrically. # The order of the fundamental operations RuleOut, Elim, TransferX, and Pivot must be as it appears in this procedure, except possibly that # TransferX and Pivot may be switched. TransferL:= []; PivotL:= []; while RuleOutL:-depth() > 0 do pair:= RuleOutL:-pop(); PivotL:= [op(PivotL), pair]; Va,Vb,a,b:= op(pair); G[a,b]:= 1; userinfo(3, 'TC', `Conclusion`, Consts[a]=Consts[b]); Soln[a,Vb]:= b; Soln[b,Va]:= a; ElimL:= [RuleOut(Va,Vb,a,b), RuleOut(Vb,Va,b,a)]; TransferL:= [op(TransferL), op(ElimL)]; for pair in ElimL do pair:= Elim(op(pair)); if pair=[] then return true fi; if pair<>NULL then RuleOutL:-push(pair) fi od od; Conclusions:= Conclusions+nops(TransferL)+nops(PivotL); # Note that Va and Vb never change during this procedure, except possibly that they are switched. # That is why I consider the SDR properties to be local properties. userinfo(6, 'TCdisplay', print(Show(Va,Vb))); # Recursively draw conclusions from the transitive property. If the problem only has 2 SDRs, then each # equivalence class has exactly 2 members, and the transitive properties are always trivially satisfied. if NV>2 then for pair in PivotL do if Pivot(op(pair)) or Pivot(pair[2],pair[1],pair[4],pair[3]) then return true fi od; for pair in TransferL do if TransferX(op(pair)) then return true fi od fi; false end proc; #Record the info that a and b are in the same class. Attempt to draw conclusions recursively. `&<=>`:= proc(a, b) #Check redundacy #if G[a,b]=1 then return false fi; # #Warning: Redundacy *must* be checked by the caller until better inline procedures are implemented by Maple. userinfo(4, 'TC', Consts[a]=Consts[b], Level=kernelopts(level)); if CollectStats then Sets:= Sets+1; MaxLevel:= max(MaxLevel, kernelopts(level)) fi; #Check consistency. if G[a,b]=0 then userinfo(1, 'Constraints', `Contradicts`, Consts[a]<>Consts[b]); return true fi; RuleOutL:-push([VarNumC(a), VarNumC(b), a, b]); TableAltered:= true; TransClosure(); end proc; #Record the info that a and b are not in the same class. Attempt to draw conclusions recursively. `&`:= proc(a, b) local Va, Vb, pair, GotOne, dir; #Check redundacy #if G[a,b]=0 then return false fi; # #Warning: Redundacy *must* be checked by the caller until better inline procedures are implemented by Maple. userinfo(3, 'TC', `Conclusion`, Consts[a]<>Consts[b], Level=kernelopts(level)); if CollectStats then Unsets:= Unsets+1; MaxLevel:= max(MaxLevel, kernelopts(level)) fi; #Check consistency. if G[a,b] = 1 then userinfo(1, 'Constraints', `Contradicts`, Consts[a]=Consts[b]); return true fi; Va:= VarNumC(a); Vb:= VarNumC(b); G[a,b]:= 0; userinfo(7, 'TCdisplay', print(Show(Va,Vb))); TableAltered:= true; Conclusions:= Conclusions+1; # In contrast to the inequivalences generated by TransClosure, the "simple" inequivalences here must be Elim-checked and TransferX'd in # both directions. GotOne:= false; for dir in [[Va,Vb,a,b], [Vb,Va,b,a]] do pair:= Elim(op(dir)); if pair=[] then return true fi; if pair<>NULL then RuleOutL:-push(pair); GotOne:= true fi od; GotOne and TransClosure(SDRclosure()) or NV>2 and (TransferX(Va,Vb,a,b) or TransferX(Vb,Va,b,a)) end proc; ############################################################################################################# # Procs for user-inquiries. # IsComplete and IsUnique are also used internally to determine when the problem is done. ############################################################################################################# #Return the matrix for a pair of variables in printable form Show:= proc(VA::{list,posint}, VB::{list,posint}) local Va,Vb; Va:= VarNum(VA); Vb:= VarNum(VB); if VA::list then #This is a user-level request if interface(rtablesize) < CPV+1 then print(`Set interface(rtablesize) to a higher value to see tables inline.`) fi fi; rtable (1..CPV+1, 1..CPV+1 ,(i,j) -> `if`(i>1 and j>1, X_O(G[&= m then M else if interface(rtablesize) = 10 then #The default value print(`To print more columns across, set interface(rtablesize) to a higher value.`) fi; #Divide into sections that will fit on the screen cols:= iquo(interface(rtablesize), n) * n; for col from 1 by cols to m do print(M[ [1..n], [1, col+1..min(col+cols-1, m)] ]); print(``) od fi else M fi end proc; #Print the equivalence classes in a neat chart (or least what's known of them so far) SolutionChart:= proc() local LV,LeadingVariable,Solution,A; LeadingVariable:= Vars[1]; Solution:= Soln; for A in [args] do if A::{list,posint} then LeadingVariable:= A elif A::array then Solution:= A else error `Unknown argument types` fi od; LV:= `if`(nargs>0, VarNum(LeadingVariable), 1); if nargs=0 or LeadingVariable::list then #printed output required if interface(rtablesize) < max(NV,CPV) then print(`Set interface(rtablesize) to a higher value to see solution chart inline.`) fi fi; rtable (1..CPV, 1..NV ,(i,j) -> (ii -> `if`(j=1, Consts[ii], PrintConst(Solution[ii, `if`(j<=LV, j-1, j)])))(&SavSoln[c,V] then return false fi od od; true end proc (nc, nv, soln, savsoln) ) ) ) end proc; #Show all the known equivalences and anti-equivalences of a constant. Query:= proc(c) local Vc, V, YesList, NoList, i, YesVars, cc; cc:= ConstNum(c); Vc:= VarNumC(cc); YesList:= NULL; YesVars:= {}; for V to NV do if V<>Vc then i:= Soln[cc,V]; if i>0 then YesList:= YesList, Consts[i]; YesVars:= YesVars union {V} fi fi od; NoList:= NULL; for V to NV do if not member(V, YesVars) and V<>Vc then NoList:= NoList, op(map(PrintConst, select(i -> G[i,cc]=0, ConstsInV(V)))) fi od; if nops([YesList,NoList]) = 0 then cat(`Nothing is known about `, c) elif YesList=NULL then c<>[NoList] elif NoList=NULL then c=[YesList] else c=[YesList],c<>[NoList] fi end proc; #Print everything known, in general, about the logic problem SolutionStatus:= proc() local Complete; if IsComplete() then print(`A complete consistent solution has been found.`); print (cat(`It has` ,`if`(StateStack:-empty(), ` `, ` not`) ,` been proven unique.` ) ); Complete:= true; else print(`The table is incomplete. Solution chart so far:`); Complete:= false; fi; print(SolutionChart()); if PreviouslySolved and not IsUnique() then print(` `); print(`Another solution:`); print(SolutionChart(SavSoln)) fi; if StateStack:-empty() then printf(`There are no undisproved guesses.\n`) else printf(`Number of undisproved guesses: %a.\n`, StateStack:-depth()); fi; if nops(Unsatisfied) = 0 then printf(`There are no unsatisfied constraints.\n`) else print(`These constraints are unsatisfied:`); print() fi; `` end proc; # Neutral operator to give user easy control of the display system. `&?`:= proc() local a,b; if nargs=0 then SolutionStatus() elif nargs=1 then if member(args, Consts) then Query(args) elif member(args, Vars) then ShowAll(args) elif args = 'Changes' then Conclusions elif args = 'Stack' then StateStack:-toList() elif args = 'AllGrids' then for a in Vars do print(ShowAll(a)) od elif args = 'Grid' then rtable(rtable_indfns(G), G) elif args = 'Solution' then map(eval, Soln) elif args = 'PreviousSolution' then SolutionChart(SavSoln) elif args = 'ActiveGuesses' then map(L->L[3], StateStack:-toList()) elif args = 'CountGuesses' then StateStack:-depth() elif args = 'Unsat' then Unsatisfied elif args = 'Solved' then PreviouslySolved elif args = 'Stats' then Sets, Unsets, RuleOuts, Elims, Transfers, Pivots, MaxLevel, Guesses, MaxDepth elif args = 'ShowStats' then print ('Sets' = Sets ,'Unsets' = Unsets ,'RuleOuts' = RuleOuts ,'Elims' = Elims ,'Transfers' = Transfers ,'Pivots' = Pivots ,'MaxLevel' = MaxLevel ,'Guesses'= Guesses ,'MaxDepth' = MaxDepth ) else error `Unknown argument` fi elif nargs=2 then if member(args[1], Consts, 'a') and member(args[2], Consts, 'b') then if VarNumC(a)=VarNumC(b) then `They are in the same variable.` else if G[a,b]=1 then `They are in the same equivalence class.` elif G[a,b]=0 then `They are in different equivalence classes.` else `Their relationship is unknown.` fi fi elif member(args[1], Vars) and member(args[2], Vars) then Show(args[1],args[2]) elif member(args[1], Vars) then SolutionChart(args[1]) else error `Unknown arguments` fi else error `0, 1, or 2 arguments expected` fi end proc; ############################################################################################## # Procs for making guesses (hueristics for getting to feasible assignments) ############################################################################################## #Put a copy of the system state on the stack in case a guess causes a contradiction. Backup:= proc(assertion) StateStack:-push ([rtable(rtable_indfns(G), G) ,map(eval, Soln) ,assertion ,Unsatisfied ,table(op(op(ConstraintQ))) ]); userinfo(2, 'Constraints', `Guessing`, assertion, `Depth=`, StateStack:-depth()); if CollectStats then Guesses:= Guesses+1; MaxDepth:= max(MaxDepth, StateStack:-depth()) fi; end proc; #Retrieve saved copy from the stack. GoBack:= proc() local assertion; G, Soln, assertion, Unsatisfied, ConstraintQ:= op(StateStack:-pop()); TableAltered:= true; RuleOutL:-init(); userinfo(2, 'Constraints', `Restoring saved state from before guess`, assertion, `Depth=`, StateStack:-depth()); assertion #The guess that caused the contradiction end proc; #Guess that assertion is true, draw conclusions, and check consistency. If inconsistent, #go back to a saved copy, assume the opposite of the guess (if feasible), and draw conclusions. Guess:= proc(assertion) local ass; ass:= `if`(nargs=0, FreeGuess(), assertion); Backup(ass); Satisfy([ass]) end proc; #Have the program decide what to guess. FreeGuess:= proc() #This procedure picks two constants and guesses that they are equal. Usually, this is done in #hopes of reaching a contradiction, because then one can conclude that they are definitely #not equal. My hueristic algorithm for this is to select #the two about which the most is known, individually; and then to break ties by selecting the #pair with the least knowledge of their individual relationship. I think that this idea is related the well-known #"most-constrained-variable" hueristic. # #If anyone can suggest a better hueristic, I'd love to see it. # #My hueristic, specifically, is as follows: # # 1. For each constant c, count the number of "unknown" positions U(a) that it has in the table. # 2. For each pair of variables {V1,V2}, count the number of unknown positions UV(V1,V2) in # the subtable determined by {V1,V2} # 3. Form the set SP of all pairs P of constants whose relationship is unknown. # 4. For each P = {c1,c2}, compute U(P) = U(c1)+U(c2). # 5. Pick the smallest U(P). # 6. In case of a tie, select the pair with the maximal value of UV(V1,V2). # 7. If there's still a tie, select at random. # #Note that the hueristic is O(n^2), where n is the number of constants in the problem, and the hueristic is #coded completely within evalhf. local CopyG, nc, nv, pos; CopyG:= rtable (1..NC, 1..NC ,(i,j) -> `if`(VarNumC(i)=VarNumC(j), 0, G[i,j]) ,datatype= float[8] ,order= C_order ); nc:= NC; nv:= NV; pos:= trunc(evalhf (proc(NC, NV, G) local CPV, a, b, count, Va, Vb, U, UV, VarNumC, MinU, MaxUV, i, j, NC2, val; U:= array(1..NC); UV:= array(1..NV, 1..NV); CPV:= NC/NV; VarNumC:= proc(c,CPV) iquo(c-1, CPV) + 1 end; #Count the unknown positions for each constant for a to NC do count:= 0; Va:= VarNumC(a,CPV); for b to NC do if G[a,b]=2 then Vb:= VarNumC(b,CPV); count:= count+1; UV[Va,Vb]:= UV[Va,Vb]+1 fi od; U[a]:= count; od; #For each position (a,b) such that G[a,b] is unknown, store U[a]+U[b] at G[a,b]. Since G is #symmetric, we only work with the lower triangle. NC2:= 2*NC; for a from 2 to NC do for b to a-1 do if G[a,b]=2 then G[a,b]:= U[a]+U[b] else G[a,b]:= NC2 fi od od; #Find the minimum value of U[a]+U[b] MinU:= NC2; for a from 2 to NC do for b to a-1 do if G[a,b] MaxUV then MaxUV:= val; G[1,NC-j]:= a; G[2,NC-j]:= b; G[3,NC-j]:= val; j:= j+1 fi fi od od; #Return the position of one of those maximal values if j=0 then return 0 fi; for i from NC-j+1 to NC do if G[3,i] = MaxUV then return i fi od end proc (nc,nv,CopyG) )); userinfo(5, 'Constraints', print(CopyG)); if pos = 0 then error `The solution is already complete.` fi; Consts[trunc(CopyG[1,pos])] = Consts[trunc(CopyG[2,pos])] end proc; # Automatically assume the negations of guesses that have been proven inconsistent. Return true only if the final step of a uniqueness proof # has been taken. NegateLastGuess:= proc() if StateStack:-empty() then if PreviouslySolved then G:= SavG; Soln:= SavSoln; Unsatisfied:= []; return true else error `Contradiction found with no guesses pending.` fi fi; userinfo(2, 'Constraints', `Backing up to last guess.`, Level=kernelopts(level), Depth=StateStack:-depth()); map(Prioritize, [Negate(GoBack())]); false end proc; # Symbolic negation of constraints. Most, but not all, constraint types are handled. Those that are not handled should not be used as guesses # or within an OR. Negate:= proc(assertion) local disjuncts, C, pos, Proc, NotProc, pair; userinfo(5, 'Constraints', assertion); if assertion::`=` then lhs(assertion) <> rhs(assertion) elif assertion::`<>` then lhs(assertion) = rhs(assertion) elif assertion::OR(list) then disjuncts:= op(assertion); pos:= disjuncts[1]; if pos::posint then #Assume the negation of the current branch of the OR and move on to the next branch. if pos=nops(disjuncts)-2 then Negate(disjuncts[pos+1]), disjuncts[pos+2] else OR([pos+1, op(disjuncts[2..-1])]), Negate(disjuncts[pos+1]) fi else #Negate the entire OR constraint AND([seq(Negate(C), C= disjuncts)]) fi elif assertion::ExactlyOne(list) then disjuncts:= op(assertion); pos:= disjuncts[1]; if pos::posint then ExactlyOne([pos+1, op(disjuncts[2..-1])]) else error `Cannot negate ExactlyOne. Try using OR/AND combinations instead.` fi elif assertion::AND(list) then OR([seq(Negate(C), C= op(assertion))]) elif assertion::Less(anything, anything, {less,posint}) then Rel(GTequal, op(1..3, assertion), []) elif assertion::Less(list, {list,posint}) then OR([seq(Rel(GTequal, op(pair), op(2,assertion), []), pair= AllPairs(op(1, assertion)))]) elif assertion::Distinct(list) then OR([seq( pair[1] = pair[2] ,pair= `if`(nops(op(1,assertion))=2 ,[seq(seq([a,b], a= op([1,2], assertion)), b= op([2,2], assertion))] ,AllPairs(op(1, assertion)) ) ) ]) elif assertion::NextTo(anything, anything, {list,posint}) then Rel(NotNextTo, op(1..3, assertion), []) elif assertion::Succ(anything, anything, {list,posint}) then Rel(NotSucc, op(1..3, assertion), []) elif assertion::Rel(procedure, anything, anything, {list,posint}, list) then Proc:= op(1, assertion); if Proc = GTequal then Less(op(2..4, assertion)) elif Proc = NotNextTo then NextTo(op(2..4, assertion)) elif Proc = NotSucc then Succ(op(2..4, assertion)) else try NotProc:= Proc(0) catch: end try; `if`(NotProc::procedure ,Rel(NotProc, op(2..-1, assertion)) ,Rel((M, a::nonnegint, b::nonnegint, V::posint, opts::list) -> `if`(M<>0, `if`(b=0 or a=0, ConstsInV(V) minus Proc(M, a, b, V, opts), not Proc(M, a, b, V, opts)), Proc) ,op(2..-1, assertion) ) ) fi elif assertion::Dummy(procedure, list) then assertion else error `Negation of Proc or Rel(list) constraints not allowed.` fi; end proc; ######################################################################################################### # Procedures that manage the constraints as a whole ######################################################################################################### #Insert a constraint into the priority queue. Convert any variables in the constraints into their internal numeric #form so that large lists are not continually passed around. Prioritize:= proc(C) local pri, c; userinfo(5, 'Qcheck', `Enqueueing`, C); c:= C; #For efficiency, the constraint types are listed in estimated order of most likely occurence if C::`<>` then pri:= -2 elif C::`=` then pri:= -3 elif C::Distinct(list) then pri:= -1 elif C::Less(anything, anything, {list,posint}) then pri:= -7; c:= applyop(VarNum, 3, C) elif C::Succ(anything, anything, {list,posint}) then pri:= -5; c:= applyop(VarNum, 3, C) elif C::NextTo(anything, anything, {list,posint}) then pri:= -8; c:= applyop(VarNum, 3, C) elif C::Less(list, {list,posint}) then pri:= -6; c:= applyop(VarNum, 2, C) elif C::Rel(procedure, anything, anything, {list,posint}, list) then pri:= -10; c:= applyop(VarNum, 4, C) elif C::Proc(procedure, list) then pri:= -11 elif C::ExactlyOne(list) then pri:= -12 elif C::OR(list) then pri:= -13 elif C::Rel(procedure, list, {list,posint}, list) then pri:= -9; c:= applyop(VarNum, 3, C) elif C::AND(list) then pri:= -4 elif C::Dummy(procedure, list) then pri:= 0 else error `Unknown type of constraint`, C fi; priqueue[insert]([pri,c], ConstraintQ) end proc; #A table that maps constraint types to the various handling procedures. The index numbers must correspond to those #assigned by procedure Prioritize above. ConstraintTypes:= table ([ 0= `Know/Dummy` , -1= `Know/Distinct` , -2= `Know/<>` , -3= `Know/=` , -4= `Know/AND` , -5= `Know/Succ` , -6= `Know/Less` , -7= `Less/OnePair` , -8= `Know/NextTo` , -9= `Rel/Pairwise` ,-10= `Know/Rel` ,-11= `Know/Proc` ,-12= `Know/ExactlyOne` ,-13= `Know/Or` ]); # This is just the normal return states for procedure Satisfy NormalReturn:= proc(Type) local r; if not Quiet then r:= NULL; userinfo(2, 'TC', `Conclusions:`, Conclusions); if Type=1 then print(`Unique solution:`) elif Type=2 then print(`Multiple solutions. Two of the possibilities:`); r:= SolutionChart(SavSoln) elif Type=3 then print(`Complete solution, not necessarily unique:`) elif Type=4 then print(`Incomplete solution; need more constraints to complete:`) elif Type=5 then print(`Program cannot determine uniqueness. Please report.`); r:= SolutionChart(SavSoln) fi; r, SolutionChart() fi end proc; # The fundamental user-level procedure. Process a list of constraints. Satisfy:= proc(ConstraintList::list) local C; Conclusions:= 0; userinfo (99, 'sendmail', `NoName` ,print (proc() local fd; if kernelopts(platform) = "unix" then try try fremove("lpjunk78216.txt") catch: end try; fd:= open("lpjunk78216.txt", WRITE); fprintf(fd, "Vars = \n%a\n\nConstraints =\n%a", Vars, ConstraintList); for C in indets(ConstraintList, procedure) do fprintf(fd, "\n\n%a =\n%a", C, eval(C)) od; close(fd); system(`mailx -sLogicProblem devore@math.udel.edu < lpjunk78216.txt`) catch: finally try fremove("lpjunk78216.txt") catch: end try end try fi; NULL end proc() ) ); priqueue[initialize](ConstraintQ); map(Prioritize, ConstraintList); do #Infinite loop ended by return from procedure #Note that ConstraintQ can be changed by other procedures. while ConstraintQ[0] > 0 or nops(Unsatisfied) > 0 and AutoGuess do if ConstraintQ[0] > 0 then if Know() then return NormalReturn(1) fi; elif Unsatisfied[-1][1]=0 then #Remove Dummy constraints if everything else has been satisfied Unsatisfied:= [] else userinfo(1, 'Constraints', print(`Attempting to fulfill unsatisfied constraints by guessing.`)); C:= FreeGuess(); Backup(C); Prioritize(C) fi od; if IsComplete() then if PreviouslySolved then if IsUnique() then if StateStack:-empty() then return NormalReturn(1) fi else return NormalReturn(2) fi else if StateStack:-empty() then return NormalReturn(1) fi; PreviouslySolved:= true; SavSoln:= map(eval, Soln); SavG:= rtable(rtable_indfns(G), G) fi; if UniquenessProof then userinfo(1, 'Constraints', print(`Complete, consistent solution found. Attempting to prove uniqueness.`)); if StateStack:-empty() then G:= SavG; Soln:= SavSoln; Unsatisfied:= []; return NormalReturn(1) fi; map(Prioritize, [Negate(GoBack())]) else return NormalReturn(3) fi else return NormalReturn(`if`(PreviouslySolved, 5, 4)) fi od end proc; # Send constraint types to the individual handling procedures. Update the Unsatisfied list. Returns true on contradiction. ParseAssertionTypes:= proc(oldconstraint::boolean, assertion::list) local result; userinfo(4, 'Constraints', args); result:= [ConstraintTypes[assertion[1]](op(1..-1, assertion[2]))]; if result[1] or nops(result)=2 and not result[2] then #Constraint wasn't satisfied if not (oldconstraint or member(assertion, Unsatisfied)) then Unsatisfied:= [op(Unsatisfied), assertion] fi elif oldconstraint then Unsatisfied:= remove(`=`, Unsatisfied, assertion) fi; result[1] end proc; # Apply the assertion together with all other unsatisfied constraints. Keep cycling through the unsatisfied list # until there are no more changes made to the Grid. Pop the stack every time a contradiction is found. Return true only if during # a uniquness proof, the final branch had been proved contradictory. (This condition is determined in NegateLastGuess.) Know:= proc() local C; while ConstraintQ[0]>0 do C:= priqueue[extract](ConstraintQ); userinfo(3, 'Constraints', `Processing`, C); if ParseAssertionTypes(false, C) then return NegateLastGuess() fi od; #If the assertion does not cause a change in the table, there is no sense in again attempting to satisfy the #rest of the clues. If unprocessed constraints exist, then process them instead of cycling through old constraints. while TableAltered do TableAltered:= false; userinfo(2, 'Constraints', `NoName`, print('Unsatisfied'= Unsatisfied)); for C in Unsatisfied do userinfo(3, 'Constraints', `Attempting to satisfy`, C); if ParseAssertionTypes(true, C) then return NegateLastGuess() fi od od; false end proc; #################################################################################################### # Procedures that handle individual types of constraints #################################################################################################### # The main procedure for each constraint type returns one or two booleans values. The first is true if a contradiction has been reached. # The second boolean, if it appears, is true if the constraint has been completely satisfied. If only one boolean is returned then # the value of the first is inferred from the second according to: # If Contradiction, then not Satisfied (obviously). # If Not Contradiction, then Satisfied (not obvious, just a useful default). # The 'Dummy' constraint does nothing except execute a user-supplied procedure. # # The procedure is passed two arguments: "thismodule" and the optionalargs list supplied with the constraint. # The optionalargs must appear in the constraint even if it is empty. # The procedure must return 1 or 2 boolean values. If the first value is "true", then a contradiction is forced and # it doesn't matter what the second value is (and it may even be omitted). The second value indicates whether the # Dummy constraint should stay on the Unsatisfied list: false indicates it should stay and true indicates it should # be removed. # # Dummy constraints are given top priority and they stay on the Unsatisfied list until the problem is complete or # the procedure itself indicates that it is satisfied. Thus, the procedure will be executed once for every pass # through the Unsatisfied list. # # This type of constraint is useful for debugging, and also useful if the user wants specific information reported # that is not provided by the userinfo/infolevel facility. # # A particularly useful application of this constraint type is to change the infolevel settings when certain conditions # are met. For example, if you know that your problem has a bug sometime after the 30th guess is made, you could do this: # FindBug:= proc(M, opts) # use `&?`= M:-`&?` in if [&? Stats][6]=opts[1] then :-infolevel[all]:= opts[2]; return false, true fi end use # false, false # end; # # And make one of the constraints # Dummy(FindBug, [30, 5]) `Know/Dummy`:= proc(Proc::procedure, optionalargs::list) local result; result:= [Proc(thismodule, optionalargs)]; if result[1] then true else false, result[2] fi end proc; #Handle equality constraints `Know/=`:= proc(a,b) local Va, Vb, ca, cb; userinfo(4, 'Constraints', args); Va, Vb, ca, cb:= InternalRep(a, b); if Va = Vb then error `constants are in the same variable` fi; evalb(G[ca,cb]<>1 and ca &<=> cb) end proc; #Handle inequality constraints `Know/<>`:= proc(a,b) local Va, Vb, ca, cb; userinfo(4, 'Constraints', args); Va, Vb, ca, cb:= InternalRep(a, b); if Va = Vb then error `constants are in the same variable` fi; evalb(G[ca,cb]<>0 and ca & cb) end proc; # Handle assertions that give a subset of an SDR `Know/Distinct`:= proc(subSDR::list) local pair, a, b, Va, Vb; userinfo(4, 'Constraints', args); for pair in `if`(nops(subSDR)=2 ,[seq(seq([a,b], a= op(1, subSDR)), b= op(2, subSDR))] ,AllPairs(subSDR) ) do Va, Vb, a, b:= InternalRep(op(pair)); if Va<>Vb and G[a,b]<>0 and a & b then return true fi od; false end proc; # Assert that a is the successor of b wrt V `Know/Succ`:= proc(a, b, V::posint) local Va, Vb, ca, cb, i, satisfied, count, last_i; userinfo(4, 'Constraints', args); Va, Vb, ca, cb:= InternalRep(a,b); if Va=V or Vb=V then error `A constant is in the designated variable` fi; #a can't be b; a can't be 1st in V; b can't be last in V if Va<>Vb and G[ca,cb]<>0 and ca & cb or G[ca,&0 and ca & &V]<>0 and cb & &>V then return true fi; #Certain other positionings can also be ruled out for i from &V do if G[ca,i]=0 and G[cb,i-1]<>0 and cb & (i-1) then return true fi od; for i from &V -1 do if G[cb,i]=0 and G[ca,i+1]<>0 and ca & (i+1) then return true fi od; #if a or b are known wrt V then the other can be deduced. satisfied:= false; #if a's position in V is known then set b's i:= Soln[ca,V]; if i>0 then if G[cb,i-1]<>1 and cb &<=> (i-1) then return true fi; satisfied:= true fi; if not satisfied then #if b's position in V is known then set a's i:= Soln[cb,V]; if i>0 then if G[ca,i+1]<>1 and ca &<=> (i+1) then return true fi; satisfied:= true fi fi; if satisfied then userinfo(2, 'Constraints', `Constraint`, Succ(a, b, V), `completely satisfied.`) fi; false, satisfied end proc; #If a's position wrt V is known, then b's position can be restricted to the two positions next to a (or the # one position next to a if a is at an end). `NextTo/CheckForKnownPosition`:= proc(V::posint, a::posint, b::posint) local pos_a, i; userinfo(4, 'Constraints', V, Consts[a], Consts[b]); pos_a:= Soln[a,V]; if pos_a>0 then for i in ConstsInV(V) minus {max(pos_a-1,&V)} do if G[b,i]<>0 and b & i then return true fi od fi; false end proc; #Check if the Next-to condition is satisfied and consistent `NextTo/Check`:= proc(V::posint, a::posint, b::posint) local pos_a, pos_b; pos_a:= Soln[a,V]; pos_b:= Soln[b,V]; if pos_a<>0 and pos_b<>0 then if abs(pos_a-pos_b) = 1 then return 1 fi; #Solved userinfo(1, 'Constraints', `Cannot satisfy`, NextTo(Consts[a], Consts[b], V)); return 0 fi; 2 #Nothing known end proc; #For every position or pair of positions that we know b can't be in, that determines a position that a can't be #in if a has to be next to b. `NextTo/RuleOutImpossible`:= proc(V::posint, a::posint, b::posint) local i; userinfo(4, 'Constraints', V, Consts[a], Consts[b]); #If b can't be in position 2 then a can't be in position 1 if G[b, & 0 and a & &V -1 do if G[b,i-1] = 0 and G[b,i+1] = 0 and G[a,i]<>0 and a & i then return true fi od; #If b can't be in the 2nd-to-last position then a can't be in the last position G[b, &>V -1] = 0 and G[a, &>V] <> 0 and a & &>V end proc; #Assert that a is next to b wrt variable V `Know/NextTo`:= proc(a, b, V::posint) local Va, ca, Vb, cb, r; userinfo(4, 'Constraints', args); Va, Vb, ca, cb:= InternalRep(a,b); if Va=V or Vb=V then error `A constant is in the designated variable` fi; #a can't be equiv to b if Vb<>Va and G[ca,cb]<>0 and ca & cb then return true fi; if `NextTo/RuleOutImpossible`(V,ca,cb) or `NextTo/RuleOutImpossible`(V,cb,ca) or `NextTo/CheckForKnownPosition`(V,ca,cb) or `NextTo/CheckForKnownPosition`(V,cb,ca) then return true fi; r:= `NextTo/Check`(V,ca,cb); if r=0 then return true fi; if r=1 then userinfo(2, 'Constraints', `Constraint`, NextTo(a, b, V), `completely satisfied.`) fi; # Mathematical question: Guessing is a relatively expensive operation, most especially when you # need to prove uniqueness also. It is probably not efficient to divide the "NextTo(a,b)" into # the cases "Succ(a,b) or Succ(b,a)" (which necessarily means guessing that one of the two # disjuncts is true). false, evalb(r=1) end proc; # If a < b wrt V, and a's or b's position is known wrt V, then certain positionings of the other can be ruled # out. `Less/CheckForKnownPosition`:= proc(V::posint, a::posint, b::posint) local pos, i; userinfo(4, 'Constraints', V, Consts[a], Consts[b]); for i from &0 and b & i then return true fi od; pos:= Soln[b,V]; if pos>0 then for i from pos to &>V do if G[a,i]<>0 and a & i then return true fi od fi; false end proc; # Check if the a < b wrt V condition is satisfied or contradictory. `Less/Check`:= proc(V::posint, a::posint, b::posint) local pos_a, pos_b; pos_a:= Soln[a,V]; pos_b:= Soln[b,V]; if pos_a<>0 and pos_b<>0 then if pos_a < pos_b then userinfo(2, 'Constraints', `Constraint`, Less(Consts[a], Consts[b], V), `completely satisfied.`); return 1 else userinfo(1, 'Constraints', `Cannot satisfy`, Less(Consts[a], Consts[b], V)); return 0 fi fi; 2 #Nothing known end proc; # If a < b wrt V and a can't be in certain positions, then b can't be in certain positions, and vice versa `Less/RuleOutImpossible`:= proc(V::posint, a::posint, b::posint) local i; userinfo(4, 'Constraints', V, Consts[a], Consts[b]); # If b can't be in any of positions i..n, then a can't be in i-1..n for i from &>V by -1 to &0 and a & (i-1) then return true fi od; # If a can't be in any of positions 1..i, then b can't be in 1..i+1 for i from &V -2 while G[a,i]=0 do if G[b,i+1]<>0 and b & (i+1) then return true fi od; false end proc; #Assert that a < b wrt V. `Less/OnePair`:= proc(a, b, V::posint) local Va, ca, Vb, cb, r; userinfo(4, 'Constraints', args); Va, Vb, ca, cb:= InternalRep(a,b); if Va=V or Vb=V then #Trivial cases if Va=V and Vb=V then if caV then error `Impossible inequality`, aV]]) fi fi; r:= `Less/Check`(V,ca,cb); if r=0 then return true elif r=1 then return false fi; #a can't be equiv to b; b can't be 1st; a can't be last if G[ca,cb]<>0 and ca & cb or G[cb,&0 and cb & &V]<>0 and ca & &>V then return true fi; if Soln[ca,V]<>0 or Soln[cb,V]<>0 then if `Less/CheckForKnownPosition`(V,ca,cb) then return true fi elif `Less/RuleOutImpossible`(V,ca,cb) then return true fi; r:= `Less/Check`(V,ca,cb); if r=0 then true elif r=1 then false else false, false fi; end proc; #Process "Less Than" type constraints of more than two constants by breaking them down into pairs `Know/Less`:= proc(subSDR::list, V::posint) local pair, r; userinfo(4, 'Constraints', args); for pair in AllPairs(subSDR) do r:= [`Less/OnePair`(op(pair), V)]; if r[1] then return true elif nops(r)=2 then Prioritize(Less(op(pair), V)) fi od; false end proc; # Process OR type constraints by guessing each disjunct in succession. `Know/Or`:= proc(assertion::list) local pos, disjuncts; userinfo(4, 'Constraints', assertion); disjuncts:= assertion; pos:= disjuncts[1]; if not (pos::posint) then pos:= 1; disjuncts:= [1, op(assertion)] fi; Backup(OR(disjuncts)); Prioritize(disjuncts[pos+1]); false end proc; # Process ExactlyOne constraints. These are exclusive ORs. The handling is very similiar to the `Know/OR` # procedure. `Know/ExactlyOne`:= proc(assertion::list) local pos, disjuncts; userinfo(4, 'Constraints', assertion); disjuncts:= assertion; pos:= disjuncts[1]; if not (pos::posint) then pos:= 1; disjuncts:= [1, op(assertion)] fi; if pos = nops(disjuncts) then true else if pos < nops(disjuncts)-1 then Backup(ExactlyOne(disjuncts)) fi; map(Prioritize, [disjuncts[pos+1], op(map(Negate, subsop(1= NULL, pos+1= NULL, disjuncts)))]); false fi end proc; # Process AND type constraints by simply putting each conjunct into the queue. # # AND constraints are used in compound constraints, most notably in OR. They are also generated internally when # an OR constraint is negated. `Know/AND`:= proc(assertions::list) map(Prioritize, assertions); false end proc; # Process constraints specified by a user procedure: # # The user procedure must return a boolean and optionally another boolean and a list: # If the current grid contradicts the desired condition, then the first boolean should be "true". In this # case, it doesn't matter what the other returned values are, and they may even be omitted. # # If the current grid satisfies the desired condition, then return false, true. In this case, it doesn't # matter what the third returned value is, and it may even be omitted. # # If the situation is still unknown, then return false, false. The optional third returned value is a list # of constraints that can now be assumed. The list is specified in the same format as the argument to the Satisfy # command. # # It doesn't matter if the list is consistent. Inconsistency will be gracefully handled. To maintain # efficiency, it is best to only pass back constraints of the form a=b and a<>b. However, it is allowed to # pass back any type of contraints, even a procedural constraint. # # The user procedure may (but is not required to) accept a module argument and a list of optional arguments. The # optional arguments list must appear in the constraint, even if it is the empty list. # # Note that if the relationship can be specified by relating it to the ordering of the constants in a variable, then # it is easier and far more efficient to use Relational/Procedural constraint type provided by the procedure after # this one. # `Know/Proc`:= proc(P::procedure, optionalargs::list) local result; userinfo(4, 'Constraints', args); result:= [P(thismodule, optionalargs)]; if result[1] then userinfo(1, 'Constraints', Proc(P, optionalargs), `contradicted.`); true elif result[2] then userinfo(2, 'Constraints', Proc(P, optionalargs), `satisfied.`); false elif nops(result)=2 then false, false else map(Prioritize, result[3]); false, false fi end proc; #Process relation-constraints (the relation being taken wrt a specific variable) specified by a user procedure. # # The constraint is specified in the form Rel(Proc, A, B, V, O), where A and B are constants, V is a variable, and O is a # list of optional arguements. # # The first argument to Proc will be "thismodule". The user is not required to use this argument. It is only for # convenience so that the user does not need to use the module prefix to refer to the exported procedures. Rather, # a "use" statement can be used. # # The second and third arguments may be constants A' and B' from variable V (note that these are not the same A and B # that are used when the constraint is specified): # If both A' and B' are nonzero, then the procedure must return false or true to indicate whether the A' and B' # satisfy or do not satisfy the relationship. The procedure must not return anything else in this case. Note that "true" # indicates a contradiction: the given A' and B' do NOT satisfy the relationship. # # If A'<>0 and B'=0, then the procedure must return a *set*, possibly empty, of valid assignments B' for B in V # given that the assignment of A in V *could be* (but not necessarily *is*) A'. # # If A'=0 and B'<>0, then the procedure must return a *set*, possibly empty, of valid assignments A' for A in V # given that the assignment of B in V *could be* (but not necessarily *is*) B'. # # Note that the previous two paragraphs are perfectly symmetric. The constants in the set passed back must be in the # internal form provided by ConstNum. It is not necessary for the user procedure to check whether the returned set # of possibilities for A' or B' have already been eliminated or are otherwise contradictory; however, it is essential # that the returned set contain all possibly valid assignments. In other words, it does not matter if the returned # set is too big; however, the returned set being too small will lead to erroneous results. # # The fourth argument is the variable V in its internal form provided by VarNum. # # The fifth argument is the list of optional arguments. The list of optional arguments must appear in the constraint # even if it is the empty list. # # Note that all constant and variable arguments and return values are in the internal numeric form. # # Note that there is nothing that prevents you from using this type of constraint on a single constant: # Rel(Proc, a, a, V, [optionalargs]). # It can also be applied pairwise to a list of constants: # Rel(Proc, [a, b, c], V, [optionalargs]). `Know/Rel`:= proc(Proc::procedure, a, b, V::posint, optionalargs::list) local Va, Vb, ca, cb, r, pos_a, pos_b; userinfo(4, 'Constraints', args); Va, Vb, ca, cb:= InternalRep(a,b); r, pos_a, pos_b:= `Rel/Check`(Proc, ca, cb, V, optionalargs); if pos_a<>0 and pos_b<>0 then r elif pos_a<>0 or pos_b<>0 then r:= `Rel/KnownPosition`(Proc, pos_a, pos_b, ca, cb, V, optionalargs); if r then userinfo (1, 'Constraints' ,`No matching position for`, Consts[`if`(pos_a<>0, ca, cb)], `wrt`, Rel(Proc, a, b, V, optionalargs) ); true else r, pos_a, pos_b:= `Rel/Check`(Proc, ca, cb, V, optionalargs); r, evalb(pos_a<>0 and pos_b<>0) fi else if `Rel/RuleOutImpossible`(Proc, ca, cb, V, optionalargs) then true else r, pos_a, pos_b:= `Rel/Check`(Proc, ca, cb, V, optionalargs); r, evalb(pos_a<>0 and pos_b<>0) fi fi end proc; #Process "Rel" type constraints of more than two constants by breaking them down into pairs. `Rel/Pairwise`:= proc(Proc::procedure, constants::list, V::posint, optionalargs::list) local pair, r; userinfo(4, 'Constraints', args); for pair in AllPairs(constants) do r:= [`Know/Rel`(Proc, op(pair), V, optionalargs)]; if r[1] then return true elif nops(r)=2 and not r[2] then Prioritize(Rel(Proc, op(pair), V, optionalargs)) fi od; false end proc; # Check whether the relational constraint is already satisfied. In any case, return the positions of a and b in # V if they are known, and return 0 if they are unknown. `Rel/Check`:= proc(Proc::procedure, a::posint, b::posint, V::posint, optionalargs::list) local pos_a, pos_b; pos_a:= Soln[a,V]; pos_b:= Soln[b,V]; if pos_a<>0 and pos_b<>0 then if Proc(thismodule, pos_a, pos_b, V, optionalargs) then userinfo (1, 'Constraints' ,`Constraint`, Rel(Proc, Consts[a], Consts[b], V, optionalargs), `contradicted.` ); true, pos_a, pos_b else userinfo (2, 'Constraints' ,`Constraint`, Rel(Proc, Consts[a], Consts[b], V, optionalargs), `satisfied.` ); false, pos_a, pos_b fi else false, pos_a, pos_b fi end proc; # If a's position in V is known, we may be able to figure out b's position. Even if we can't, we may be able to # narrow down the possibilities for b. Vice versa for the case where b's position is known. `Rel/KnownPosition`:= proc(Proc::procedure, pos_a::nonnegint, pos_b::nonnegint, a::posint, b::posint, V::posint, optionalargs::list) local Possibles, i, n, c, all; userinfo(4, 'Constraints', args); all:= ConstsInV(V); Possibles:= all intersect Proc(thismodule, pos_a, pos_b, V, optionalargs); n:= nops(Possibles); c:= `if`(pos_a=0, a, b); if n>1 then for i in all minus Possibles do if G[c,i]<>0 and c & i then return true fi od elif n=1 then i:= Possibles[1]; evalb(G[c,i]<>1 and c &<=> i) else true fi; false end proc; # Suppose that both a's and b's position in V are unknown. Then by assuming each possibility for a's position, we # obtain a list of possibilities for b's position. Then exclude all the possibilities that are not in that list. # Vice versa by assuming each possibility for b's position. `Rel/RuleOutImpossible`:= proc(Proc::procedure, a::posint, b::posint, V::posint, optionalargs::list) local possibleB, possibleA, possible, i, n, c, pair, all; userinfo(4, 'Constraints', args); all:= ConstsInV(V); possibleB:= {}; possibleA:= {}; for i from &V do if G[a,i]=2 then possibleB:= possibleB union Proc(thismodule, i, 0, V, optionalargs) fi; if G[b,i]=2 then possibleA:= possibleA union Proc(thismodule, 0, i, V, optionalargs) fi od; for pair in [[a, possibleA], [b, possibleB]] do c:= op(1, pair); possible:= all intersect op(2, pair); n:= nops(possible); if n>1 then for i in all minus possible do if G[c,i]<>0 and c & i then return true fi od elif n=1 then if G[c, possible[1]] <> 1 and c &<=> possible[1] then return true fi else userinfo (1, 'Constraints' ,`No possible positions for`, Rel(Proc, Consts[a], Consts[b], V, optionalargs) ); return true fi od; false end proc; ############################################################################################################ # Some standard procedures for passing to "Rel" constraints ############################################################################################################ # Specify that a and b are in the same block of a partition of V. It is not necessary that a complete # partition be passed. Any subset of a partition with at least two blocks is fine. It is assumed that # a and b are distinct. SameBlock:= proc(M, a::nonnegint, b::nonnegint, V::posint, subpartition::list(set)) local S, c; c:= `if`(a=0, b, a); for S in map(_S -> map(ConstNum, _S), subpartition) while not member(c, S) do od; `if`(b=0 or a=0, S minus {c}, not member(b, S)) end proc; # Specify that a and b are in different blocks of a partition of V. It is not necessary that a complete # partition be passed. Any subset of a partition with at least two blocks is fine. DifferentBlock:= proc(M, a::nonnegint, b::nonnegint, V::posint, subpartition::list(set)) local subp, all, S, c; subp:= map(S -> map(ConstNum, S), subpartition); all:= `union`(op(subp)); c:= `if`(a=0, b, a); for S in subp while not member(c, S) do od; `if`(b=0 or a=0, all minus S, member(b, S) or not member(b, all)) end proc; # a and b must satisfy an equation. Equation:= (M, a::nonnegint, b::nonnegint, V::posint, solutions::list(set)) -> `if`(b=0 ,eval(solutions[1], _A= a) ,`if`(a=0, eval(solutions[2], _B= b) ,not (member(a, eval(solutions[2], _B= b)) and member(b, eval(solutions[1], _A= a))) ) ); # a and b are separated by at least 'separation' positions in V Separated:= proc(M, a::nonnegint, b::nonnegint, V::posint, separation::list) local n; n:= separation[1]; `if`(b=0, ConstsInV(V) minus {$a-n..a+n}, `if`(a=0, ConstsInV(V) minus {$b-n..b+n}, evalb(abs(b-a)<=n))) end proc; # a >= b wrt V. This is only used internally for the negation of "Less" constraints. GTequal:= (M, a::nonnegint, b::nonnegint, V::posint) -> `if`(b=0, {$&V}, evalb(a `if`(b=0, ConstsInV(V) minus {a-1, a+1}, `if`(a=0, ConstsInV(V) minus {b-1, b+1}, evalb(abs(b-a)=1))); # a is not the successor of b wrt V. This is only used internally for the negation of "Succ" constraints. NotSucc:= (M, a::nonnegint, b::nonnegint, V::posint) -> `if`(b=0, ConstsInV(V) minus {a-1}, `if`(a=0, ConstsInV(V) minus {b+1}, evalb(a-b=1))); ############################################################################################################ # Initialization procedures ############################################################################################################ #The constructors -- Build the table and initialize each entry. #Initialize all other global variables. Initialize:= proc() local Va,Vb,a,b; global infolevel; infolevel[sendmail]:= 99; if nops({op(map(nops,Vars))}) <> 1 then error `lists are not the same size` fi; Consts:= map(op,Vars); CPV:= nops(Vars[1]); NV:= nops(Vars); NC:= nops(Consts); protect('Consts','CPV','NV','NC'); Divider:= ; if NC <> NV*CPV then error `duplicate constant` fi; if NV<2 or NC<4 then error `must have at least 2 variables and 4 constants` fi; G:= rtable(symmetric, 1..NC, 1..NC, datatype= integer[1]); # The block diagonal entries are not used for anything. for Va from 2 to NV do for Vb to Va-1 do for a from &Va do for b from &Vb do G[b,a]:= 2 od od od od; StateStack:= SimpleStack(); RuleOutL:= SimpleStack(); UniquenessProof:= true; AutoGuess:= true; CollectStats:= false; Quiet:= false; Reinitialize() end proc; #Restart the problem without having to load the module again. Reinitialize:= proc() local Va,Vb,a,b; for Va from 2 to NV do for Vb to Va-1 do for a from &Va do for b from &Vb do G[b,a]:= 2 od od od od; Unsatisfied:= []; Soln:= array([[0$NV]$NC]); for a to NC do Soln[a,VarNumC(a)]:= a od; SavSoln:= map(eval, Soln); TableAltered:= false; PreviouslySolved:= false; StateStack:-init(); RuleOutL:-init(); priqueue[initialize](ClueQ); Sets:= 0; Unsets:= 0; Elims:= 0; Transfers:= 0; Pivots:= 0; RuleOuts:= 0; MaxLevel:= 0; Guesses:= 0; MaxDepth:= 0; userinfo(1, 'Constraints', `NoName`, print(`Okay`)) end proc; #Main body of module Initialize() end module end proc: