Open access peer-reviewed chapter

Backbone Guided Local Search for the Weighted Maximum Satisfiability Problem

By He Jiang and Jifeng Xuan

Published: October 1st 2009

DOI: 10.5772/9610

Downloaded: 1110

1. Introduction

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 unlessP=NP. 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 thatPNP. 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.

2. Preliminaries

In this section, we shall give some definitions and related properties.

Definition 1. Given a set of Boolean variablesV={x1,x2.,xn}, a propositional formulaϕis a conjunction on a set ofmclausesC={C1,C2.,Cm}. Each clauseCiis a disjunction of|Ci|literals, where each literallijis 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 variablesVand the set of clausesCcan be denoted asSAT(V,C).

Definition 2. Given a set of Boolean variablesV={x1,x2.,xn}, a propositional weighted formulaϕis a conjunction on a set ofmweighted clausesC={C1,C2.,Cm}. Each weighted clause is associated with a positive weightw(C˜i). 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 aswMAXSAT(V,C)and a solution (assignment) can be denoted as

s={xi|xiis  assigned  true}{xi|xiis  assigned  fales}

with cost functionw(V,C˜,s)=C˜iC˜w(C˜i)[C˜i is satified by s], where[]=1 (0) forbeing true (false).

Without loss of generality, we shall assume in the following part of this paper, that the weightw(C˜i)is a positive integer for each clauseC˜i.

Definition 3. Given a weighted MAX-SAT instancewMAXSAT(V,C), letΠ*={s1*,s2*,...,sq*}be the set of all optimal solutions to it, whereq=|Π*|represents the number of optimal solutions. Backbone in weighted MAX-SAT instancewMAXSAT(V,C)is defined asbone(V,C˜)=s1*s2*sq*.

The backbonebone(V,C˜)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 backbonebone(V,C˜)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 instancewMAXSAT(V,C˜), the biased weighted MAX-SAT instance is defined aswMAXSAT(V,C), whereC¯=C˜{xi,¬xi|xiV}and the weight associated with every clauseC¯iC¯is defined as follows.

  1. w¯(C¯i)=w(C¯i) C¯iC˜  C¯i{xj,¬xj|xjV}
  2. w¯(C¯i)=w(C¯i)+1/22j C¯i=xjC˜,xjV
  3. w¯(C¯i)=w(C¯i)+1/22j+1 C¯i=¬xjC˜,xjV
  4. w¯(C¯i)=1/22j C¯i=xjC˜,xjV
  5. w¯(C¯i)=1/22j+1 C¯i=¬xjC˜,xjV

Given a weighted MAX-SAT instance, it is easy to verify that the following property holds:C¯iC¯w¯(C¯i)=C˜iC˜w(C˜i)+1/22+1/23++1/22n+1=C˜iC˜w(C˜i)+1/21/22n+1.

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 variablesVand the set of weighted clausesC˜, there exists a unique optimal solution to the biased weighted MAX-SAT instancewMAXSAT(V,C).

Proof. Given any two distinct solutionss1,s2to the biased weighted MAX-SAT instancewMAXSAT(V,C¯), we will show thatw(V,C¯,s1)w(V,C¯,s2).

Firstly, we construct a weighted MAX-SAT instancewMAXSAT(V,{xi,¬xi|xiV})wherew(xi)=1/22i,w(¬xi)=1/22i+1forxiV. We have that

w(V,C¯,s1)=w(V,C˜,s1)+w(V,{xi,¬xi|xiV},s1).

Since the weightw(C˜i)is a positive integer for each clauseC˜iC˜, thusw(V,C˜,s1)must be the integer part ofw(V,C¯,s1)andw(V,{xi,¬xi|xiV},s1)must be the fractional part ofw(V,C¯,s1). Similarly,w(V,{xi,¬xi|xiV},s2)must be also the fractional part ofw(V,C¯,s2). By assumption thats1s2, there must exist a variablexjVsuch thatxjs1s2andxjs1s2. In the following proof, we only consider the case thatxjs1,¬xjs2. For the case that¬xjs1andxjs2, it can be proved in a similar way.

Obviously, the clausexjcan be satisfied bys1, while it cannot be satisfied bys2. When viewed as binary encoded strings, the2jth bit of the fractional part ofw(V,C¯,s1)will be 1, however the same bit ofw(V,C¯,s2)will be 0. Hence, we have thatw(V,C¯,s1)w(V,C¯s2).

Thus, this lemma is proved.

Lemma 2. Given the set of Boolean variablesVand the set of weighted clausesC˜, ifsis the unique optimal solution to the biased weighted MAX-SAT instancewMAXSAT(V,C), thensis also optimal to weighted MAX-SAT instancewMAXSAT(V,C).

