Three Truth Values for the SAT and MAX-SAT Problems

1 Introduction

The satisfiability problem (SAT) [Garey and Johnson, 1979] consists in finding a truth assignment that satisfies a wellformed Boolean expression. An instance of the SAT problem is then defined by a set of Boolean variables (also called atoms) CG BP CUDC BD BN BMBMBMBN DC D2 CV and a Boolean formula AUBM
BU D2 AX
BU. As usual, the formula AU is supposed to be in conjunctive normal form (CNF) (i.e., it is a conjunction of clauses where a clause is a disjunction of literals 1 ). The formula is said to be satisfiable if there exists an assignment (i.e., a function BTBM CG AX
BU D2 ) satisfying AU and unsatisfiable otherwise. The search space CB corresponds to the set of all possible assignments.AU is obviously satisfied if all of its clauses are satisfied. In this context, the maximum satisfiability problem (MAX-SAT) corresponds to the minimization of the number of false clauses.

Two classes of methods are used to solve SAT and MAXSAT problems, namely exact and approximate methods.

Exact methods are able to find all the solutions of an instance or, if there is no solution, to prove its unsatisfiability. These methods are generally based on the Davis-PutnamLogemann-Loveland procedure [Davis et al., 1962] which explores a binary search tree, building incrementally truth assignments. They provide very good results but are not suitable for the MAX-SAT problem. Other exact methods, generally based on Branch and Bound (B&B) algorithms [Borchers and Furman, 1999] have been designed to handle MAX-SAT, but their performances are often limited for large instances.

Approximate methods are mainly based on local search and evolutionary algorithms. We focus here on local search algorithms which have been widely studied in the SAT community [Selman et al., 1992; 1994; Spears, 1996; Mazure et al., 1997; Hirsch and Kojevnikov, 2001]. As usual, these algorithms rely on the fundamental characteristics of local search: the exploration of the search space is achieved by moving from an element to one of its neighbors, these moves being performed according to specific heuristics. Therefore, they expect to minimize, on the assignments space, a function corresponding to the number of false clauses. They are thus naturally designed for the MAX-SAT problem and allow one to handle large instances.

1 A literal is a variable or its negation.

The efficiency of such algorithms is strongly related to their capacities to finely exploit specific areas of the search space when needed (i.e., intensify the search) and to widely explore the space by moving to different promising areas (i.e., diversify the search). These aspects are controlled through parameters to ensure a good tradeoff between diversification and intensification. But, actually these two notions are not really well defined and therefore, parameters tuning remains a key point when using such algorithms.

We should remark that exact and approximate methods do not use the same representations for their search space. Their hybridizations [Mazure et al., 1998; Prestwich, 2000; Habet et al., 2002; Prestwich, 2004] are not trivial since exact methods work on partial assignments incrementally completed by the resolution process while approximate algorithms explore the set of all possible complete assignments. A partial assignment is an assignment where some variables are not yet valued and can be thus considered as the representation of a set of complete assignments. From a local search point of view, the use of such partial assignments could lead to new diversification and intensification processes. Indeed, the diversification of the search could be achieved by moving over large sets of complete assignments induced by given partial assignments, while the valuation of some variables of such partial assignments could be considered as a way to focus on a more restricted part of the search space.

The purpose of this paper is to define a uniformmodel for these two types of assignments in order to precisely define and study the fundamental mechanisms of local search for SAT and MAX-SAT resolutions. This framework allows us to propose a new local search scheme which provides a uniform control of the search and which can be introduced in well known local search procedures: Tabu Search and Walksat.

2 A 3-Valued Framework

We propose a new resolution framework for the SAT and the MAX-SAT problems which introduces a third truth value undefined in order to improve the resolution efficiency. Within this framework, local search methods will be extended in order to take into account partial assignments and, therefore, several notions and logical rules have to be redefined.

2.1 Standard Local Searches

In the classic SAT and MAX-SAT context, the search space CB is the set of all possible complete truth assignments. The objective function to maximize corresponds to the number of satisfied clauses given by the D7D8CPD2CSCPD6CS CTDACPD0 function:

where D7CPD8B4BTBN B5 means that the clause is satisfied by the assignment BT BE CB and CYBXCY is the cardinality of the set BX.

The moves are clearly possible flips of the values of a given assignment. The flip of a variable CX in an assignment BT is the swap of its truth value (T (true) to F (false) or F to T). The best flip is selected thanks to a D7D8CPD2CSCPD6CS CWD3D3D7CT function which returns the variable whose flip provides the best improvement (i.e., maximizes the number of false clauses which become true after the flip minus the number of satisfied clauses which become false).

