WinSAT

Introduction

In an effort to support the SAT research community we have developed the WinSAT application. Its primary use is to help researchers run different algorithms on SAT problems, and provide results that can help in their analysis. You can currently use the program to search for solutions using a few stochastic algorithms such Basic Hill-Climbing, GSAT and WalkSAT. You can also enhance the search using K-Means clustering and perturbations. Although we do not recommend that a researcher skip on programming the different search methods on their own, but this tool should provide a benchmark by which they can test their algorithms against. (If you don't know what satisfiability is, then please read our SAT and MAX-SAT for the Lay-Researcher page.)

Using WinSAT you can open CNF files, and run the different search methods on them. You can also cascade the different search methods one after the other, loop through them several times and observe the results at each stage of the search. You can create random instances using the Fixed-Clause-Length model for a range of k values, variables and ratios. In addition, You can start with as many initial random assignments as you wish.

Each of the different search methods has its own settings. You can set the number of iterations you want the method to run before ending the search, you can set the probability of the random walk in WalkSat, or you can set how many centroids you would like the K-Means algorithm to find for example.

Once WinSAT is run, it stores the results of the search for each of the assignments in a sheet. The problem description is included in the sheet along with the cost (the number of unsatisfied clauses). Each new problem that is run will have its results recorded in the sheet. Form the results sheet you can also view the CNF file that was loaded or randomly created for test. In addition, the solution, true or false represented by 1s and 0s can be viewed through the results sheet.

We have created a page on the performance of the WinSat compared with ubcsat. This should give you an idea of how fast WinSat performs.

The Control Panel

The control panel is pretty much where everything is. You can load CNF files, create random problem instances, set the working directory, and choose search methods, open the results sheet and so on:

Opening a CNF file

To open a CNF file go to the File menu, and choose Open CNF File. The CNF file should follow the DIMACS format.

Once the file is loaded WinSat will display the file information as the current problem. This information will include the file name, the number of variables, the number of clauses and the ratio.

Random CNF Files

In addition to loading CNF files you can also generate random CNF files for your search. There are several parameters you need to set to create these files. These parameters control the the size of the problems, and the number of instances you want to generate. You can create problems with different literals per clause, a specific number of variables, and ratio. You can also generate a range of problems starting from a particular number of variables, and ending with another in steps. The same applies to the ratio. You can also specify how many problems instances you want to have per step.

The parameter found in the random problems section is k. This value specifies the number of literals you want to have in each clause. If you wanted to generate a 3-SAT problem, then you would set "k from" to 3 and "k to" to 3. When the problems are generated they will have exactly 3 literals per clause. If you wanted to generated a variable number of literals per clause, then set a lower and upper values for k. As an example, if you wanted to generate problems with 2 to 5 literals per clause, then set "k from" to 2, and "k to" to 5.

You can also set the number of variables in your random problems. If you want your to have a problem with 100 variables, then set the "from" and "to" of the variables text boxes to 100. On the other hand, if you wanted to create many problems starting from 4000 variables ending with 8000 variables in steps of 1000, then you would set "Variables from" to 4000, the "Variables to" to 8000 and the "Variables Steps" to 1000. That should create 5 random problem instances at each step.

You can also set the ratio α for the problems. That will affect the number of clauses per problem. If you had 50 variables with a ratio of 4.3, then your problem will have 215 clauses. Setting the ratio range is done in exactly the same way as the variables.

Each time you change the number of variables or the ratio the number of clauses will change in the "Clauses from" and "Clauses to" text boxes.

If you wanted to have a multiple number of problem instances per step, then set the "Instances per step" to the desired value.

It's important to know that the problems are created when the WinSAT starts solving them. Each problem is created after last one is solved, and the last one is discarded. If you wanted to save these problems as they are created, then place a check for the option, "Save instances to file as they are created."

Each of the files saved will have a prefix that you can assign. This can be done in the "File prefix" text box. Each problem saved will have the number of variables, clauses, and the problem instance preceded with the prefix. So if you had the prefix zzz, the number of variables 50, and the number of clauses 215, then the file name will be, "zzz_50_214_1."

You can also save the results after each search has the search has finished. Place a check on "Save result assignments after search." After each problem has been searched, the results of the search will be saved in zero and one format.

If you just wanted to create random CNF files just click on the "Create & Save Now" button, and the entire range of problems will be created and saved to the working directory. It's also important to know that if you run the search after you created and saved these problem, a new set of problems will be created for the search. If you wanted to test your search on the saved problems you would have to load them.

Search Methods

Once you have loaded the CNF file, or set your random problem parameters you can apply your selection of search methods, the number of initial assignments and the different settings of the search methods. Before you start searching a CNF file, make sure that the "Solve" option is set to the "CNF File" or "Random CNF". This option is set automatically to CNF file when you load a file.

There are currently 3 search methods you can choose form, and 2 search enhancers methods. The search methods that are found in this application are currently stochastic. Although they are incomplete methods, but they perform very well. The 3 search methods are Basic Hill-Climbing, GSAT, and WalkSAT. The search enhancers are K-Means clustering, and perturbations. The latter two must be included with other search methods for them to have any impact on the search.

To start your first search select the Basic Hill-Climb method from the drop down box, and click on "Start" button.

Notice that you have 10 initial assignments set in the "Initial assignments" text box. That means that the search will start applying Basic Hill-Climbing on the problem starting from 10 different initial assignments one at a time; it takes one assignment, apply the search method, and once it went through all the iterations, it will create another random assignment, and start the search again.

At any time during the search you can stop or pause the search. Just click on the "Stop" or "Pause" buttons to halt the search.

When you stop the search and restart it again, the search will restart from the beginning. The initial assignments will be re-initialized with random values, and the search will start with the first assignment and go through the rest of the assignments. On other hand, when you pause the search and resume it, the search will resume from the point it had stopped at.

Notice that there is a progress bar that shows how far the search has reached for the selected search method. This just show the number of iterations or bit flips that have already been carried.

The progress bar can be enabled or disabled if you wish. It is recommend that you turn off the progress bar if you notice that it is moving extremely fast especially if you are running WinSAT on a great deal of initial assignments, or problems, and you had set the number of iterations of the search method to a small number (will talk about the search methods settings later). If the progress bar is zipping through the search this could slow your search down. Otherwise, if you notice that the search method is moving slowly it is worth having it enabled. This way you will know how far you are in the search. You can enable or disable the progress bar even during the search.

Cascading Search Methods

One of the useful features of WinSAT is its ability to cascade search methods so that different method are applied to the problem in succession. You can start with a Basic Hill-Climber followed by WalkSat for example. Since, for example, the Basic Hill-Climber is fast in finding local solutions it is intuitive to use it first in the search. With it you can reach a plateau very quickly. Then you can apply WalkSAT, which has a random walk element, after the Basic Hill-Climber plateaus. More importantly you can start the with a search method on a large number of assignments, apply a search method, then apply K-Means clustering to resultant assignments, and finally apply another search method to the centroids obtained via K-Means. We will discuss the K-Means algorithm in the Search Enhancement section.

All you have to do to cascade methods is select the a method form each of the dropdown menus.

Once you have selected the methods you would like to apply to the search you can click start, and the search will start.

All at Once

One of the options that might not be obviously important is the option, "All at once." This option allows you to apply a particular search to all the assignments before going to the next search method. Although it might not be necessary to have this at all times, but it is enforced when K-Means is applied. K-Means clustering required all the assignments available to perform a clustering on them. Therefore, having a single assignment passed to K-Means is useless. This is the only case this option is set automatically to ensure all the assignments are available for processing. Otherwise, you can set this option if you wish to, but it is not necessary as I mentioned before.

Looping Through Search Methods

Suppose that you wanted to apply a search method such as GSAT or Basic Hill-Climbing, and then wanted to perturb the results so that your search would get unstuck from a local minimum. You then wanted to repeat the search again, and then perturb the results another time. You could cascade this process several times, but then you would only have 3 searches followed by 3 perturbations. Instead you can loop through your choice of search methods and perturbations using Loops. By default the number of loops assigned to each pair of search methods is 1. You can change that so that you can loop through your search methods as many times as you like.

Another way of using loops is to start with a Basic Hill-Climb with several hundred assignments, cluster the assignments, and then Hill-Climb again on the resulting centroids. This process could be repeated many times using loops.

Saving the results

We mentioned earlier how you can save solutions of problems after random problems had been searched. This does not apply to CNF files. If you place a check mark on the "Save result assignments after search" in the "Random Problems" section you will only save the results if the search was done on random problems. However, to save the results of a search performed on a CNF file you would have to explicitly do that using the "Save Results". Just go to the "File" menu, and choose "Save Results," specify the file name, and save.

Setting the Current Directory

We already mentioned saving results to files either automatically or through the file menu. You can set a current working directory so that all your files are saved to that directory. To do that, simply click on the folder icon in the "Current Directory" section.

This will open the directory structure on your current drive. Here you can select the drive and the directory. After that you can click on the "Open" button. This will change your current directory to the newly specified one.

Results Sheet

During or after running your search you can view the results of the search. The information that is stored in the results sheet includes the problem description, cost of each assignment, a link to open the CNF file, and a link to open the solution file. If you run WinSAT on several problem instances with different configurations you will be able to access each of the problem results through the results sheet. To open the results sheet go to the "Results" menu, and select "Results sheet."

An example of this sheet with a couple is as follows:

Notice that each 3 columns represent one problem instance. Each time the a new random instance is generated or the start button is pressed, a new set of columns is created to accommodate the solutions of this new random instance. However, when the problem is loaded from a CNF file, then the results sheet will apply the results to the sheet at the same location even if the search is re-started several times.

This sheet is updated after each search is applied to the assignment fully. Notice the open-file icons in the sheet. Use these to view the contents of the files. You can do that by double-clicking on the icons. If you click on the icon in front of the "Problem File" you will open the problem file:

If you double click on the in front of the solution file, then you will open the solution file. Notice that each line of the solution file contains a string of bits representing the assignment.

You can clear the sheet from all the results by choosing "Clear Results Sheet" from the "Results" menu. You can also have this done automatically by selecting the menu item "Clear Results On Start." This way the results sheet is cleared every time you click on the start button.

Search Enhancers

Search enhancers are methods that can be used in conjunction with search methods to enhance the search. Used by themselves they they might worsen results. Currently there are two search enhancers implemented. The first is the Perturbations, and the second is the K-Means Algorithm.

Perturbations is nothing more than flipping assignment bits at random. You can specify how many bits on average you want to flip, and Perturbations will randomly select bits at random and flips them. Perturbations help in getting unstuck in a local optimum. When that happens, flipping a bit at random, although might worsen results initially, on the long run might help improve results.

K-Means is entirely different. It is used for clustering. For our purposes when you have assignments that are similar or grouped in space, K-Means might be able to identify these groups and find their center points or centroids. This method has been shown to be effective in many areas such as image compression, classification, and so on. We have used this method in conjunction with Basic Hill-Climbing to get results that are far superior than results obtained by other stochastic methods.

The idea is to start a hill-climbing on several assignments, then use K-Means to cluster the groups and obtain their centroids, then apply another set of hill-climbs on the centroids to get better results. The best search Algorithm to use with K-Means is the Basic Hill-Climber since it can search through many assignments very quickly.

Search Settings

Each of the search methods has its own settings. You can set each of the search method settings by clicking on the "Settings button" next to the drop down menus.

To change settings you have to choose a search method from the drop down menu. After choosing the search method click on the "Settings" button. Will bring up the settings of search method you have chosen. Note that the settings of each of the methods in each of the drop down menus are maintained separately. So if you chose WalkSAT from the first drop down menu, and you changed its settings, then you changed it to GSAT, and changed its settings, and then you went back to WalkSAT the changes you have made will be available. Also, setting WalkSAT in one of the drop down menus does not affect WalkSAT settings in the other dropdown menus.

Basic Hill-Climbing Settings

Basic hill-climbing is based on the standard hillc-climber. It's very simple, fast, and can be superior to other search methods on m many problem instances. However, it does plateau fairly quickly. If you have a problem that you would like to hill-climb on extremely many times fast then it is recommended to try this method. You should try this method on your problem first anyway. Since it will give an indication of how hard your problem is.

The basic hill climber takes an initial assignment, pick a bit at random, flips it, and computes the cost (the number of unsatisfied clauses) of this new assignment. If the cost is less than or equal to the previous cost, then it keeps the new assignment. Otherwise, the the bit is unflipped. This process is repeated over and over again. There are only two things you can set with the Basic hill climber: the number of iterations, and exit criteria.

The number of iterations specifies the maximum number of bit-flips that the Basic Hill-Climber is allowed. The larger this number the longer it will take the hill climber to work with each assignment. Sometimes it is futile to set the iterations to a very large number since each assignment will be worked on for a very long time, and the Basic Hill-Climber might plateau long before the number of iterations is exhausted. However, if you set the number of iterations to a small number, then you might prematurely end the search even before plateauing. This when the exit criteria comes in.

The exist criteria allows the search to exit prematurely based on how long it's been since a decrease in cost. Place a check on "Exit prematurely," then select "Percent iterations" or "Iterations." After that assign a number to the "Exit after plateauing for." Suppose you set the value to 1000, and selected iterations, then WinSAT will check to see if 1000 iterations had passed since the last decrease in cost. If no changes occur for this 1000 iteration, the search will stop (or move on to the next search). If you select "Percent iterations," and assign 10 to the "Exist after plateauing for," then the program will exist if 10% of the iterations (in the "Number of iterations") had passed.

GSAT Settings

In GSAT, the settings are not much different than in the Basic Hill-Climber. Although, the search methods are different. The way GSAT works is described in the SAT and MAX-SAT for the Lay-Researcher page. Please read the section on Incomplete Methods, GSAT to understand the difference between the two search methods.

Due to the overhead of finding the next best move in GSAT, the search becomes much slower than the Basic Hill-Climber especially on large problems. In certain problems this gives GSAT the edge over Basic Hill-Climbing, but sometimes you can run the Basic Hill-Climber several hundred times in the time you can run GSAT even once. making the next best move in GSAT might result in avoiding making unnecessary sideway moves (might), but having many assignments tried quickly in Basic Hill-Climbing might result having one of the assignment successfully reaching the solution. It's a trade off.

With the GSAT settings, what is mentioned for the Basic Hill-Climber settings applies here exactly. Except the "Number of iterations" is changed to the "Number of flips." The difference is because in Basic Hill-Climbing WinSAT making flips and reversing them for each iteration. So each iteration does not necessarily end up with a flip. With GSAT every time a flip is made it is kept. Since the flip was arrived at after an exhaustive search through the neighbourhood.

WalkSAT Settings

WalkSAT build upon GSAT by introducing a random walk. This helps in escaping local minimums, and it has been shown to be a very effective method. Please SAT and MAX-SAT for the Lay-Researcher to understand how it works. It's available in the Incomplete Methods, WalkSAT section. In addition to being able to set maximum number of flips and the exit criteria, you can also set the probability of the random walk.

You can set the "Random walk probability" to a value between 0 and 1. If you set this value to 0, then the method becomes GSAT since it performs no random walks. If you set it to 1, then it will not apply GSAT, but it will basically apply a random walk. Any value in between will apply a random walk with the probability specified (p), and GSAT with a probability of 1-p.

Again, WalkSAT is very effective, but has the overhead of GSAT and the random walk.

Random Perturbations

Perturbations is a search enhancer. What is does is simple. It flips bits of an assignment at random. You can set the number of bits to flip on average using the Perturbations' settings.

You can set the number of bits to flip on average in each assignment. You can either specify the number of bits or the percent bits to flip of the total number of bits. If, for example, you set the number of bits to be 10, and you had 100 bits (or variables), 10 bits will be randomly and flipped. That means that a bit might be picked twice and flipped that means that it will be returned to its original state. That is why its 10 bits on average that are flipped.

K-Means Settings

As mentioned in the Search Enhancers section K-Means is method used to find the centroids of clusters of assignments. You can set how many centroids or clusters for K-Means to find, and what to do with the centroids and resultant assignments.

First, you can set the number of centroids you want to have by assigning either a value or a percent. So if you were working with 1000 assignments, and have set the number of centroids to 10, then K-Means will find 10 clusters and their centroids. If you set it to 10 percent, then it will find 100 clusters and centroids. You can do that in the "Centroids" section of the settings.

It's very important to know that when you start with 1000 initial assignments, and then use K-Means to find 10% centroids, the number of assignments will change in the "Initial assignments" text box to 100 after passing through K-Means. So if you decide to loop through Basic Hill-Climbing and K-Means bare in mind that the number of assignments will decrease until it reaches 1. Then it makes no sense to cluster using K-Means anymore. That's when you can use diversification to create more assignments from the centroids. You can also keep replace the worst assignments with the centroids. That should replenish your supply of assignments.

In the assignment control section, you can specify how you would like WinSAT deal with the centroids. Before describing Assignment control lets describe how the centroids are obtained in a cluster. Suppose K-Means grouped the following assignments into a single cluster:

1000011111001
1100001111101
1000011100101
1000011110000
1100001110001

Then the number centroid can be obtained by the sum of each bit of across each assignment and dividing by the number of assignments. Basically, you are obtaining the average of the cluster. This is what you would get:

1   0.4   0   0   0   0.6   1   0.8   0.4   0.4   0   0.8

These are real numbers. If you choose "Keep only centroids (discard all assignments)," then the initial assignments used in finding the clusters, and the centroids are rounded off to the nearest 0 or 1, and kept for the next search. So the above centroids would become:

100001110001

If the second choice was picked, "Diversify results using centroids by creating," this will consider each of the real values in the centroids as a probability of being a 1 or a 0. That is to say that the first bit of the new assignment will be a 1 probability 1, and the second bit of the assignment will be a 1 with probability of 0.4, and so on. Further more, the number of assignments created will based on the number you specify. If you had 10 centroids, and you wanted to create 500 new assignments based on the probability scheme, then each centroid will be used to create 50 assignments.

In addition to that, we having the mapping of the probabilities, the sigmoidal function below:

Suppose we had the following centroid:

0.2   0.1   .45   .12   0   0.6   1   0.8   0.9   0.1   0   0.85

You know that the first bit will be a 1 with a probability 0.2, and second bit with a probability of 0.1. That means that it is likely that these bits will be set to 0 which is reasonable. It's the opposite for 0.8, 0.85 and 0.9. They will most likely become 1s. The values such as 0.45 and .6 are closer to the center and the have a sort of 50-50 chance of becoming either a 0 or a 1. What if you wanted to give the lower and higher values more emphasis so that they almost certainly become 0s or 1s, and the values in the middle still have the same sort of chance of becoming as they did before. To do that you can adjust the slider below the graph to accomplish this.

Currently this mostly visual. Notice that in the above graph any probability that is less than 0.3 is certain to become a zero, and anything that is above 0.7 is also certain to become a 1. Anything in between is spread between 0 and 1.

What this diversification does is that operation does is it creates many more new assignments that are based on centroids. This is sort of like focusing with K-Means an Defocusing with the diversification.

Parameter Settings

Once you have set all the different search parameters you can save them as an XML file. All your settings including the "Random Problem" section parameters, the number of initial assignments, the search methods, the settings of the search methods and the working directory for these settings will be saved in this XML file. You can later load these settings instead of resetting them manually.

This way you can design different search schemes, and store or load each scheme, and compare the results of the different schemes.

Download WinSat v2.04 (May 30th, 2009)

Version 2.04 of WinSat bug fixes

• Clearing the sheet while running the search crashed WinSat. Clearing sheet is disabled while running
• In GSAT, the search wouldn't stop if the search reached unsat = 0. Now it stops.
• Pause button icon shows resume icon if clicked more than once.
• Elapsed time issues with regards to the pause and stop buttons.

Version 2.0 features, enhancements and bug fixes.

Enhancements

We have improved on the speeds of GSAT and WalkSat immensely. The speeds are no longer hampered by the size of the problem as much as before. The current implementation of GSAT and WalkSat might be the fastest ever. We have compared WinSat against UBCSAT (which is a great program with a plethora of algorithms), and found that for large problems specifically WinSat can perform approximately an order of magnitude more flips than UBCSAT in the same amount of time. We will be posting the restults soon.

New features

• Elapsed time: the elapsed time will be incremented every second on the control panel below the progress bar. In addition, it will be reported in the results sheet.
• Last effective flip: a new column to the right of the Current cost column will report the last effective flip. So if you set your WalkSat to 100,000,000 flips and run WinSat not every flip will decrease the cost (reduce the number of satisfied clauses). Some flips will increase it, others will decrease it, and some will not change the cost. Only when the cost is decreased will that flip will be recorded. This way you will know that out of 100,000,000 when the search plateaued.

Bug fixes

• Previously, the Results sheet displayed the ratio and the number of clauses as 0 when a cnf file was loaded, and tested. This has been corrected.
• Previously, when WinSat was run on a cnf file then every simulation (every time you click the start button) was recorded in the same place in the Results sheet. Now, every simulation is recorded in a new column. This was done so you can run multiple simulations on the same problem, and have the results of all simulations available. This is wasn't a bug, but I thought I'd change it anyway

Download and install WinSAT. This application works on Windows XP and Vista. Although, I haven't tried it on Windows 2000 but I believe that it should work there too. Included with the application is are a few sample CNF files.

If you would like to be notified of any updates to WinSat, then please leave your email.

If you have any problems with WinSAT or would like to report a bug, please send me an email at:

Dr. Mohamed Qasem mqasem@gmail.com

Back to the home page

This page has been visited 19421 times.