# 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`, a**V]])
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:
**