A naive local search algorithm for SAT and MAX-SAT consists in selecting the best move at each step (using D7D8CPD2CSCPD6CS CWD3D3D7CT). It stops either when a solution is found or when a maximum number of steps has been reached. Then, it returns the best assignment found (w.r.t. D7D8CPD2CSCPD6CS CTDACPD0). Specific control heuristics can be added to improve the efficiency of the search, such as random walks and other noise strategies [Selman et al., 1994].

2.2 Introducing an undefined Value

Our purpose is to provide a uniform framework to represent complete and partial assignments. Concerning complete assignments, with classical D8D6D9CT and CUCPD0D7CT values, the logical interpretation rules are well-known but, with partial assignments, non valued variables appear and we decide to introduce a third truth value to represent them.

We add a truth value U(undefined) and consider the set of truth values CC BP CUCDBN CCBN BYCV in our 3-valued framework. This new value induces some changes in the standard logical interpretation rules. Two approaches can be used to define these rules: an optimistic approach and a pessimistic approach.

• AF The optimistic approach is the most commonly used. Indeed, all the exact methods exploring a search tree are based on this approach. A clause is considered undefined if none of its literals is true and at least one of its literals is undefined. This approach corresponds to the following simplification rules:

• AF We propose here an alternative pessimistic approach which relies on the fact that as soon as a clause has a false literal and no true literal, it is considered as false. An undefined clause must have all its literals set to undefined. This approach corresponds to the following rules:

Our search structure is now defined and we may study the precise behavior of local search algorithms on this structure with three truth values.

2.3 Local Search Transitions

We define a partial order BT on the set CC such as CD BT CC and CD BT BY. In this context, given a SAT problem with D2 variables, our search space will be the set CC D2 . The ordering relation BT can be naturally extended to CC D2 : B4DC BD BN A1 A1 A1 BN DC D2 B5 BT B4DD BD BN A1 A1 A1 BN DD D2 B5 if and only if BLCXBN DC CX BT DD CX and CYBN DD CY BT DC CY . We consider the partial ordering B4CC D2 BNBTB5 with the greatest element BQ BP B4CDBN A1 A1 A1 BNCDB5. This structure will now be used to precisely describe the behavior of local search algorithms. We consider a basic local search move 2 as a transition BT AX BT BC where BTBNBT BC BE CC D2 . Since we only consider here a classical neighborhood we require that transitions B4DC BD BN A1 A1 A1 BN DC D2 B5 AX B4DD BD BN A1 A1 A1 BN DD D2 B5 satisfy BLCXBN DC CX BIBP DD CX and BKCY BIBP CXBN DC CY BP DD CY . This neighborhood corresponds to a hamming distance equal to 1 between two neighbors, which is related to the CUD0CXD4 function.

On the one hand, we first consider the assignment landscape point of view. The 3-valued framework allows us to handle both partial and complete assignments and, as mentioned above, a partial assignments is seen as a representation of a set of smaller assignments (w.r.t. BT). Therefore, diversification consists in considering larger sets of elements of the search space while intensification focus on fewer elements. The transition corresponds to a layer exploration when the number of undefined variables remains the same.

- Diversification: BT AX BT BC with BT BC BT BT - Intensification: BT AX BT BC with BT BT BT BC

• Layer Exploration: BT AX BT BC with BT BIBT BT BC and BT BC BIBT BT

On the other hand, we have to take into account the evaluation of the assignments. The introduction of the third truth value requires us to redefine the D7D8CPD2CSCPD6CS CTDACPD0 function and the D7D8CPD2CSCPD6CS CWD3D3D7CT function of section 2.1, since the number of undefined clauses must be taken into account. The new evaluation function CTDACPD0 returns the number of true clauses as well as the number of undefined clauses. In this context, an assignment is better than another if it satisfies more clauses. If the number of true clauses is equal for two assignments, the one generating the greatest number of undefined clauses will be considered as the best assignment.

2 With three truth values, the concepts of flip is not valid anymore. We prefer to use the concept of move, step or transition.

where D9D2CSCTCUCXD2CTCSB4BTBN B5 means that the clause is undefined by the assignment BT BE CB.

Using this function, we may define CBD3D0 AU , the set of all the solutions for a formula AU: CBD3D0 AU BP CUBTCYCTDACPD0B4BTB5 BP B4CZBN BCB5BN BT BE CC D2 CV with CZ BP CYCU CY BE AUCVCY.

We define the order BQ CTDACPD0 as the lexicographic extension B4BQBNBQB5 of the order BQ on the pair constructed by the CTDACPD0 function. We may now consider the transitions from this evaluation point of view.

• Improve: BTAXBT BC with BT BC BQ CTDACPD0 BT
• Preserve: BT AX BT BC with CTDACPD0B4BT BC B5 BP CTDACPD0B4BTB5

