The Satisfiability problem (SAT) is a famous NP-Complete problem, which consists of an assignment of Boolean variables (true or false) and some clauses formed of these variables. A clause is a disjunction of some Boolean literals and can be true if and only if any of them is true. A SAT instance is satisfied if and only if all the clauses are simultaneously true. As a generalization of SAT, the Maximum Satisfiability problem (MAX-SAT) aims to maximize the number of satisfied clauses. When every clause is associated with some weight, the MAX-SAT turns to the weighted Maximum Satisfiability problem (weighted MAX-SAT) with numerous applications arising in artificial intelligence, such as scheduling, data mining, pattern recognition, and automatic reasoning. According to the computational complexity theory, there’s no polynomial time algorithm for solving weighted MAX-SAT unless . Hence, many heuristic algorithms capable of finding near optimal solutions in reasonable time have been proposed for weighted MAX-SAT, including GSAT, GLS, Taboo Scatter Search, ACO, and GRASP/GRASP with path-relinking.
As an efficient tool for heuristic design, the backbone has attracted great attention from the society of artificial intelligence in recent years. The backbone is defined as the common parts of all optimal solutions for an instance. Since it’s usually intractable to obtain the exact backbone, many approximate backbone guided heuristics have been developed for NP-Complete problems, including 3-SAT, TSP, QAP, et al. For SAT or MAX-SAT, some character and algorithms of backbone are in research. And a BGWalksat (backbone guided local search algorithm with Walksat operator) has been developed for MAX-SAT and achieves better performance than existing heuristics. However, as to our knowledge, there is no theoretical result or backbone guided heuristics reported in the literature for weighted MAX-SAT.
In this chapter we investigated the computational complexity of the backbone for weighted MAX-SAT and developed a backbone guided local search (BGLS) algorithm. Firstly, we proved that there’s no polynomial time algorithm to retrieve the full backbone under the assumption that . In the proof, we mapped any weighted MAX-SAT instance to a biased weighted MAX-SAT instance with a unique optimal solution by slightly perturbing, which is also optimal to the original instance. Based on this proof, we indicated that it’s also intractable to retrieve a fixed fraction of the backbone, by reducing any weighted MAX-SAT instance to a series of weighted MAX-SAT instances with smaller scale. Secondly, we developed a backbone guided local search algorithm with pseudo-backbone frequencies. It consists of two phases: the sampling phase records local optima to compute pseudo-backbone frequencies and the backbone phase uses such information to guide the following local search. Experimental results demonstrated that BGLS obtained better solutions than GRASP/ GRASP with path-relinking in far less time.
In this section, we shall give some definitions and related properties.
Definition 1. Given a set of Boolean variables , a propositional formula is a conjunction on a set of clauses . Each clause is a disjunction of literals, where each literal is either a variable or its negation. A clause is satisfied if at least one of its literals evaluates to true, and the propositional formula is said to be satisfied if all of its clauses are satisfied. The satisfiability problem (SAT) aims to find an assignment of values to the variables such that a given propositional formula is satisfied. Formally, a SAT instance on the set of Boolean variables and the set of clauses can be denoted as .
Definition 2. Given a set of Boolean variables , a propositional weighted formula is a conjunction on a set of weighted clauses . Each weighted clause is associated with a positive weight . The weighted maximum satisfiability problem (weighted MAX-SAT) consists of finding an assignment of values to the variables such that the sum of the weights of the satisfied clauses is maximized. Similar to the SAT, a weighted MAX-SAT instance can be denoted as and a solution (assignment) can be denoted as
with cost function , where =1 (0) for being true (false).
Without loss of generality, we shall assume in the following part of this paper, that the weight is a positive integer for each clause .
Definition 3. Given a weighted MAX-SAT instance , let be the set of all optimal solutions to it, where represents the number of optimal solutions. Backbone in weighted MAX-SAT instance is defined as .
The backbone is essential for heuristic algorithms design, since a heuristic cannot obtain an optimal solution to a weighted MAX-SAT instance unless it retrieves the full backbone. In contrast, if the backbone is retrieved, the search space could then be effectively reduced by assigning literals in the backbone to true.
In Definition 4, we shall introduce the definition of the biased weighted MAX-SAT instance, which will be used in the following proof.
Definition 4. Given a weighted MAX-SAT instance , the biased weighted MAX-SAT instance is defined as , where and the weight associated with every clause is defined as follows.
Given a weighted MAX-SAT instance, it is easy to verify that the following property holds: .
3. Computational complexity for backbone
3.1. Weighted MAX-SAT and biased weighted MAX-SAT
In this section, we shall investigate the relationship between the solution of a weighted MAX-SAT instance and that of the biased weighted MAX-SAT instance in Lemma 1 and Lemma 2.
Lemma 1. Given the set of Boolean variables and the set of weighted clauses , there exists a unique optimal solution to the biased weighted MAX-SAT instance .
Proof. Given any two distinct solutions , to the biased weighted MAX-SAT instance , we will show that .
Firstly, we construct a weighted MAX-SAT instance where for . We have that.
Since the weight is a positive integer for each clause , thus must be the integer part of and must be the fractional part of . Similarly, must be also the fractional part of . By assumption that , there must exist a variable such that and . In the following proof, we only consider the case that , . For the case that and , it can be proved in a similar way.
Obviously, the clause can be satisfied by , while it cannot be satisfied by . When viewed as binary encoded strings, the th bit of the fractional part of will be 1, however the same bit of will be 0. Hence, we have that .
Thus, this lemma is proved.
Lemma 2. Given the set of Boolean variables and the set of weighted clauses , if is the unique optimal solution to the biased weighted MAX-SAT instance , then is also optimal to weighted MAX-SAT instance .
Proof. Otherwise, there must exist a solution to the such that . By assumption that the weight is a positive integer for each clause , thus we have . Since , we have that . Similarly, . It implies that , which contradicts with the assumption that is the unique optimal solution to the . Thus, this lemma is proved.
3.2. Computational complexity for retrieving backbone
In Theorem 1, we shall show the intractability for retrieving the full backbone in weighted MAX-SAT. In addition, we shall present a stronger analytical result in Theorem 2 that it’s NP-hard to retrieve a fixed fraction of the backbone.
Theorem 1. There exists no polynomial time algorithm to retrieve the backbone in weighted MAX-SAT unless .
Proof. Otherwise, there must exist an algorithm denoted by which is able to retrieve the backbone in weighted MAX-SAT in polynomial time.
Given any arbitrary weighted MAX-SAT instance , the biased weighted MAX-SAT instance can be constructed by an algorithm denoted by in time.
Since the is also a weighted MAX-SAT instance, its backbone can be computed by in polynomial time (denoted by). By Lemma 1, the backbone is the unique optimal solution to the . By Lemm2, the is an optimal solution to the as well.
Hence, any weighted MAX-SAT instance can be exactly solved in time by and . Obviously, such conclusion contradicts with the result that weighted MAX-SAT is NP-hard. Thus, this theorem is proved.
Theorem 2. There exists no polynomial time algorithm to retrieve a fixed fraction of the backbone in weighted MAX-SAT unless .
Proof. Otherwise, given any weighted MAX-SAT instance , we can always construct a biased weighted MAX-SAT instance according to Definition 4. As proven in Theorem 1, the backbone is an optimal solution to the .
If there exists a polynomial time algorithm to retrieve a fixed fraction of the backbone, we can acquire at least one literal in the . In the following proof, we only consider the case that ( ). For the case that ( ), it can be proved in a similar way.Let be the set of those clauses containing , let be the set of the remaining parts of the clauses from after deleting . Since , we can construct a new smaller weighted MAX-SAT instance , where .
By repeating such procedures, an optimal solution to can be finally obtained literal by literal in polynomial time, a contradiction. Hence, this theorem is proven.
4. Backbone guided local search
4.1. Framework of backbone guided local search
In this section, we shall present the framework of backbone guided local search (BGLS) for weighted MAX-SAT. In BGSL, the local search process is guided by the backbone frequency, a group of probabilities representing the times of solution elements appearing in global optima. Since it’s NP-hard to retrieve the exact backbone, we shall use the pseudo-backbone frequency instead, which can be computed by the approximate backbone (the common parts of local optima).
The framework of BGLS consists of two phases. The first phase (sampling phase) collects the pseudo-backbone frequencies with traditional local search and the second one (backbone phase) obtains a solution with a backbone guided local search. Every run of local search is called a try. Each of two phases uses an input parameter to control the maximum tries of local search (see Algorithm 1).
Algorithm 1: BGLS for weighted MAX-SAT
Input: weighted MAX-SAT instance , , , a local search algorithm
2. for to do
2.1 obtain a solution with ;
2.2 sample backbone from ;
2.3 if then ;
3. for to do
3.1 obtain a solution with backbone guided ;
3.2 if then ;
4. return ;End
Both of the two phases use the same local search algorithm. However, in the sampling phase, a particular step is used to sample backbone information from local optima. And the backbone phase uses this sampling to guide the following local search. Although many local search algorithms can be used as the algorithm in Algorithm 1, we proposed an improved Walksat in practice which is originally designed for MAX-SAT. Thus, some necessary modifications should be conducted for adapting it to weighted MAX-SAT.
4.2. Walksat for weighted MAX-SAT
In Algorithm 2, we shall present the Walksat for weighted MAX-SAT. In contrast to Walksat for MAX-SAT, some greedy strategies have been added to Algorithm 2 to fit weighted MAX-SAT. A try of Walksat needs two parameters. One is maximum number of flips that change the value of variables from true to false or inversely. The process of Walksat seeks repeatedly for a variable and flips it. When a variable is flipped, its break-count is defined as the number of satisfied clauses becoming unsatisfied. Obviously, the value of break-count will be nonnegative. And a variable with a zero break-count means the solution will be no worse than that before flipping. The other parameter is the probability for noise pick, which is used for determining when to use noise pick.
The Walksat for weighted MAX-SAT works as follows. After an initial assignment is generated by random values, Walksat picks a clause (clause pick) from one of the unsatisfied clauses with maximum weight randomly. Then the algorithm flips one of variables of this clause under the following rules: if there’re more than one variable of zero break-count, then flip one of them randomly, otherwise flip any of variables randomly with the probability parameter (noise pick). For the case that the probability is not satisfied, pick one variable with least break-count randomly (greedy pick). Because the diversity of solutions depends on the parameter for noise pick and the static setting of it cannot react to the solving process. So we choose a dynamic noise setting strategy (step 2.6) to set the parameter for noise pick: if the solution quality decreases, the noise parameter will increase to , otherwise will decrease to , where is a predefined constant number.
In summary, there’re five random actions (in step 1, 2.1, 2.3, respectively) during the whole process of the Walksat for weighted MAX-SAT. And we’ll modify them in the backbone phase of BGLS (see Section 4.4).
Algorithm 2: Walksat for weighted MAX-SAT
Input: weighted MAX-SAT instance , , a probability for noise pick
1. let be a random assignment of variables of , ;
2. for to do
2.1 pick , as one of the unsatisfied clauses with maximal weight, randomly;
2.2 compute the break-count of all variables in ;
2.3 if a zero break-count exists
then pick one variable of zero break-count in , randomly;
else with a probability , pick one of all variables in , randomly;
and with a probability , pick one variable of least break-count ones in , randomly;
2.4 flip this variable and obtain solution ;
2.5 if then ;
2.6 adjust the value of ;
3. return ;
4.3. Pseudo-backbone frequencies sampling
Given a particular problem instance, the exact difference between local optima and global optima cannot be exactly predicted unless those solutions are found, due to the diversity of instances. In this subsection, we analyze some typical instances to investigate the difference. The distance between local optima and global optima is defined as the number of different value of variables. For comparison among different instances, this distance is normalized by the total number of variables.
The sampling algorithm for local optima is Walksat for weighted MAX-SAT, where maximum of flips is set to be 200 and the noise probability is set to be 0. For every instance, the sampling algorithm was run for 50 times and 50 local optima were generated. Fig. 1 shows the distances between local optima and global optima for four instances. The weight of solutions is plotted against the normalized distances to global optima. From Fig. 1, we can draw the conclusion that all the normalized distances between local optima and the global optimum are between 0.4 and 0.8. It implies that local optima and global optima have common values for most of variables. Thus, some approximate backbone can be retrieved to guide local search to find better solutions.
Furthermore, we recorded the number of every variable value in local optima and a probability of true or false being chosen for every variable can be computed. For every instance, we tested whether the variables in global optima tend to take the value with higher probability. And we found that more than 70% (74% for jnh1, 70% for jnh7, 73% for jnh209, and 73% for jnh210, respectively) of all variables in global optima take the values (true or false) with higher probabilities appearing in the local optima. It implies that a priority set of values can be made of those values with higher probability.
To guide the Walksat for weighted MAX-SAT, two forms of information should be recorded to construct the pseudo-backbone frequencies: the frequencies of variables and the frequencies of clauses. After obtaining any local optimum, the pseudo-backbone frequencies are updated. On one hand, the frequencies of variables record the times of the variable value appearing in local optima. On the other hand, the frequencies of clauses record the times of clauses being satisfied. The pseudo-backbone frequencies will be computed in the sampling phase (see Step 2.2 of Algorithm 1).
4.4. Backbone guided walksat for weighted MAX-SAT
As discussed in Section 3.2, there’re five random actions in the Walksat. Instead of the traditional random choosing, we shall determine the variable values by the pseudo-backbone frequencies (see Algorithm 3).
Algorithm 3: Backbone guided Walksat for weighted MAX-SAT
Input: weighted MAX-SAT instance , , a probability for noise pick , pseudo-backbone frequencies
1. let be a random assignment of variables of , guided by , ;
2. for to do
2.1 pick from as one of the unsatisfied clauses with maximum weight, guided by ;
2.2 compute the break-count of all variables in ;
2.3 if a zero break-count exists
then pick one variable of zero break-count ones in randomly, guided by ;
else with a probability , pick one of all variables in randomly, guided by ; and with a probability , pick one variable of least break-count ones in , guided by ;
2.4 flip this variable and obtain solution ;
2.5 if then ;
2.6 adjust the value of ;
3. return ;
The first random action is an initial assignment generation in Step 1 of Algorithm 3. An initial value of a variable can be guided by the frequencies of the values. The second random is in Step 2.1. In pseudo-backbone, the frequencies of clauses satisfied in local optima have been recorded. According to this, the probability of each clause being satisfied can be computed to direct which clause should be firstly satisfied. And then Step 2.3 includes three remaining random choices. These three choices are similarly guided by the same approximate backbone as the first random and the probabilities will be computed under the same method as the second random.
5. Experimental results
In this section, we presented the experimental results for BGLS over weighted MAX-SAT benchmark. All the codes are implemented and compiled in C++ under a Pentium IV D 2.8GHz with 1GB memory. In the algorithm 1, 2 and 3, we have indicated 4 input parameters (the tries and maximum flips of two phases, respectively). In this experiment, we use identical parameters for both phases with 50 tries and 400 flips.
Since the best heuristics (GRASP/GRASP with path-relinking) for weighted MAX-SAT are tested on distinct experimental platforms, we conducted a system performance conversion according to SPEC. The system of GRASP with path-relinking is more than 15.69 times faster than ours (see Appendix) and only some of the instances’ running time is available. Since there’s no platform of R4400 in SPEC, we give no running time of GRASP on PD2.8G.
The problem instances of weighted MAX-SAT in the experiments include 44 instances, each of which has 100 variables and 800, 850 or 900 clauses, respectively. Tab. 1 shows the results of our experiments and the comparison with other algorithms. The column “Instance” indicates the input instances of benchmark and the column “Optima” shows the weight of global optima of instances. The following three columns “GRASP”, “GRASP with path-relinking” and “BGLS” show the performance and results of the three algorithms, respectively. Each of them has sub-columns “weight” (the maximum weight obtained) and “time” (the time of running) for reporting the details. And the last column “Improvement” means the improvement of BGLS over GRASP, which is computed through dividing difference between the weight of BGLS and GRASP by the weight of global optima. A positive value means BGLS can obtain a better solution than GRASP, and vice verse.
From Tab.2, BGLS is more efficient than GRASP for nearly all the instances except instance “jnh208”. The average of improvement is 0.0369%. For 19 instances out of 44, BGLS can always get global optima, however GRASP can get global optima for only 4 instances. And BGLS uses far less time than GRASP with path-relinking.
In this chapter, analytical results on the backbone in weighted MAX-SAT were presented in this paper. We showed that it is intractable to retrieve the backbone in weighted MAX-SAT with any performance guarantee under the assumption that . And a backbone guided local search algorithm was proposed for weighted MAX-SAT.
Results of this paper imply a new way to incorporate the backbone in heuristics. The approximate backbone used to guide the flipping of literals in those local search based heuristics. However, a multilevel strategy was introduced in the proof of Theorem 2. According to the proof, a new smaller weighted MAX-SAT instance could be constructed after a literal being fixed. By such a way, we can gradually reduce the original weighted MAX-SAT instance to a series of weighted MAX-SAT instances with less variables and clauses. Conversely, the solution to the original instance could be reconstructed with solutions of those reduced weighted MAX-SAT instances and fixed literals.
Many local search operators can apply on the BGLS for adapting with different problems. For weighted MAX-SAT, we used an improved Walksat to obtain local optima. Related to the common local search, BGLS heavily depends on the backbone sampled to simplify the scale of problems and to intensify local search. The process of retrieving backbone is to collect the feature from local optima. A note to design the similar algorithm is that a backbone guided algorithm can work well if and only if the local optima and the global optimum have the certain common parts.
In the future work, some interesting things remain to be investigated. Firstly, it needs further work on computational complexity for retrieving the backbone in the SAT. Although weighted MAX-SAT is a generalization of the SAT, it is not straightforward to prove the NP-hardness of retrieving the backbone in the SAT. The difficulty lies on the fact that the SAT isn’t an optimization problem like weighted MAX-SAT but a typical combinatorial problem instead. For weighted MAX-SAT, we can always construct a weighted MAX-SAT instance with a unique optimal solution (i.e., the backbone) by slightly perturbing. However, such a method could not be directly applied to the SAT. Secondly, the ways for approximating the backbone are to be further explored. The backbone was approximated by the common parts of local optimal solutions. However, we argue that there may exist better ways for approximating the backbone in weighted MAX-SAT. A good example of approximating the backbone by novel ways can be found in the traveling salesman problem (TSP). They proposed four strategies for approximating the backbone other than by the common parts of local optimal solutions: Minimum Spanning Tree, Nearest Neighbor, Lighter Than Median, and Close Pairs. By those new strategies, they claimed that very large TSP instances can be tackled with current state-of-the-art evolutionary local search heuristics. Inspired by their work, we shall approximate the backbone in weighted MAX-SAT in the future, by some similar methods which are generally exploited by exact algorithms.