source code here !!!
news:
here's a one line patch that may be needed to compile on some systems
(BSD based ones?). i was sort-of aware of this, but chose to ignore
the issue. the relevant compiliation errors are pretty obvious. one of
these days, i'll fix this permanently in the release ...
*** Chaff2.C.orig Sat Jun 16 23:46:04 2001
--- Chaff2.C Wed Jul 17 19:41:04 2002
***************
*** 2,7 ****
--- 2,8 ----
// See the file LICENSE for details. #include"Solver.H"
+ #include<sys/time.h>
#include<sys/resource.h>
//#include<mon.h>
if you're brave, here's a binary dev snapshot that includes support for
custom decision orderings. you can a static ordering by providing a
weights file with the odering you want. i hope this build works ... tell me
otherwise :)
several people have asked about what some of the parameters mean, with
respect to controling memory usage and such. here's a snipet from a email
i sent out about this -- it should give you some ideas:
if you send me the instnaces, i can play with them. otherwise, the only
parameter that directly affects the database growth is the
addPostfixOnly=n with refers to the number of literals that must be
unassigned before an added clause is deleted. i think the default is 200,
you can also try 150, 100, or even smaller, depending on the instance. you
can try:
lime.smj
which is a different config that has this parameter set to 100, and
restarts less frequently, and adds more randomness. NOTE: this is now the
same lime.smj as in the current tarball. so if you have the current
tarball, you already have this configuration.
changing the frequency of restarts (restartPeriod and
restartPeriodIncrement) and the relevance parameter (addPostfixOnly) are
probably the two parameters worth messing with -- you can also change the
clearPeriod and clearPeriodIncrement, which effects how often the decision
statistics are right-shifted by clearShiftAmt. all the xxxPeriod
parameters are in units of (# of decisions).
also, randomnessAtRestart and baseRandomness control the amount of
randomness in the decision heuristic. baseRandomness = n means that a
variable with up to the n'th highest score may be chosen at each deicison.
randomnessAtRestart = n increases baseRandomness by n transiently (for n
decisions) at each restrart.
email me
solaris binary
linux binary
also, here's a staticly linked version of the linux binary (only the
executable). if you get shared library errors running the Chaff2
executable from the above linux package, grab this replacement exec:
static Chaff2 exec (for spelt3 distrib only)
you still need the above full distribution for the samples, config
files, scripts, and documentation (haha).
the README is (way) out of date, here's a supplement:
sample files:
[myfile.cnf]
p cnf 4 1
1 2 3 4 0
[myfile.cnf.w]
1 1 -1 1
4 2 -4 2
3 3 -3 3
2 4 -2 4
the .w file is a list of pairs <[-]variable, weight>, noting that a varaible
and it's negation are considerend seperatly. the decision heuristic will
choose the varaible (or negation) with the highest score. ties are broken
randomly. In the example above, the ordering would be { 2, 3, 4, 1 } with
the polarity of the decison chosen randomly, since the weight of x and -x
are the same for each var.
the default configuration file is cherry.smj, edit it as follows to do a
static ordering.
enable weights by setting:
useWeightsFile = 1
the name of the weights file is given by:
weightsFile = %1$s%2$s.w
also, if you want the ordering to be static, you would disable the internal
heurisitic with this parameter. other wise, don't change this.
maxLitsInClaseForConfDriven = 0
further, the weights generated by the internal heuristic are fairly small
(say always less than 10000) so if you specify very high initial weights,
you can 'partially' override the internal heuristic, for example, if you
set:
[myfile.cnf.w]
1 10000 -1 10000
4 10000 -4 10000
3 20000 -3 20000
2 20000 -2 20000
if would divide the vars into two 'pools'. if the interal heuristic is
diabled, then chaff would choose randomly from the 20000 pool, or if no
20000 var was unassigned, choose randomly from the 10000 pool. however, if
the internal heuristic is *not* disabled, then the internal heuristic would
break the 'tie' since if would (dynamically) add to the scores of the
varaibles.
note that i've never seen a purely static ordering the performs well on
large instances.
email me as questions arise,
Matt.
PS, note on filenames:
... in the configuartion file, there are two special varaibles %1$s and
%2$s
that chaff will substitue with the path and base name (respectivly) of
the
cnf file being processed, so if you specify:
BlahFile = %1$s%2$s.blah
OtherFile = %2$s.baz
AnotherFile = myspecificfile.thunk
then run Chaff like:
Chaff2 ../bar/foo2.cnf
then it will try to open:
../bar/foo2.cnf.blah (to use as the BlahFile)
foo2.cnf.baz (to use as the OtherFile)
myspecificfile.thunk (to use as the AnotherFile)
This works exactly for config parameters that expect a filename.
MULTIPLE SOLUTIONS:
gererall outline:
1) chaff finds a solution (if any) -- this solition S is a *full*
assignment
(chaff can only find full assignments during search).
2) chaff unassigns as many variables in the solution as it can, such that
all clauses still have at least one satisfying assignment. the heuristic
used is greedy -- a single pass is made through the varaibles, and each is
unassigened if possible, (in order, monotonically).
2a) if a set of primary variables is specified, PV, then only variables in
this set are considered for unassignment.
3) a clause representing the soltuion is added to the database, and search
proceeds.
3a) if PV is specified, any varaibles in the solution not in set PV are
discarded from the added clause. i.e. two solutions that differ only in
assignements to non-PV vars are 'uninteresting' and are all pruned
simultaniously.
4) the process continues until the instance is unsat (or ressources/max
solutions are exceeded).
example:
the inputs files are as follows:
mmoskewcz@freedom:~/work/s2temp> cat ss.cnf
p cnf 7 9
1 -2 3 0
-1 -3 0
2 -3 0
-1 2 6 0
1 -6 0
-2 -6 0
3 6 -7 0
-3 7 0
-6 7 0
mmoskewcz@freedom:~/work/s2temp> cat ss.cnf.primary
1 1
-1 1
2 1
-2 1
7 1
-7 1
and the configuration file is as follows (there are only a couple of
changes
from the default, to enable solution enumeration and such):
[topLevel]
includeLoadTime = 0
abortTime = 0
printCommandLineParams = 11
printResourceUsage = 11
printNewlineAtEnd = 0
[solver]
printInfoMessages = 11
printStats = 11
printDecisions = 0
restartPeriod = 2000
restartPeriodInc = 200
randomnessAtRestart = 3
addPostfixOnly = 200
minimizeSolutions = 0 # archaic and unused option
findMultipleSolutions = 1
solutionsFile = %2$s.sols
limitSolutionsToN = 0
markSpecialVars = 1
specialVarsFile = %1$s%2$s.primary
[decMem]
printInfoMessages = 1
baseRandomness = 0
maxLitsInClaseForConfDriven = 10000 # ie. consider all clases
breakTiesRandomly = 1
useLazyErase = 1
clearPeriod = 2000
firstClear = 2000
clearPeriodIncrement = 10
clearShiftAmt = 3
useWeightsFile = 0
weightsFile = %1$s%2$s.w
decayWeights = 0
[claseMem]
printInfoMessages = 11
printStats = 11
cleanupPeriod = 30000
run the code:
mmoskewcz@freedom:~/work/s2temp> ./Chaff2 ss.cnf
cnf path: ""
cnf base: "ss.cnf"
using solutions output file: "ss.cnf.sols"
Using config file: cherry.smj
Using log file: chaff.log
Using CNF file: ss.cnf
Each '*' from ClaseMem is 30000 Decisions ---
Using special vars file: "ss.cnf.primary"
Beginning solve()
All clases read/checked/added to db.
Unsatisfiable instance. Not sat. No solution.
Begin Solver::outputStats() ...
addedClases: 5
conflicts: 6
tooBigToAddClases: 0
totalDupes: 0
implLoops: 0
numImpls: 0
numDecs: 21
... Solver::outputStats() ends.
Begin ClaseMem::outputStats() ...
Initial clases: 9
Initial lits: 21
Initial lits/clase: 2.33333
Initial max lits in a clase: 3
final clases: 16
final lits: 41
final lits/clase: 2.5625
Final max lits in a clase: 3
deleted clases: 0
deleted lits: 0
deleted lits/clase: nan
net clases: 16
net lits: 41
net lits/clase: 2.5625
clases touched: 0
total skips: 0
impl skips: 0
... ClaseMem::outputStats() ends.
UserTimeForSearch: 0
TotalUserTime: 0
MaxMemUsedMB: 0
and finally, the output
mmoskewcz@freedom:~/work/s2temp> cat ss.cnf.sols
"[00XXXX0]"
"[11XXXX0]"
"[10XXXX1]"
"[01XXXX1]"