picture The Stochastic Local Search SAT Solver from
The University of British Columbia - ß-Lab

(return the the main ubcsat page)

Algorithms in UBCSAT

Introduction

To the best of our knowledge all algorithms in UBCSAT behave identically to their orginal implementation. While the exact results may differ (because of different random search trajectories, etc.) over several runs the run-length distributions generated by UBCSAT are equivalent to those produced by the original algorithms.

For most algorithms the UBCSAT implementation is faster (or just as fast) as the original implementation. In the few circumstances where UBCSAT is slower the difference is usually due to UBCSAT reporting overhead and can be eliminated by turning off reports (use parameters: -r out null -r stats null).

Adaptive G2WSAT
Reference: Chu Min Li, Wanxia Wei, and Harry Zhang
Combining adaptive noise and look-ahead in local search for SAT
In Proceedings of the Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT-07), volume 4501 of Lecture Notes in Computer Science, pages 121-133, 2007.
(pdf)
-alg adaptg2wsat
Notes:
  • Uses Novelty+ as the WalkSAT algorithm and selects the oldest (not best) decreasing promising variable.
  • See the G2WSAT entry for additional implementation details.
Adaptive G2WSAT+p
Reference: Chu Min Li, Wanxia Wei, and Harry Zhang
Combining adaptive noise and look-ahead in local search for SAT
In Proceedings of the Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT-07), volume 4501 of Lecture Notes in Computer Science, pages 121-133, 2007.
(pdf)
-alg adaptg2wsat+p
Notes:
  • Uses Novelty+p as the WalkSAT algorithm.
  • See the G2WSAT entry for additional implementation details.
Adaptive Novelty+
Reference: Holger H. Hoos
An adaptive noise mechanism for WalkSAT
In Proceedings of the Eighteenth National Conference in Artificial Intelligence (AAAI-02), pages 655-660, 2002.
(pdf)
-alg adaptnovelty+
Notes:
  • There was an typo in the paper for updating wp: It should be wp := wp - wp * phi / 2. The results in the paper, the original implementation and the UBCSAT implementation are all based on this corrected value.
  • In the paper, the noise being adapted is the novelty noise (-novnoise in the novelty algorithm), not the random walk parameter (-wp) which is set to 0.01 by default in Adaptive Novelty+.
  • The UBCSAT implementation uses a higher precision to store the adaptive noise parameter, which may cause slight algorithmic variations on longer runs.
-alg adaptnovelty+ -v params
Notes:
  • This variant has 2 parameters (phi,theta) that allow you to adjust the algorithm's adaptivity.
-alg adaptnovelty+ -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT) including a weighted clause selection scheme.
Conflict-Directed Random Walk
Reference:
(pdf)
-alg crwalk
Notes:
  • Also known as Papadimitriou's algorithm.
-alg crwalk -v schoening
Reference:
(pdf)
Notes:
  • Also known as Schöning's Algorithm.
  • Is Papadimitriou's algorithm with a restart every 3n steps.
-alg crwalk -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT) including a weighted clause selection scheme.
-alg crwalk -v schoening -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT) including a weighted clause selection scheme.
DDFW: Divide and Distribute Fixed Weights
Reference: Abdelraouf Ishtaiwi, John Thornton, Abdul Sattar, and Duc Nghia Pham
Neighbourhood clause weight redistribution in local search for SAT
In Proceedings of the Eleventh International Conference on Principles and Practice of Constraint Programming (CP-05), volume 3709 of Lecture Notes in Computer Science, pages 772-776, 2005.
(pdf)
-alg ddfw
Notes:
  • The original implementation from the authors has a parameter (-tl) that was not mentioned in the original paper: with probability (1-tl) a random neighbour (in lieu of the neighbour with maximum penalty) is selected to distribute weight from. The UBCSAT implementation includes this parameter with a default setting of (0.99).
Deterministic Conflict-Directed Random Walk
Reference: Dave A. D. Tompkins and Holger H. Hoos
On the quality and quantity of random decisions in stochastic local search for SAT
In Proceedings of the Nineteenth Conference of the Canadian Society for Computational Studies of Intelligence (AI-06), volume 4013 of Lecture Notes in Artificial Intelligence, pages 146-158, 2006.
(pdf)
-alg dcrwalk
Notes:
  • This algorithm was developed for acadameic interest, and is not recommended for practical applications.
