Galo's Home Page

MinSAT is a research topic not broadly studied. It is an interesting problem because is the minimization of SAT and is a NP-Hard problem. More important it has great impact in the work done to build WalkMINQBF because it helps in the creation of a subformula that will help in getting an UNSAT answer for the QBF Solver we built.

Learning about minsat was not an easy task. Since there are not many papers about it the most logic way of understanding the problem was reading about MaxSAT. MaxSAT gave us some ideas about how to build a MinSAT solver.

Complete Minsat

Before attempting to build a minsat solver that was quick and useful for our purposes I built a complete minsat solver that uses enumeration to try all the existent solutions searching for the minsat optimal value. As expected this solver was easy to build and of course only gave me some better understanding of the minsat problem because after adding more than 15 variables it becomes a very slow solution. (Sometimes, I also used it as a tool to verify the job done by the incomplete algorithm done for the WalkMINQBF algorithm)

Building WalkMINSAT

We decided to use WalkSAT as a template to build an efficient MINSAT solver. WalkSAT was studied and used as an easy way to create a stochastic local search method needed to build WalkMINQBF. The data structures and the way it iterates through the clauses and variables were ideal to create a quick and incomplete MINSAT solver without worrying about the design of the data structures to hold the information.

WalkSAT is a very efficient code that uses a lot of programming tricks to be fast. After understanding some of the arrays and variables used to create a SAT solution we modified the behavior so the solver instead of searching to maximize the number of SAT clauses it began to minimize them. After changing the meaning of what a good answer is (instead of looking for the maximum number of SAT clauses we look for the minimum) we added some new heuristics to the code.

The most important data structures and functions from the original walkSAT are described below. Then I will explain the main modifications done to convert the walkSAT code into walkMINSAT.

To explain each data structure we will use the following figure so we can easily understand the components that WalkSAT uses to solve a SAT formula.

In the figure we can see the following data structures that are filled when a sat formula is parsed.

Clauses	Keeps the information of all the clauses of the SAT formula
Numoccurences	Shows the number of clauses where each literal can be find
Occurrence	Shows the clause number where each literal is found. It is related to numoccurences because it will have exactly the same amount of numbers as the sum of the values of numoccurences

Using the above data structures, the algorithm is capable of iterate through the clauses where the value of the variables have been modified instead of searching in the complete set of clauses. It is a very clever way to prove the satisfiability of the problem without having to run through the m number of clauses.

The following figure will show some dynamic data structures used by the heuristics to decide which is the best way of moving through the search space.

Atom	Keeps the actual value given to a variable. If 1 it is –var if 0 it is +var
Breakcount	Keeps the information of the number of clauses that will become UNSAT if the variable of the index is flipped. (i.e. in the figure if we change the variable 2 only one clause will become UNSAT)
Makecount	Similar to Breakcount but it counts the number of SAT clauses

Breakcount and Makecount are used to decide which the best variable to flip is. In general they provide very useful information to make good decisions about how to flip variables. They are used by the heuristics to decide which is the best variable to flip.

Additionally to the data structures from above, WalkSAT relies on two special arrays that help to make the algorithm faster. The False and WhereFalse arrays are used to quickly modify the information hold about the clauses that are modified when a flip is done. They are very useful to avoid the need of iterating through all the clauses to make the modifications to the makecount and breakcount of the variables.

False	Holds the clauses that are false at this time given the actual assignment of the atom array.
WhereFalse	This array helps to identify where the given clause is in the false array. It is useful because using it you can know which clauses are still false on the formula and have to be considered by the heuristics. In other words, it is a dictionary used to obtain the position of a clause in the false array.

To solve the MINSAT problem we added the following data structures based on the idea and spirit of the false array of the WalkSAT algorithm:

Numtruelit	It holds the number of true literals each clause holds. It depends on the current assignment given to atom. For example if there is a clause like: and the current assignment is the value of numtruelit for this clause will be 2 because of the value of and
Onetrue	This array holds the clauses that have 1 as its value in the numtruelit.
True	It contains the clauses that are true. It means that the numtruelit value of the clauses on this array is more than or equals to 1.
Whereonetrue	It identifies where a given clause can be find in the onetrue array. It is useful because it is used to identified which clauses have only onetruelit without having to iterate through them
WhereTrue	As with wherefalse from WalkSAT it helps to know the clauses that are still true in the formula. It gives you a way to access them without iterating through all.

As we can see from all the data structures explained we can see that the algorithm has a complete control of the clauses and the relation between them and the variables. One of the main advantages of the WalkSAT algorithm is the capacity to update the information of the clauses without iterating through all the clauses so we used the same structure but using the true literals instead of the false information.

