| | Author | Average Score | Description |
| 1 | Aaron Doll | 2.32 | This is an efficient implementation of Walksat, with a p valueof .25. This probabilistically sets the starting values basedon the number of times a variable's sign is true.
|
| 2 | dusty | 2.37 | This sat-solver implements SatSolver with a faster check for the number of clauses that become false when a clause is flipped.
|
| 3 | Aristotle | 2.41 | WalkSat with random switch probability 0.2
|
| 4 | CookieMonster | 2.48 | InitSat is a WalkSat variant which attempts to begin WalkSat's stochastic process from a highly favorable starting model. It uses random sampling methodsto first randomly generate models and starts with the truthassignment which satisfied the most clauses. Thus, the rest of WalkSat (selecting a random unsatisfied clause, picking the literal within that clause which causes the fewest number of previously satisfied clauses to become unsatisfied) proceeds from a starting model in which variables which "favor" one truth assignment are already thusly assigned. Also includes randomized restarts.
|
| 5 | spl | 2.62 | Optimized WalkSat that keeps track of the best model it has seen so far. It keeps track of which clauses a literal is in, and also keeps track of the number of unsatisfied clauses total, to avoid re-computing every iteration.
|
| 6 | Matt Haake | 2.79 | Modified version of walkSAT, which randonly generates p for choosing if the algorithm should choose greedily or randomly. Also, allows for random resets and does some pruning for clauses of length 1. Only checks clauses which will have been changed by flipping a symbol to imporove performance
|
| 7 | Tao | 4.16 | I implement the WalkSAT algorithm. To speed up the searching of symbol-clause pair, for each symbol, I implement the HastSet to store the indices of clauses where it appears.
|
| 8 | David H. | 4.31 | This is an implementation of WalkSat
|
| 9 | Quite Satisfied | 4.42 | WalkSAT variant that stores a map for each literal to the clauses it appeasrs in so that only relevant clauses are checked.
|
| 10 | BH | 4.53 | WalkSat Breakcount: Use a breakcount- the number of already satisfied clauses that become broken if a symbol is flipped, to choose which bit to flip
|
| 11 | Glenn Fisher | 4.58 | This SAT solver implements WalkSAT but improves upon the initial assignment of symbols using the pure symbol and unit clause heuristics described in Russell/Norvig p. 260.
|
| 12 | jgs | 4.67 | This sat-solver uses WalkSAT with an empirically optimized probability to try and maximize the number clauses it can satisfy before time runs out.
|
| 13 | Joshua Zimmer | 4.76 | This sat-solver generates models via WalkSAT and returns the best one when time runs out.
|
| 14 | Janie Gu | 4.92 | This sat-solver is a variant of the WalkSAT algorithm that uses an adaptive mechanism to dynamically adjust the probability of random walk.
|
| 15 | Mike Hawk | 4.96 | A modified WalkSat
|
| 16 | Deric Cheng | 5.03 | This sat-solver implements an enhanced version of the WalkSAT algorithm by choosing to either randomly flip a symbol in the model or flip the symbol that maximizes the number of satisfied clauses.
|
| 17 | Anon5 | 5.05 | My SatSolver works like vanilla walksat with one major modification. Let p be the probability of choosing to do a 'random walk' move. p starts out low and is increased when walksat hasn't been making progress (i.e. is at a local minimum).
|
| 18 | Andys | 5.11 | Variant of WalkSAT, with varying probability of flipping
|
| 19 | Walter Little | 5.12 | Modification of WalkSAT that presets unit clauses to the appropriatevalue
|
| 20 | NA | 5.14 | Modified WalkSAT
|
| 21 | Yacob Y. | 5.18 | A variant on Walk-SAT where we generate the probability for flipping a random symbol in the clause every time through the loop instead of a constant 0.5.
|
| 22 | Sabar Dasgupta | 5.18 | Solves Sat problems using a variation of WALKSAT that saves the best model seen so that it can be returned if time elapses.
|
| 23 | Absurdity | 5.22 | Implements the WalkSAT algorithm for finding satisfying models of CNF sentences.
|
| 24 | haoyu | 5.26 | DPLL algorithm, with early termination, pure symbol heuristic and unit clause heuristic.
|
| 25 | EC | 5.32 | Vanilla WalkSat
|
| 26 | Andrew Grasso | 5.33 | Implements WALKSAT
|
| 27 | Mr. Blobby | 5.34 | Mr. Blobby's SAT solver is an implementation of WalkSat that random walks with probability 0.5 and random restarts if no solution is found within 6 seconds of last search.
|
| 28 | John Whelchel | 5.44 | This is an implementation of the WalkSAT satisfiability algorithm. It flips a random symbol approximately 20% of the time based on my own personal experiments.It also initalizes the intial model to false/true valuesbased on the number of occurences of each symbol as atrue or false value in the CNF.
|
| 29 | snowflakes | 5.51 | My SAT solver uses walksat with adaptive noise. If the algorithm goes6 steps without improving, it increases the noise, and if it goes 3 stepswithout increasing the noise, it decreases it
|
| 30 | Andrew Werner | 5.54 | The implementation is WalkSAT as outlined in the text.
|
| 31 | HashTagAlreadyFallBreak | 5.57 | A variation of WalkSat, with improved implementation
|
| 32 | vhsiao | 5.62 | This is a variant of WalkSAT that performs pure symbol heuristics before entering the main while loop. Also, it attempts to use some "early termination" techniques to make it easier to find the literal which maximizes the number of satisfied clauses
|
| 33 | AFC | 5.66 | This sat-solver implements DLL with indexing optimizations, random restarts, and intelligent ordering
|
| 34 | Valya Barboy | 5.76 | Implements WalkSAT in order to try to find solutions to CNF sentences. Randomizes p, the probability with which it picks whether to flip a random symbol or the one that satisfies the most clauses.
|
| 35 | 0108 | 5.93 | An implementation of the WalkSat algorithm, using a p of 0.5.
|
| 36 | Green "The Bean" Choi | 5.94 | This sat-solved is an iterative version of DPLL algorithm.
It implements iteration (not recursion), degree heuristic, true clause storage, unit clause propogation, and excludes non-initial pure symbol propogation
|
| 37 | Tree Prophet | 6.05 | I implemented DPLL with the pure symbol and unit clause heursitics with the optimization of always keeping track of the best model found so far and short-circuiting as soon as that best model has all clauses satisfied or when time runs out. In the case of the latter, as is the case when the algorithm runs to completion, the model generated along the search that satisfies the most clauses is returned.
|
| 38 | Lisa Kim | 6.11 | This sat-solver generates random models
using Walk SATand returns the best one when time runs out.
|
| 39 | DeeEmEm | 6.26 | DPLL algorithm with addition of keeping track of best assignment found so far.
|
| 40 | Matt Goldsmith | 6.56 | I used WalkSAT with a couple optimizations. I kept a list of unsatisfied clauses to speed up getting a random one and getting the number of unsatisfied clauses. In the algorithm, there is also a key-map object of symbols to clauses to reduce the time it takes to update the unsatisfied clause list after changing a symbol.
|
| 41 | 13a | 6.65 | First, the solver looks for pure symbols and unit clauses. Then it does WalkSAT for a certain time, after which it changes to a different algorithm that is like WalkSAT, but looks at the shortest unsatisfied clauses. The more time the algorithm has run, the more random flips it does at a time.
|
| 42 | bigwig | 6.69 | Basic walksat. One possible improvement is that it decides whether or not todo walksat or pick a random unsatisfied clause beforechecking to see if it's satisfiable... therefore reducing the amount of data it needs to keep track of while check if satisfiable.
|
| 43 | Aaron H | 6.69 | Uses a modified WalkSAT algorithm with infinite number of flips and random restarts. The timer value indicates when the algorithm should 'give up'.
|
| 44 | Charlie Shucheng Zhu | 6.85 | My SAT solver's description: A variant of WalkSAT solver with restart feature.
|
| 45 | Jonathan Kwok | 6.99 | Modification of WalkSat taking account for clauses with only one literal.
|
| 46 | ModifiedWalkSatBreakZero | 7.22 | This algorithm uses more advanced data structures to implement WalkSat with an additional modification that symbols in failed clauses that do not break other clauses when switching are flipped first.
|
| 47 | Jameh | 7.41 | This sat-solver uses a simple randomized WalkSat algorithm to solve satisfiability problems.
|
| 48 | Solving For Clauses | 7.42 | On every iteration, the algorithm picks an unsatisfied clause and picks a symbol in the clause to flip. It chooses randomly between flipping by minimizing the number of unsatisfied clauses in the new state and picking the symbol randomly
|
| 49 | Linda | 7.42 | A run-of-the-mill walkSat implementation that flips a randomly selected literal of a randomly chosen unsatisfied clause.
|
| 50 | CAPS LOCK | 7.49 | Version 2.0, an optimized implementation of WalkSAT. There are a couple of small changes: randomly generating multiple initial models, only updating the model after the min conflicts step if the new model is better, etc. The big change is to when the algorithm chooses to random walk vs. searching for min conflicts: if the number of symbols * the average number of symbols per clause is less than or equal to the number of clauses, the algorithm only random walks and never searches for min conflicts.
|
| 51 | Ben Chen | 7.65 | The SatSolver is based on WalkSat with a slight modification. Clauses that contain only one literal each are initially noted. Because a clause with only have one literal is trivially easy to solve, the values of the symbols corresponding to these single literal clauses are permanently set. During WalkSat, changing the values of these preset symbols is avoided.
|
| 52 | burrito | 7.79 | Implementation of WalkSAT that includes some optimizations. One is to save a copy of the model that satisfies the most clauses so far, and when time runs out to return that best model, instead of the model that is currently being used by the algorithm.
|
| 53 | Elphaba | 8.01 | This sat-solver implements DPLL and relies on the degree heuristic for variable ordering. When time runs out it returns the current model with unset literals set to false.
|
| 54 | Khoa | 8.04 | An implementation of WalkSat
|
| 55 | An Extremely Ordinary Sloth | 8.05 | This is a variant of Walk-SAT. It sets up a list of literals whose values should never change and uses random restarts.
|
| 56 | Mike Honcho | 8.21 | Based around walkSAT, but prioritizes unsatisfied clauses with less literals in them, and then prioritizes literals which are in lessclauses with exactly 1 satisfied literal in them (i.e. that would become unsatisfied if said literal changed signs
|
| 57 | kt4124 | 8.36 | Variant of WalkSat and Novelty. With probability (1-p), flips either the symbol in a given clause that minimizes the number of unsatisfied clauses in the model, or the 2nd best symbol, based on the symbol's age. Otherwise, flips a random symbol in the clause.
|
| 58 | Keji Xu | 8.43 | This SAT-Solver uses WalkSAT and returns modelor best model if time runs out. It quickly selects unsatisfied clauses and
most likely flips the literal in that clause that will minimize the number of unsatisfied clauses.
|
| 59 | R. A. B. | 8.51 | WalkSat algorithm with restarting to avoid local minima. At each iteration does random flip with probability one-half and greedy flip with probability one-half.
|
| 60 | Shaheed Chagani | 8.79 | WalkSAT with improvements like an adaptive value of p, an improved starting model and a faster way to calculate the number of Unsatisfied Clauses
|
| 61 | Blam | 8.95 | This is an implementation on a variant of WalkSAT. The difference is it does a random restart if the time remaining is 1/3 the time that is allowed by the parameter
|
| 62 | Nihar the Great | 9.32 | This solver uses a modified version of WalkSAT to solve the problem. With every iteration, it picks a random variable in an unsolved clause and checks to see if flipping it will benefit. If so, it flips it. Also, all variables are initially set to false
|
| 63 | Ytterbium | 9.41 | A modified version of WalkSAT. Occasionally flips two clauses instead of one.
|
| 64 | bfang | 9.59 | Runs DPLL (pure symbol heuristic, unit clause heuristic, degree heuristic)
and switches to WalkSAT with frequent random restarts when time is almost up.
|
| 65 | Samuel Jerome | 9.70 | It's walkSAT with 5 random restarts.
|
| 66 | Tiny Wings | 9.92 | This is basically a WalkSAT implementation but tries to optimize runtime using efficient data structures and bookeeping schemes.
|
| 67 | dfshasdsf12 | 10.00 | This sat-solver utilizes a probabilistic variant of WalkSat to generate the best model or solve the CNF.
|
| 68 | Joel Faron | 10.49 | This is a modified version of the DPLL sat-solver which includes better variable ordering and some randomization.
|
| 69 | Sprt | 10.62 | This sat-solver combines elements of DPLL (namely pure symbol finding) with a modified WalkSat algorithm (randomly flips two variables in an unsatisfied clause rather than one) in order to find a model satisfying the provided CNF, or to return the best model found so far if a solution cannot be found within the time limit.
|
| 70 | Ravi Tandon | 10.65 | Implementation of a modified version of the WalkSat Solver.
|
| 71 | LilThug | 11.35 | WalkSAT, with some initial allowances for the pure symbol heuristic and the unit clause heuristic.
|
| 72 | Boomshanka | 11.42 | Implements a version of walkSAT that has several improvements including adding a watch literal, a HashMap of symbols to their respective clauses, a maximizing function to flip the variable that maximizes true clauses, and more.
|
| 73 | KingBach | 11.45 | Sat solver does unit resolution sets most common variable first and then follows standard WalkSat procedure (but does not reset original unit resolved variables).
|
| 74 | Brendan Wright | 11.47 | A DPLL-based solver. I was careful to avoid repeated computation in my model-checking method by maintaining a list of which clauses were invalid on the previous check, and only checking those.
|
| 75 | weezy | 11.50 | This SatSolver implements a version of WalkSAT similar to that described in the Russell and Norvig text.
|
| 76 | Mickey Mouse | 11.58 | This algorithm is an adjusted WalkSAT algorithm. The improvements being used are randomizing the probability at which a random clause is switched and having random restarts with a small probability.
|
| 77 | bchouSolver | 12.11 | DPLL solver with random restarts and random walking. The random branching heuristic favors symbols that appear many times but in short clauses.
|
| 78 | Anon_K_P | 12.24 | This SAT solver uses a variant of DPLL with early termination but without the pure symbol or unit clause heuristics. It returns either a satisfying model or the best model found when time runs out.
|
| 79 | Mark Fillmore | 12.26 | This sat-solver is a modified version of WalkSAT. It gives every clause a random rank and inserts it into a Priority Queue. All literals are initially set to false. Clauses are then removed from the Priority Queue, and if they are not satisfied, a random literal assignment is made. Simulted annealing determines whether or not this random assignment is allowed to continue. If it is, any clause that contains this literal is put back on the Priority Queue. This is repeated until time runs out, or a satisfiable solution is disovered.
|
| 80 | George Okeowo | 12.57 | This sat-solver uses a simplified blend of DPLL and randomization, returning the best found thus far when time runs out.
|
| 81 | RedOrangeBlue | 12.68 | WalkSAT with the pure symbol method from DPLL and an objective function which accounts for both satisfied and unsatisified clauses.
|
| 82 | Cam Porter | 13.10 | Improvised WalkSat algorithm that takes into account the timer, as well as implementing a few efficiencyimprovements based on trial and error, and methods mentioned in the book
|
| 83 | T. Capote | 13.10 | Variation on standard WalkSAT algorithm. Some improvements includenot flipping most recently flipped symbol in order to prevent stagnationand favoring minimizing unsatisfied clauses over random flipping as timeelapsed increases. Favors random flips if minimizing unsatisfied clausesis of little help.
|
| 84 | Happy | 13.29 | Runs a version of WalkSat with 5 intermediate points at which it checks whether the best assignment has been updated recently. If not, it resets the values to 0 and thus restarts the search
|
| 85 | The Kraken | 13.42 | This implements the walkSat algorithm, which uses a hill climbing approach combined with some randomness. A couple improvements being randomly restarting fresh with a new input seed and sometimes flipping 2 bits instead of 1.
|
| 86 | BMJ | 13.87 | This solver implements WalkSAT with the unit clause heuristic.
|
| 87 | cat | 14.07 | Implements WalkSat. Does some initial pre-processing to make it more efficient. Uses a counter to determine which variable to flip and randomly uses the counter or flips a variable at random (w/ probability .8).
|
| 88 | Supahaka | 14.69 | The love-child of WalkSAT and DPLL. Performs forward chaining while doing WalkSAT. As an impatient child, will give up if it doesn't see much progress being made.
|
| 89 | Alex Fish | 14.90 | My algorithm is a vanilla version of WalkSat. In implementing the algorithm, I've made some slight improvements.Particularly, I avoid reevaluating each clause more than once when computing the set of false clauses and determining whether or not a false clause still exists.
|
| 90 | David Lackey | 14.99 | This sat-solver uses a variant of the WalkSAT algorithm to solve CNF formulas before time runs out.
|
| 91 | Mercury | 15.35 | Variant of WalkSat where breakcounts are only approximated by the number of clauses where a symbol is true, vs the number of clauses where that symbol is false. Indexing and added datastructures allow fast choice of random unsatisfied clause, symbol assignment propagation, and choice of next symbol. Runtime dominated by branching cost of major while loop.
|
| 92 | Sunny | 15.63 | This sat-solver uses DPLL method along with gaussian (mean = given time/2) type random restarts
|
| 93 | Gewang | 15.98 | When time runs out, the SAT-solver will return the best random model it generates
|
| 94 | Jessie Chen | 16.28 | WalkSAT implementation. Min-conflicts is implemented by flipping each symbol and finding the flip that results in the smallest number of unsatisfied clauses.
|
| 95 | K.L. | 16.52 | walkSAT - literal to flip is one that maximizes true clauses
|
| 96 | cmF5a3ly | 17.39 | Modified WalkSAT with randomization and restart. When encountering multiple options on which symbol to flip, WalkSAT picks a random one, cycling through each symbol a large number of times. After randomizing a large number of symbols, WalkSAT restarts to look for a better locally optimal solution.
|
| 97 | Bebe Shi | 17.52 | WalkSAT but returns the best model found.
|
| 98 | SuperFan | 18.04 | This algorithm is an implementation of a k beam Walk-Sat with random restarts. The algorithm continuously updates the remembered models by randomly choosing a model and flipping a bit, then deciding whether to accept the move or use the heuristic.
|
| 99 | Bob Dondero | 18.35 | This sat-solver starts with the pure symbol and unit clause heuristics; flips the symbol that will minimize the number of unsatisfied clauses; applies random restarts with some probability p, or with certainty if the min flip symbol is unhelpful; and consistently checks if the model has been improved.
|
| 100 | Fanny | 18.66 | My SAT solver based on walkSAT.
|
| 101 | Dr Roberto | 19.07 | Variant of DPLL that uses indexing and keeps track of which clauses and symbols are being affected by a specific change in the model and then only checks those as opposed to checking all of them is search for potential new satisfactions. It also contains random choice of true or false and symbol ranking.
|
| 102 | Qinlan Shen | 19.97 | DPLL algorithm with degree heuristic and top level component analysis. Runs DPLL, choosing the symbol in the largest number of unsatisfied clauses when examining non-pure, non-unit-clauses symbols. This sat solver will perform component analysis before assigning the first symbol.
|
| 103 | TSATTER | 21.52 | This algorithm implements...
|
| 104 | cjt | 23.72 | This sat-solver generates models using the WalkSat algorithm.
|
| 105 | Tom T | 26.30 | This SAT solver is a variant of WALKSAT. First, it tries to assign truth values to pure symbols. Then, it uses WALKSAT to solve the remaining literals.
|
| 106 | soccer | 26.55 | This algorithm is a version of the standard WalkSat with several imporvements.These include making the probability of flipping a random symbol inversely related to the number of false clauses and making it possible to flipseveral random symbols during a single step of the algorithm. Random restarts are also possble depending on the number of sybmols
|
| 107 | Nikhilesh Sigatapu | 27.00 | DPLL with unit propagation, pure literal elimination. Picks most frequently occuring variable to try true/false for backtracking each time
|
| 108 | Yan Wu | 27.43 | This sat-solver uses WalkSat to solve a given CNF. Variations include random restarts after a given number of literal flips, and selecting 3 unsatisfied clauses instead of one.
|
| 109 | Sat Solver 2013 | 31.39 | This sat-solver uses WalkSat with efficient indexing that maintains a list of clauses in which each symbol appears as positive and negative literals.
|
| 110 | The Whitman Whale | 35.07 | A DPLL implementation of sat solver. For speed, datastructures are maintained that all clauses containing a symbol to be referenced.
|
| 111 | Sally Smith | 37.95 | I implemented walksat as it is stated in the pseudocode in the textbook. I created a random model and then with probability p, flipped a randomly selected symbol in a randomly selected false clause. With probability (1-p), I flipped the symbol in the randomly selected false clause that maximizes the number of satisfied clauses. When time runs out, I return the best model I have.
|
| 112 | Bar Shabtai | 43.67 | The SAT solver is an improvement on the classic WalkSat algorithm. It does so by picking the unsatisfied clause with the least amount of literals. The rest of the algorithm follows the classic one
|
| 113 | ebp | 44.34 | Keeps track of both a current model and symbols that we're certain of, trying to find the latter when we can and otherwise choosing which variable to flip randomly as in WalkSat.
|
| 114 | Jordan Ash | 54.77 | This is a fairly straight-forward implementation of thewalkSAT algorithm. Values for MAXFLIPS and p were determined by experimentand are outlined in the assignment writeup. The documentation used as aid with this assignment could be found at http://www.cs.duke.edu/courses/spring01/cps271/LECTURES/sat.pdf.
|
| 115 | jabreezy | 57.97 | This Sat Solver is based on DPLL. It is implemented as an iterative SAT search. It deduces at each step with unit propagation, in addition to preprocessing done before all steps. Each next variable is chosen for assignment based on a priority queue in which the variables are ranked by occurences in clauses. The assignment for said variable is also chosen by heuristic (of which I have two).
|
| 116 | David Paulk | 71.80 | MySatSolver is designed to be an improvement of the vanilla WalkSAT algorithm. The features that enhance MySatSolver are that probability of flipping a random symbol is given as function of the clause-to-variable ratio in the satisfiability problem, and that the number of symbol sign flips to maximize the number of satisfied clauses depends on the change in the number of satisfied clauses resulting from the previous rounds of symbol-flipping.
|
| 117 | Miranda | 105.24 | This sat-solver works and returns the best one when time runs out.
|
| 118 | Igor | 142.24 | description
|