Proof. Otherwise, there must exist a solutionsto thewMAXSAT(V,C˜)such thatw(V,C˜,s)w(V,C˜,s*). By assumption that the weightw(C˜i)is a positive integer for each clauseC˜iC˜, thus we havew(V,C˜,s)w(V,C˜,s*)+1. Sincew(V,C¯,s)=w(V,C˜,s)+w(V,{xi,¬xi|xiV},s), we have thatw(V,C¯,s)w(V,C˜,s)+1/21/22n+1. Similarly,w(V,C¯,s*)w(V,C˜,s*)+1/21/22n+1. It implies thatw(V,C¯,s)w(V,C˜,s)w(V,C˜,s*)+1w(V,C¯,s*), which contradicts with the assumption thatsis the unique optimal solution to thewMAXSAT(V,C¯). 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 unlessP=NP.

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 instancewMAXSAT(V,C), the biased weighted MAX-SAT instancewMAXSAT(V,C¯)can be constructed by an algorithm denoted byΓinΟ(n)time.

Since thewMAXSAT(V,C)is also a weighted MAX-SAT instance, its backbonecan be computed byΛin polynomial time (denoted by). By Lemma 1, the backbone is the unique optimal solution to thewMAXSAT(V,C¯). By Lemm2, thebone(V,C¯)is an optimal solution to thewMAXSAT(V,C˜)as well.

Hence, any weighted MAX-SAT instance can be exactly solved inΟ(n)+Ο()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 unlessP=NP.

Proof. Otherwise, given any weighted MAX-SAT instancewMAXSAT(V,C˜), we can always construct a biased weighted MAX-SAT instancewMAXSAT(V,C¯)according to Definition 4. As proven in Theorem 1, the backbonebone(V,C¯)is an optimal solution to thewMAXSAT(V,C˜).

If there exists a polynomial time algorithmΛto retrieve a fixed fraction of the backbone, we can acquire at least one literalin thebone(V,C¯). In the following proof, we only consider the case that=xj(xjV). For the case that=¬xj(xjV), it can be proved in a similar way.

LetC^be the set of those clauses containing¬xj, letC^be the set of the remaining parts of the clauses fromC^after deleting¬xj. Since=xj, we can construct a new smaller weighted MAX-SAT instancewMAXSAT(V\{xj},C˜), whereC˜={C˜i|C˜iC˜,C˜i contains no xj or ¬xj}C^.

By repeating such procedures, an optimal solution towMAXSAT(V,C˜)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 instancewMAXSAT(V,C˜),n1,n2, a local search algorithmH

Output: solutions*

Begin

//sampling phase

1.w*=

2. fori=1ton1do

2.1 obtain a solutionsiwithH;

2.2 sample backbone fromsi;

2.3 ifw(V,C~,si)w*thenw*=w(V,C~,si),s*=si;

//backbone phase

3. fori=1ton2do

3.1 obtain a solutionsiwith backbone guidedH;

3.2 ifw(V,C~,si)w*thenw*=w(V,C~,si),s*=si;

4. returns*;

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 algorithmHin 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 parameterpwill increase top+(1p)φ, otherwisepwill decrease toppφ/2, 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 instancewMAXSAT(V,C˜),num, a probability for noise pickp

Output: solutions

Begin

1. letsbe a random assignment of variables ofV,w=w(V,C~,s);

2. fori=1tonum1do

2.1 pickc, as one of the unsatisfied clauses with maximal weight, randomly;

2.2 compute the break-count of all variables inc;

2.3 if a zero break-count exists

then pick one variable of zero break-count inc, randomly;

else with a probabilityp, pick one of all variables inc, randomly;

and with a probability1p, pick one variable of least break-count ones inc, randomly;

2.4 flip this variable and obtain solutions;

2.5 ifw(V,C~,s)wthenw'=w(V,C~,s),s=s;

2.6 adjust the value ofp;

3. returns;

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 flipsnumis set to be 200 and the noise probabilitypis 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.

Figure 1.

Relationship between local optima and global optima for 4 typical instances.

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 instancewMAXSAT(V,C˜),num, a probability for noise pickp, pseudo-backbone frequenciesF

Output: solutions

Begin

1. letsbe a random assignment of variables ofV, guided byF,w=w(V,C~,s);

2. fori=1tonum1do

2.1 pickcfromsas one of the unsatisfied clauses with maximum weight, guided byF;

2.2 compute the break-count of all variables inc;

2.3 if a zero break-count exists

then pick one variable of zero break-count ones incrandomly, guided byF;

else with a probabilityp, pick one of all variables incrandomly, guided byF; and with a probability1p, pick one variable of least break-count ones inc, guided byF;

2.4 flip this variable and obtain solutions;

2.5 ifw(V,C~,s)wthenw=w(V,C~,s),s=s;

2.6 adjust the value ofp;

3. returns;

End

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.