Deterministic Adaptive Novelty+
Reference: Dave A. D. Tompkins and Holger H. Hoos
On the quality and quantity of random decisions in stochastic local search for SAT
In Proceedings of the Nineteenth Conference of the Canadian Society for Computational Studies of Intelligence (AI-06), volume 4013 of Lecture Notes in Artificial Intelligence, pages 146-158, 2006.
(pdf)
-alg danov+
Notes:
  • This algorithm was developed for acadameic interest, and is not recommended for practical applications.
G2WSAT: Gradient-based Greedy WalkSAT
Reference: Chu Min Li and Wen Qi Huang
Diversification and determinism in local search for satisfiability
In Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT-05), volume 3569 of Lecture Notes in Computer Science, pages 158-172, 2005.
(pdf)
-alg g2wsat
Notes:
  • Uses Novelty++ as the WalkSAT algorithm.
  • Selects the best decreasing promising variable available, as per the paper and original implementation.
  • The algorithm noise parameter p as described in the paper is implemented in UBCSAT as (-novnoise).
  • The MAX-TRIES and MAX-FLIPS parameters correspond to UBCSAT parameters (-srestart MAX-FLIPS -cutoff MAX-TRIES * MAX-FLIPS). See the online UBCSAT FAQ for more details.
  • The original algorithm software implementation performed some pre-processing, whereas UBCSAT does not. See the online UBCSAT FAQ for more details.
  • The pre-processing was: duplicate literal elimination, pure literal elimination, true clause elimination and unit propagation.
-alg g2wsat -v novelty+oldest
Notes:
  • Uses Novelty+ as the WalkSAT algorithm.
  • Selects the oldest (not necessarily the best) decreasing promising variable.
  • This is the algorithm variant used by Adaptive G2WSAT+.
-alg g2wsat -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT) including a weighted clause selection scheme.
-alg g2wsat -v novelty+oldest -w
G2WSAT+p: Gradient-based Greedy WalkSAT with look-ahead
Reference: Chu Min Li, Wanxia Wei, and Harry Zhang
Combining adaptive noise and look-ahead in local search for SAT
In Proceedings of the Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT-07), volume 4501 of Lecture Notes in Computer Science, pages 121-133, 2007.
(pdf)
-alg g2wsat+p
Notes:
  • Uses Novelty+p as the WalkSAT algorithm.
GSAT: Greedy Search for SAT
Reference: Bart Selman, Hector Levesque, and David Mitchell
A new method for solving hard satisfiability problems
In Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), pages 459-465, 1992.
(pdf)
-alg gsat
Notes:
  • The MAX-TRIES and MAX-FLIPS parameters correspond to UBCSAT parameters (-srestart MAX-FLIPS -cutoff MAX-TRIES * MAX-FLIPS). See the online UBCSAT FAQ for more details.
-alg gsat -v simple
Notes:
  • This is a simpler variant that behaves the same as GSAT, but is implemented in a more striaghtforward manner, and is typically slower.
-alg gsat -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
GSAT/TABU: GSAT with Tabu search
Reference: Bertrand Mazure, Lakhdar Saïs, and Éric Grégoire
Tabu search for SAT
In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97), pages 281-285, 1997.
(pdf)
-alg gsat-tabu
Notes:
  • Also known as TSAT.
  • The MAX-TRIES and MAX-FLIPS parameters correspond to UBCSAT parameters (-srestart MAX-FLIPS -cutoff MAX-TRIES * MAX-FLIPS). See the online UBCSAT FAQ for more details.
-alg gsat-tabu -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
GWSAT: GSAT with Random Walk
Reference: Bart Selman and Henry Kautz
Domain-independant extensions to GSAT : Solving large structured variables
In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI-93), pages 290-295, 1993.
(pdf)
-alg gwsat
Notes:
  • Also known as GSAT-WALK, RWS-GSAT, GRSAT, GSATRW.
  • The algorithm noise parameter p as described in the paper is implemented in UBCSAT as (-wp).
  • The MAX-TRIES and MAX-FLIPS parameters correspond to UBCSAT parameters (-srestart MAX-FLIPS -cutoff MAX-TRIES * MAX-FLIPS). See the online UBCSAT FAQ for more details.
-alg gwsat -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
HSAT: GSAT with History Information
Reference: Ian P. Gent and Toby Walsh
Towards an understanding of hill-climbing procedures for SAT
In Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI-93), pages 28-33, 1993.
(pdf)
-alg hsat
Notes:
  • The MAX-TRIES and MAX-FLIPS parameters correspond to UBCSAT parameters (-srestart MAX-FLIPS -cutoff MAX-TRIES * MAX-FLIPS). See the online UBCSAT FAQ for more details.