- Deteriorate: BT AX BT BC with BT BQ CTDACPD0 BT BC

Using these concepts, a move is now characterized from each point of view: for instance, a given move may correspond to a diversification and improve transition.

These notions are illustrated in example 1. Indeed, in our 3-valued framework, both exact and approximate methods can be modeled. The search trees used by Davis-PutnamLogemann-Loveland like procedures are sets of intensification and diversification transitions whereas classic local search algorithms perform sets of improving, deteriorating and preserving transitions at the lowest layer (with no undefined value).

At this stage, one has to consider possible combinations of these transitions, issued from these two points of view, to build a general local search process.

The purpose of the search process is to increase the number of true clauses. When this is not possible, it is then preferable to increase the number of undefined clauses and thus to reduce the number of false clauses. We propose a new CWD3D3D7CT function which selects a variable and a change of its value which maximizes the number of true clauses and minimizes the number of false clauses (increasing the number of undefined clauses if necessary).

At this step, the main components of a local search algorithm have been described. We will now study their behaviour and combination.

2.4 Evaluation of the Logical Rules

We want to measure the effect of the logical interpretation rules, presented in section 2.2, on the search process. As described before, a 3-valued local search (3LS) algorithmmay return now partial assignments which represent indeed sets of assignments. To evaluate the quality of these partial assignments, it is necessary to explore exhaustively the corresponding subset in order to find the best complete assignment that it contains. This can be achieved thanks to a Branch and Bound procedure (B&B) which performs an exhaustive search by exploring a restricted search tree whose root is the partial assignment provided by the 3LS algorithm.

Table 1 compares the effects of the different logical rules. Tests are realized on standard random 3-sat instances with 500, 1000 and 2000 variables (F500.cnf, F1000.cnf and F2000.cnf). The 3LS algorithm used for these tests is a 3valued Tabu Search (3TS-BB, see next section). The algorithm runs until 5000 iterations are performed. The number of undefined variables (D2CQBM DACPD6BM CD), the number of clauses with one, two and three undefined variables (B4CDBN CDCDBN CDCDCDB5) and the quality (B4CCBNCDBN BYB5 CPCUD8CTD6 BFCCCB-BUBU) are memorized for the last partial assignment found. To estimate the potential quality of the partial assignment found by 3TS-BB, a B&B algorithm is executed and provides the best complete assignment (B4CCBN BYB5 CPCUD8CTD6 BUB2BU) by assigning the undefined variables.

Table 1 shows a clear dominance of the pessimistic interpretation. The quality of the partial assignment found during the 3TS-BB is better since the number of true clauses found after B&B is greater than the corresponding number obtained with the optimistic interpretation.

2.5 Impact of Transitions in the Search Process

The optimistic and the pessimistic interpretations do not involve the same behaviour w.r.t. the different combinations of transitions characterizing a move, as described in section 2.3. Table 2 presents the evolution of the number of true, undefined and false clauses (T,U,F) for the optimistic (opt.) and the pessimistic (pes.) approaches and all the combinations of transitions excepted for the "preserve" transition since no change is performed in this case.

Table 2: Possible evolutions of the number of true, undefined and false clauses (T,U,F) due to the different combinations of transitions. (BQ: increase, AL: increase or remain stable, BP: remain stable, AK: decrease or remain stable, BO: decrease and D7: increase, decrease or remain stable)

We may assess common properties for the optimistic and pessimistic approaches. When applying an intensification transition, it is neither possible to create undefined clauses nor to delete true clauses. Concerning the diversification transition, true clauses cannot be created and undefined clauses cannot be deleted. Specific properties related to the optimistic and pessimistic interpretations can also be depicted: using the optimistic approach, false clauses cannot be generated during a diversification transition while in the pessimistic case, undefined clauses cannot be created nor deleted during the "Layer exploration".

3 3-valued Framework used inWell-known Algorithms

Tabu Search (TS) [Glover and Laguna, 1997; Mazure et al., 1997] and Walksat [Selman et al., 1994] are two well-known local search algorithms for SAT and MAX-SAT. To show the interest of the 3-valued framework, we have adapted these two algorithms in order to obtain 3TS-BB and 3Walksat-BB. The CWD3D3D7CT and the CTDACPD0 functions (2.3) were used to transform the two algorithms in their 3-valued versions.

3.1 3TS-BB