6. Conclusions

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 thatPNP. 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.

InstanceOptimaGRASPGRASP with path-relinkingBGLSImprovement
weightweighttime (seconds)weighttime (seconds)weighttime (seconds)
R4400PD2.8GAltix3700PDPD
jnh1420925420737192.1-4207393505491420925130.0447%
jnh4420830420615467.9----420813270.0470%
jnh542074242048830.9----420679270.0454%
jnh6420826420816504.2----420826260.0024%
jnh7420925420925188.1----42092550.0000%
jnh8420463419885546.4----420138270.0602%
jnh942059242007841.2----420289260.0502%
jnh10420840420565591.1-4203573004707420828270.0625%
jnh11420753420642757.4-420516--420672260.0071%
jnh12420925420737679.2-420871--420925140.0447%
jnh1342081642053312.9----420816260.0673%
jnh14420824420510197.7----420824260.0746%
jnh15420719420360424.6----420719260.0853%
jnh16420919420851392.8----420919260.0162%
jnh17420925420807448.0----42092520.0280%
jnh18420795420372142.9----420525260.0364%
jnh19420759420323611.3----420584260.0620%
jnh201394238394238604.3-394222400627639423800.0000%
jnh202394170393983348.7-393870--394029250.0117%
jnh203394199393889265.3----394135250.0624%
jnh205394238394224227.6----39423840.0036%
jnh207394238394101460.8----39423840.0348%
jnh208394159393987335.1----39381925-0.0426%
jnh209394238394031170.1----39423870.0525%
jnh210394238394238130.7----39423840.0000%
jnh211393979393739270.0----393979240.0609%
jnh212394238394043244.1-394006--394227250.0467%
jnh214394163393701486.4----394124240.1073%
jnh215394150393858601.8----394066240.0528%
jnh216394226394029441.1----394176250.0373%
jnh217394238394232125.4----39423800.0015%
jnh218394238394099155.7----39423810.0353%
jnh219394156393720502.8----393993250.0693%
jnh220394238394053513.5----394205240.0386%
jnh301444854444670522.1----444842310.0387%
jnh302444459444248493.9----444459280.0475%
jnh303444503444244416.1----444296280.0117%
jnh30444453344421496.7-4441254507060444318270.0234%
jnh305444112443503424.9-443815350054915443533290.0068%
jnh306444838444658567.8-444692200031380444838280.0405%
jnh307444314444159353.5----444314270.0349%
jnh30844472444422250.2----444568280.0778%
jnh30944457844434986.8----444488280.0313%
jnh31044439144428244.7----444307280.0056%

Table 1.

Experimental Results for Instances.

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.

Acknowledgments

This work is partially supported by the Natural Science Foundation of China under Grant No. 60805024; the National Research Foundation for the Doctoral Program of Higher Education of China under Grant No. 20070141020; the Natural Science Foundation of Liaoning Province under Grant No.20051082.

Appendix

According to Tab. 2, the performance conversion from SPEC shows as follows: SGI Altix 3700: Intel 865P = 510/32.5 = 15.6923 > 15.69.

SGI Altix 3700 Bx2 (1600 MHz L3 Itaninum 2)Intel 865P (2.8 GHz Pentium D)
CINT 2000 Rates51032.5

Table 2.

Benchmark from SPEC.

How to cite and reference

Link to this chapter Copy to clipboard

Cite this chapter Copy to clipboard

He Jiang and Jifeng Xuan (October 1st 2009). Backbone Guided Local Search for the Weighted Maximum Satisfiability Problem, Evolutionary Computation, Wellington Pinheiro dos Santos, IntechOpen, DOI: 10.5772/9610. Available from:

Embed this chapter on your site Copy to clipboard

<iframe src="http://www.intechopen.com/embed/evolutionary-computation/backbone-guided-local-search-for-the-weighted-maximum-satisfiability-problem" />

Embed this code snippet in the HTML of your website to show this chapter

chapter statistics

1110total chapter downloads

1Crossref citations

More statistics for editors and authors

Login to your personal dashboard for more detailed statistics on your publications.

Access personal reporting

Related Content

This Book

Next chapter

Hybrid Differential Evolution – Scatter Search Algorithm for Permutative Optimization

By Donald Davendra, Ivan Zelinka and Godfrey Onwubolu

Related Book

First chapter

Novel Binary Particle Swarm Optimization

By Mojtaba Ahmadieh Khanesar, Hassan Tavakoli, Mohammad Teshnehlab and Mahdi Aliyari Shoorehdeli

We are IntechOpen, the world's leading publisher of Open Access books. Built by scientists, for scientists. Our readership spans scientists, professors, researchers, librarians, and students, as well as business professionals. We share our knowledge and peer-reveiwed research papers with libraries, scientific and engineering societies, and also work with corporate R&D departments and government entities.

More about us