The algorithm that the minsat method uses (as described on the paper written by Yannet Interian, Gabriel Corvera and Bart Selman) is the following:

The algorithm will try to follow the same idea of the WalkSAT algorithm. It begins with a random assignment to the variables of the formula then it will chose one to flip using a given heuristic defined on the algorithm as ChooseVar if it finds a better assignment (one with less satisfied clauses) it will save it and continue trying to find a better assignment until the number of steps ends.

After creting the structures we have to decide how to choose the variable to flip. Those heuristics were easily added because WalkSAT has a very easy way to add heuristics. So we decided to begin to test some ideas of how to minimize random SAT problems in an efficient and quick way. As stated by the paper we began using a heuristic named WORST similar to one found in WalkSAT until we created the Mixed_Balance which is based on the creation of a score called Balance.

Random	It picks a variable to flip completely at random.
Worst	With probability p selects the variable that is true in a random clause selected from the one_true array and then flips the value of the variable. (one_true array holds the clauses that have only one literal true and because of it the clause is still SAT). With probability 1-p it just selects one at random.
Balance	Calculates the balance score of certain number of clauses selected at random from the one_true array and then selects the true variable from the clause with the best score.
Mixed	Mixes the balance heuristic with the worst heuristic selecting to use each heuristic given a certain probability of mixture.
Mixed_2	Creates an array with the variables that have the worst makecount (number of clauses that will be SAT if flipped) and then selects the variable with the best balance score.
Mixed_Block	At the initialization of each try certain variables are given a random value and are block. The heuristic acts as balance but ignoring the blocked variables.
Best_and_Second	Creates a best and second array where the variables with the best and second makecount (number of clauses that will be SAT if flipped) are stored and then it selects the variable with the best balance score from the two arrays.
Mixed_Balance	This is the chosen heuristic used as part of the WalkMINQBF solver. It mixes the Best And Second Heuristic with the Mixed_2 heuristic using certain noise.

We know that minimizing the universal part of the formula we will get sub-formulas with higher density that at the same time will have more chances of been UNSAT. The balance score used by mixed_balance and balance is useful to determine which clauses and variables will help to get a higher density and then get more UNSAT sub-formulas.

After testing each heuristic with different parameters we decided to use the mixed_balance heuristic for the WalkMINQBF algorithm because it has the properties we needed:

Some tests run on the different heuristics also show why the Mixed Balance heuristics was selected over the others. The following chart shows the number of QBF formulas each heuristic helped to solve once integrated with the QBF solver.

The main difference between the three heuristics was that the Mixed_Balance takes into consideration the properties of the variables and clauses and not just selects the variables at random as Random or Worst does.

As the chart shows, Mixed_Balance is quicker on solving the QBF problems and also it does it better than the other 2 heuristics.

Additionally, the mixed_balance was the only heuristic that gave us UNSAT sub-formulas closer to ratios between 3.8 and 4.0 meaning that those sub-formulas are better because there are more likely UNSAT.

To define quickly the best balance score of a formula when a change was going to be done, we defined the function d_balance. With this function we calculate the difference in the balance score of the formula so we can understand how the formula will move on through finding the minsat assignment when choosing certain variable to be flipped.

The implementation of d_balance only visits the modified variables on the modified clauses to calculate the value instead of looking at all the clauses.

Complete WalkMINSAT and more Heuristics

The WalkMINQBF algorithm does not needs a complete Minsat algorithm because it needs several solutions approximated to the minimal value so it can try to prove UNSAT on each. After working with WalkMINQBF I decided to complete the MINSAT Solver using the same ideas that are described for MAXSAT in the paper written by Borchers.

Borchers uses WalkSAT to get a good approximation of a solution that satisfies the MAXSAT problem (get the maximum number of satisfied clauses). After running the local search it tries to search through all the solutions to find the optimum solution using the value got from WalkSAT as a way to cut the tree.

As I already have the MinSAT local search done the only part I added to the algorithm was the complete branch and bound algorithm. The whole idea was to use the value obtained from the MinSAT local search to cut the search tree. As happens with a complete MAXSAT solver, the complete MinSAT solver is not very efficient, but when solving small problems it shows that the local search answer is very accurate. I played with some other heuristics described below to try the efficiency of some of them and I got different results from creating new heuristics and running them in a complete search.

MinSAT & WalkSAT

Complete Minsat

Building WalkMINSAT

Complete WalkMINSAT and more Heuristics

Downloads