## ## ##### ##### $$$$$ $$$$ $$$$$$ ## ## ## ## ## $$ $$ $$ $$ ## ## ##### ## $$$$ $$$$$$ $$ ## ## ## ## ## $$ $$ $$ $$ #### ##### ##### $$$$$ $$ $$ $$ ====================================================== 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