The 3-valued Tabu Search (3TS-BB) is a local search metaheuristics based on standard Tabu Search. Its aim is to maximize the number of true clauses and minimize the number of false clauses. The exploration of the search space is achieved by moving from an assignment to an other selected by the CWD3D3D7CT function. These moves are guided by the CTDACPD0 function which evaluates their benefit. In order to avoid problems induced by local optima, 3TS-BB uses a tabu list containing informations on previously visited configurations to forbid some possible loops in the search process. The length of the tabu list is set to 10% of the number of variables (empirical result inspired by [Mazure et al., 1997]). One expects 3TSBB to return a complete assignment to answer to the MAXSAT problem. Then, we decide to regularly complete the partial assignments with a B&B procedure in order to generate a complete assignment. This completion is realized every D7 moves (empirically fixed to 5000). To reduce the execution time, B&B must not be used when there are too many undefined variables in the partial assignments. We impose that the maximum number of unassigned variables should not to be greater than a bound CQ (empirically fixed to 100). The search stops when a solution is found or when BDBC BI moves are executed.

3.2 3Walksat-BB

The general process of the 3-valued Walksat (3Walksat-BB) uses similar principles. Like the standard Walksat, 3WalksatBB is a randomized local search algorithm, which tries to determine the best move by randomly choosing an unsatisfied clause and selecting one of its variable thanks to the CWD3D3D7CT function. We use as basis the version v41 of Walksat. The search is composed of BDBC tries. Each try starts with a random assignment and after BDBC BH moves, the best assignment found is completed with a classic B&B, if it is not a complete assignment. When a solution is found, the search stops. Like Walksat, 3Walksat-BB uses the "novelty" heuristic [Selman et al., 1994] with a noise set to 0.5 (its default value).

Remark: It is important to note that, contrary to the standard local search algorithms, the 3-valued algorithms may start their searches with the BQ assignment B4CDBN A1 A1 A1 BNCDB5. The influence of the initial assignment in the results is then avoided.

4 Experimental Results

Due to the approximate and non-deterministic nature of TS, 3TS-BB, Walksat and 3Walksat-BB, each algorithm runs 20 times on each benchmark. Tests are realized on a cluster with Linux and Alinka (5 nodes each of them with 2 CPU Pentium IV 2.2 GHz and 1 Gb of RAM) used sequentially. The maximum number of allowed local search steps is BDBC BI . For our algorithms, we consider that a backtrack performed during the B&B procedure has the same cost than a local search step.

All studied instances (Table 3) have been used for SAT competition 2003 [Simon et al., 2003] and contain satisfiable and unsatisfiable instances. They come from different families of instances.

To study the four algorithms we present two tables (Tables 4 and 5): the first one is a comparison between TS and 3TSBB and the second one between Walksat and 3Walksat-BB. Two criterions are used: the number of false clauses (fc.) and the number of steps (including local search moves and B&B backtracks) to obtain the best result (steps). For these two criterions we present the average (avg.) and its standard deviation (s.d.). Another interesting value is proposed in the last column: the percentage of improvement of the 3-version v.s the standard version, w.r.t. the average number of false clauses.

Tables 4 and 5 show that the 3-valued framework permits to boost classic local search methods like TS andWalksat. Indeed, 3TS-BB provides an improvement which can be sometimes weak and exceptionally negative (A0BDBMBLBEB1 for ezfact64 3) but often really more significant for most of the instances (B7BLBFBMBJBDB1 for par32-5) and all the families. For Walksat, the improvement is less important with the 3-valued framework. However, 3Walksat-BB provides interesting results because 8 families are improved (4 more than 15%) and only 2 families are deteriorated (never more than -5%).

It is interesting to remark that the 3TS-BB and 3WalksatBB results are better while the search power represented by the number of steps is in the same order of magnitude. Execution time is not mentioned in the tables but remains approximatively the same with and without the 3-valued framework.

5 Discussion and Conclusion

Our 3-valued framework allows us to handle partial assignments and, thanks to these partial assignments, some characteristics of the formula, like the backbone [Dubois and Dequen, 2001], can be easily defined. The backbone of a satisfiable formula AU is the set of entailed literals. A literal D0 is entailed by AU if and only if AU CM B4BMD0B5 is unsatisfiable. In the 3-valued framework, the backbone is the element BT BE CBD3D0 AU such that BT BC BT BTBN BT BC BE CBD3D0 AU .

In this paper, we have proposed a new resolution framework for SAT and MAX-SAT problems which includes a third truth value D9D2CSCTCUCXD2CTCS in order to handle both partial and complete assignments. We have precisely studied the extension and behavior of local search algorithms using this third truth value. Two possible logical interpretations have been considered and it appears that the pessimistic approach provides better results than the optimistic approach.

We have then introduced this 3-valued framework inside Tabu Search and Walksat algorithms and the results are very promising. Our future works will consist in developing new specific heuristics using this 3-valued framework and in extending other well known algorithms in a 3-valued version. This framework could also serve as basis for full hybridizations of complete and incomplete resolution techniques.

Acknowledgments

The work presented in this paper is partially supported by the CPER COM program. We would like to thank the anonymous referees for their useful comments.