-alg hsat -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
HWSAT: HSAT with Random Walk
Reference: Ian P. Gent and Toby Walsh
Unsatisfied variables in local search
In Hybrid Problems, Hybrid Solutions, pages 73-85, 1995.
(pdf)
-alg hwsat
Notes:
  • The MAX-TRIES and MAX-FLIPS parameters correspond to UBCSAT parameters (-srestart MAX-FLIPS -cutoff MAX-TRIES * MAX-FLIPS). See the online UBCSAT FAQ for more details.
-alg hwsat -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
IRoTS: Iterated Robust TABU Search
Reference: Kevin Smyth, Holger H. Hoos, and Thomas Stützle
Iterated robust tabu search for MAX-SAT
In Proceedings of the Sixteenth Conference of the Canadian Society for Computational Studies of Intelligence (AI-03), volume 2671 of Lecture Notes in Artificial Intelligence, pages 129-144, 2003.
(pdf)
-alg irots
-alg irots -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
Novelty
Reference: David McAllester, Bart Selman, and Henry Kautz
Evidence for invariants in local search
In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97), pages 321-326, 1997.
(pdf)
-alg novelty
Notes:
  • The algorithm noise parameter p as described in the paper is implemented in UBCSAT as (-novnoise).
-alg novelty -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT) including a weighted clause selection scheme.
Novelty+: Novelty with Random Walk
Reference: Holger H. Hoos
On the run-time behaviour of stochastic local search algorithms for SAT
In Proceedings of the Sixteenth National Conference on Artificial Intelligence (AAAI-99), pages 661-666, 1999.
(pdf)
-alg novelty+
-alg novelty+ -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT) including a weighted clause selection scheme.
Novelty++: Novelty with Diversification Probability
Reference: Chu Min Li and Wen Qi Huang
Diversification and determinism in local search for satisfiability
In Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT-05), volume 3569 of Lecture Notes in Computer Science, pages 158-172, 2005.
(pdf)
-alg novelty++
Notes:
  • The algorithm noise parameter p as described in the paper is implemented in UBCSAT as (-novnoise).
  • The MAX-TRIES and MAX-FLIPS parameters correspond to UBCSAT parameters (-srestart MAX-FLIPS -cutoff MAX-TRIES * MAX-FLIPS). See the online UBCSAT FAQ for more details.
-alg novelty++ -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT) including a weighted clause selection scheme.
Novelty+p: Novelty+ with look-ahead
Reference: Chu Min Li, Wanxia Wei, and Harry Zhang
Combining adaptive noise and look-ahead in local search for SAT
In Proceedings of the Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT-07), volume 4501 of Lecture Notes in Computer Science, pages 121-133, 2007.
(pdf)
-alg novelty+p
Notes:
  • The algorithm noise parameter p as described in the paper is implemented in UBCSAT as (-novnoise).
PAWS: Pure Additive Weighting Scheme
Reference: John Thornton, Duc Nghia Pham, Stuart Bain, and Valnir Ferreira Jr.
Additive versus multiplicative clause weighting for SAT
In Proceedings of the Tenth Pacific Rim International Conference on Artificial Intelligence (PRICAI-08), pages 405-416, 2008.
(pdf)
-alg paws
RoTS: Robust Tabu Search
Reference: Éric D. Taillard
Robust taboo search for the quadratic assignment problem
Parallel Computing, 17 no. 4-5 pp. 443-455, 1991.
(pdf)
-alg rots
Notes:
  • The UBCSAT implementation is based on the software implementation provided by Thomas Stützle.
-alg rots -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
R-Novelty
Reference: David McAllester, Bart Selman, and Henry Kautz
Evidence for invariants in local search
In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97), pages 321-326, 1997.
(pdf)
-alg rnovelty
Notes:
  • The algorithm noise parameter p as described in the paper is implemented in UBCSAT as (-novnoise).
R-Novelty+: R-Novelty with Random Walk
Reference: Holger H. Hoos
On the run-time behaviour of stochastic local search algorithms for SAT
In Proceedings of the Sixteenth National Conference on Artificial Intelligence (AAAI-99), pages 661-666, 1999.
(pdf)
-alg rnovelty+
RGSAT: Restarting GSAT
Reference: Dave A. D. Tompkins and Holger H. Hoos
Warped landscapes and random acts of SAT solving
In Proceedings of the Eighth International Symposium on Artificial Intelligence and Mathematics (SAIM-04), 2004.
(pdf)
-alg rgsat
Notes:
  • This algorithm was developed for acadameic interest, and is not recommended for practical applications.
