Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

195 lines (168 sloc) 10.253 kB
## ## ##### ##### $$$$$ $$$$ $$$$$$
## ## ## ## ## $$ $$ $$ $$
## ## ##### ## $$$$ $$$$$$ $$
## ## ## ## ## $$ $$ $$ $$
#### ##### ##### $$$$$ $$ $$ $$
======================================================
SLS SAT Solver from The University of British Columbia
======================================================
...Developed by Dave Tompkins (davet [@] cs.ubc.ca)...
------------------------------------------------------
... project website: http://www.satlib.org/ubcsat ....
------------------------------------------------------
======================
Future Planned Changes
======================
* Expect several new algorithm implementations with version 1.2
- if there is an algorithm you'd like to see, let us know :)
------------------------
Changes in version 1.1.0
------------------------
BUG BUG BUG
INTRO | FIXED | DESCRIPTION
1.0.0 1.1.0 Stats & RTD reports can cause crash when no (-r out) specified with a steps column
1.0.0 1.1.0 RTDs with search steps > 2^31 weren't sorted properly: (un)signed int issue
1.0.0 1.1.0 The RTD report could be incorrect if non -cutoff termination is used (-timeout, -noimprove) and <100% success
1.0.0 1.1.0 Wrong heuristic trigger for weighted adaptive nov+ [-alg adaptnovelty+ -w]
1.0.0 1.1.0 Score miscalculation in [-alg novelty(+) -w] and [-alg walksat-tabu -w]
1.0.0 1.1.0 Std. Deviation statistic miscalculation for row stats (not col. stats)
1.0.0 1.1.0 Some stats (example: VarFlipCounts) would only count from last restart
* code cleanup: Major changes to all help messages, now specific parameter verbose/terse messages req'd
* code cleanup: Method for adding column statistics has been changed / simplified
* parameter change: -prestart is now -srestart \
* parameter change: -rrestart is now -prestart } sorry about the confusion
* parameter change: -srestart is now -drestart /
* parameter change: -varinit is now -varinitfile
* parameter change: -timeout is now -gtimeout
* parameter change: -timeout is now seconds per run, -gtimeout is total seconds for all runs
* parameter change: you can now specify max as a parameter value for the cutoff i.e.: -cutoff max
* parameter change: you can now specify parameters as a factor of the # vars, i.e.: -srestart 100n
* parameter change: -varinitgreedy is now deterministic
* report change: report "best" has been renamed "bestsol"
* report change: report "unsatclauses" now prints for unsuccessful runs, and has a new paramter
* report change: the default statistics provided have been modified slightly
* column change: column/stat "time" has been renamed "timesteps"
* new algorithm: "DDFW" (-alg ddfw)
* new algorithm: "G2WSat" (-alg g2wsat)
* new algorithm: "Novelty++" (-alg novelty++)
* new algorithm: "PAWS" (-alg paws)
* new algorithm: "random walk" (-alg urwalk)
* new algorithm: "conflict-directed random walk" (-alg crwalk)
* new algorithm: "Deterministic crwalk" (-alg dcrwalk)
* new algorithm: "Deterministic Adaptive Novelty+" (-alg danovp)
* new algorithm: "RGSAT" (-alg rgsat)
* new algorithm: "Novelty+p" (-alg novelty+p)
* new algorithm: "G2WSAT+p" (-alg g2wsat+p)
* new algorithm: "Adaptive G2WSAT" (-alg adaptg2wsat)
* new algorithm: "Adaptive G2WSAT+p" (-alg adaptg2wsat+p)
* new algorithm: "VW1" (-alg vw1)
* new algorithm: "VW2" (-alg vw2)
* new algorithm variant: "Schoening's Algorithm" (-alg -crwalk -v schoening)
* new algorithm variant: "SAPS/WInit" (-alg -saps -w -v winit)
* new algorithm variant: "SAPS/WSmooth" (-alg -saps -w -v wsmooth)
* new algorithm variant: "Paramaterized Adaptive Novelty+" (-alg adaptnovelty+ -v params)
* new report: "Penalty report" (-r penalty)
* new report: "Penalty Mean report" (-r penmean)
* new report: "Penalty Stddev report" (-r penstddev)
* new report: "Penalty CV report" (-r pencv)
* new report: "Mobility" (-r mobility)
* new report: "Mobility - Fixed Window" (-r mobfixed)
* new report: "Mobility - Fixed Window Frequency" (-r mobfixedfreq)
* new report: "Auto-Correlation-Length" (-r autocorr)
* new report: "Unique solutions" (-r uniquesol)
* new report: "Best Step Solution Quality" (-r beststep)
* new report: "Trajectory Best Local Minima" (-r tbestlm)
* new report: "False Histogram" (-r falsehist)
* new report: "Distance" (-r distance)
* new report: "Distance Histogram" (-r disthist)
* new report: "Bias Counts" (-r biascount)
* new report: "Triggers" (-r triggers)
* new column: "Time in seconds, measured" (time)
* new column: "# of Local Minima Encountered" (localmins)
* new column: "% of steps in Local Minima" (percentlocal)
* new column: "Distance to known solutions(s)" (soldistance)
* new column: "Fitness-Distance Correlation Factor" (fdc)
* new column: "Auto-Correlation Length" (acl)
* new column: "Auto-Correlation of distance one" (acone)
* new column: "Estimated Auto-Correlation Length from AC of 1" (estacl)
* new column: "Mean Mobility of window size n (# vars)" (mobn)
* new column: "Mean Mobility of window size x" (mobx)
* new column: "Normalized Mean Mobility for window size n" (normmobn)
* new column: "Normalized Mean Mobility of window size x" (normmobx)
* new column: "Mobility C.V. for window size n" (mobncv)
* new column: "Mobility C.V. for window size x" (mobxcv)
* new column: "Average (Mean) # of False Clauses" (qualmean[_w])
* new column: "Std.Dev. # of False Clauses" (qualstddev[_w])
* new column: "Coeff. of Var. # of False Clauses" (qualcv[_w])
* new column: "Number of Restarts" (restarts)
* new column: "Worst solution encountered" (worst[_w])
* new column: "Last solution encountered" (last[_w])
* new column: "First solution encountered" (start[_w])
* new column: "Mean Improvement per Step to Best Solution" (bestavgimpr[_w])
* new column: "First Local Minimum - # of False Clauses" (firstlm[_w])
* new column: "Step of the First Local Minimum Encountered" (firstlmstep[_w])
* new column: "Improvement from Start to First LM / Impr. to Best" (firstlmratio[_w])
* new column: "Mean of the Trajectory Best LM" (tbestlmmean[_w])
* new column: "C.V. of the Trajectory Best LM" (tbestlmcv[_w])
* new column: "Number of up steps" (upsteps)
* new column: "Percent of up steps" (percentup[_w])
* new column: "Number of down steps" (downsteps)
* new column: "Percent of down steps" (percentdown[_w])
* new column: "Number of side steps" (sidesteps)
* new column: "Percent of side steps" (percentside[_w])
* new column: "Random Decisions Per Step" (randstep)
* new column: "CV of the Variable Flip Count Distribution" (flipcountcv)
* new column: "CV of the Clause Unsat Count Distribution" (unsatcountcv)
* new column: "Mean Branching Factor" (branchfact[_w])
* new column: "Mean Bias - Max" (biasmax)
* new column: "Mean Bias - Final" (biasfinal)
* new statistic: added the number of runs executed (runs)
* new statistic: added the number of successful runs (numsolve)
* new statistic: added the name of the instance file (instname)
* new statistic: added the algorithm parameters (alginfo)
* new statistic: added the number of unique solutions found (numunique)
* new statistic: added the version of UBCSAT (version)
* new statistic: added a statistic for the agemean column example in the mylocal.c (thanks to FH)
* new stat field: added var+stderr+vmr+sum
* new stat field: added stepmean
* new stat field: added solvemean+solvemedian+solvemin+solvemax
* new stat field: added failmean+failmedian+failmin+failmax
* new parameter: -filesoln specifies a file of known solutions for analysis & measuring FDC, solution distance, etc.
* new parameter: -filerand specifies a file to read random bits from (instead of PRNG)
* new parameter: -fileabort specifies a file that can be created to abort the current job
* new parameter: -findunique is like -find, except it only counts unique solutions
* new parameter: -rflush will flush out all output buffers between runs
* new function: CalculateStats() & CorrelationCoeff()
* new function: ActivateTriggers() & DeActivateTriggers() for explicit activation
* new file: ddfw.c
* new file: g2wsat.c
* new file: random.c
* new file: paws.c
* new file: derandomized.c
* new data type: VARSTATE is an array of bytes to store variable state information
* new data type: VARSTATELIST is a linked list of VARSTATEs
* code cleanup: all globals are now initialized in SetupUBCSAT() -- allows for multiple calls to ubcsatmain()
* code cleanup: ReadCNF() is now more robust w.r.t. invalid files, comments, etc.
* code cleanup: columns are now only allocated RAM when necessary (for medians, etc.)
* code cleanup: many weighted [_w] columns and statistics fail for unweighted algorithms
* code cleanup: all columns and statistics for weighted instances now end in [_w]
* code cleanup: added field bSpecialFileIO to REPORT for reports with "special" i/o requirements
* code cleanup: moved all (pClause++) elements outside of loops (bug fix)
* code cleanup: removed warning for failed activation of already disabled trigger
* code cleanup: changed default report for gwsat to default (was wdefault)
* code cleanup: Typo: WalkSatSKC was incorrectly coded as SKG (too many Dreamworks movies ;)
* code cleanup: UpdateBestFalse & UpdateSaveBest were moved from PostFlip to PostStep
* code cleanup: Now All parameters have a terse & verbose description
* code cleanup: IsLocalMinimum() now takes an argument for weighted algorithms as well
* code cleanup: "," can now be used to separate parameters instead of "|" (looks cleaner)
* code cleanup: IRoTS algorithms modified re: maintaining previous state information
* code cleanup: the "best[_w]" columns no longer require the "BestFalse" trigger
* code cleanup: renamed ActivateTrigger to ActivateTriggerID (and ActivateStat, etc...)
* code cleanup: changed code to use the constant FLOATZERO
* code cleanup: increased MAXCNFLINELEN
* code cleanup: CopyParameters() now adds to the end of the list instead of replacing it
------------------------
Changes in version 1.0.0
------------------------
* The changes in 1.0.0 (from 0.9.7) are far too numerous to list
* consult the archive section of the website for older revisions
Jump to Line
Something went wrong with that request. Please try again.