-alg rgsat -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
RSAPS: Reactive SAPS
Reference: Frank Hutter, Dave A. D. Tompkins, and Holger H. Hoos
Scaling and probabilistic smoothing: Efficient dynamic local search for SAT
In Proceedings of the Eighth International Conference on Principles and Practice of Constraint Programming (CP-02), volume 2470 of Lecture Notes in Computer Science, pages 233-248, 2002.
(pdf)
-alg rsaps
Notes:
  • See the SAPS entry for additional implementation details.
SAMD: Steepest Ascent Mildest Descent
Reference: P. Hansen and B. Jaumard
Algorithms for the maximum satisfiability problem
Computing, 44 pp. 279-303, 1990.
(pdf)
-alg samd
Notes:
  • very similar to GSAT-TABU, except the age of flipped variables are not changed (and hence not tabu) if they were flipped in an improving search step.
-alg samd -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
SAPS: Scaling and Probabilistic Smoothing
Reference: Frank Hutter, Dave A. D. Tompkins, and Holger H. Hoos
Scaling and probabilistic smoothing: Efficient dynamic local search for SAT
In Proceedings of the Eighth International Conference on Principles and Practice of Constraint Programming (CP-02), volume 2470 of Lecture Notes in Computer Science, pages 233-248, 2002.
(pdf)
-alg saps
Notes:
  • The paper describes the clause weight update procedure to be: w_i := w_i * rho + (1 - rho) * w_avg, but in practice the first term (w_i * rho) is a scalar change that can be ignored. However, this also means that setting rho = 0 may not achieve the desired effect.
  • As a result the former change in the clause updates, clause weights can grow to be arbitrarily large and so UBCSAT (as did the original SAPS implementation) performs a re-normalization: whenever a clause weight exceeds the value of 1000, all clause weights are divided by 1000.
  • The UBCSAT implementation has an additional parameter of a threshold (-sapsthresh) that is used to determine how much an improvement is considered to be an improvement. The default parameter of (-0.1) is consistent with the value used in the original SAPS implementation. This threshold was not mentioned in the paper.
-alg saps -v winit -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
  • Clause penalties are initialized to the clause weights.
-alg saps -v wsmooth -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
  • Clause penalties are initialized to the clause weights and smoothed back to their initial values.
SAPS/NR: De-randomized version of SAPS
Reference: Dave A. D. Tompkins and Holger H. Hoos
Warped landscapes and random acts of SAT solving
In Proceedings of the Eighth International Symposium on Artificial Intelligence and Mathematics (SAIM-04), 2004.
(pdf)
-alg sapsnr
Notes:
  • See the SAPS entry for additional implementation details.
Uniform Random Walk
-alg urwalk
-alg urwalk -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT).
VW1: Variable Weighting Scheme One
Reference:
(pdf)
-alg vw1
Notes:
  • The algorithm noise parameter p as described in the paper is implemented in UBCSAT as (-wp).
VW2: Variable Weighting Scheme Two
Reference:
(pdf)
-alg vw2
Notes:
  • The algorithm noise parameter p as described in the paper is implemented in UBCSAT as (-wp).
  • Variable Weights are implemented in UBCSAT with (double) floating point precision.
  • In author's original source code, it exits on the first freebie variable it discovers, whereas in UBCSAT it uniformly randomly selects amongst all freebies randomly (as described in the paper) -- This is a very minor discrepency.

WalkSAT
Reference: Bart Selman, Henry A. Kautz, and Bram Cohen
Noise strategies for improving local search
In Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI-94), pages 337-343, 1994.
(pdf)
-alg walksat
Notes:
  • Also known as WSAT and WalkSAT/SKC
-alg walksat -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT) including a weighted clause selection scheme.
WalkSAT/TABU: WalkSAT with TABU search
Reference: David McAllester, Bart Selman, and Henry Kautz
Evidence for invariants in local search
In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97), pages 321-326, 1997.
(pdf)
-alg walksat-tabu
-alg walksat-tabu -v nonull
Notes:
  • Modified to take a random walk in lieu of a null flip.
-alg walksat-tabu -w
Notes:
  • This is a weighted variant that incorporates clause weights into the heuristic (i.e.: for Weighted MAX-SAT) including a weighted clause selection scheme.