The identification of unsatisfiable problem instances poses a few questions, including knowing why the instance is unsatisfiable and how it can be repaired to become satisfiable. For example, configuring a product may not always result in a feasible configuration, but in that case the customer would be pleased to receive explanations to understand what made the configuration unfeasible or alternatively to receive some hints about how to make it feasible. Such feedback is in general expected to be as precise as possible, i.e. to identify a minimal reason of unsatisfiability and to minimize the impact of restoring satisfiability.
If one considers Boolean satisfiability (SAT), then these questions are answered identifying Minimal Unsatisfiable Subformulas (MUSes) and obtaining Maximum Satisfiability (MaxSAT) solutions. Similarly, in the context of the Constraint Satisfaction Problem (CSP) these questions are answered by identifying Minimal Unsatisfiable Cores (MUCs) and obtaining Maximum CSP (MaxCSP) solutions. However, as recently pointed out [7], in CSPs one may consider unsatisfiable sets of tuples instead of unsatisfiable sets of constraints. The first is considered to be a finer-grained explanation as unsatisfiable sets of tuples may eventually not contain as many tuples as unsatisfiable sets of constraints.
Let us get back again to the configuration of a product. Suppose you have two configuration requirements for your new car: (1) it has to be a sports car and (2) you want it to have the most inexpensive type of seats. It turns out that the car model that you have selected does not allow such configuration. So you may be simply told that those two requirements are not compatible or, much better, that a sports car must have leather seats which is incompatible with having cloth seats. The latter explanation is certainly more precise. Also, it will be easier for you to repair the initial configuration either keeping all but one of the characteristics of a sports car (leather seats) or forgetting about inexpensive seats.
This paper addresses the problem of repairing an unsatisfiable CSP instance by removing the smallest number of tuples. This has in general less impact than removing constraints, and in the worst case the same impact. A MaxSAT encoding is used to solve the problem of repairing a CSP for which constraints are defined as conflicts, with no need of first extracting a MUC. Using an unsatisfiability-based MaxSAT solver has the advantage of identifying unsatisfiable sets of tuples while restoring satisfiability.
The paper is organized as follows. The next section introduces the preliminaries, alongside with illustrative examples. Next, the new approach for restoring satisfiability in a CSP using MaxSAT is described. Experimental results show that the proposed approach is feasible. Finally, the paper concludes and points out future research directions.
In what follows we assume that CSP variables have finite domains and that the constraints over variables correspond to conflicts rather than supports. An assignment to a CSP instance is a set {(v 1 , a 1 ), . . . , (v k , a k )} where {v 1 , . . . , v k } ⊆ X is a set of variables and k. In case k = n the assignment is said to be complete. Assuming that a constraint relation specifies disallowed assignments, i.e. the conflicts, a solution to a CSP instance is a complete assignment such that no assignment to a constraint scope is a member of the corresponding constraint relation. A CSP instance for which there is a solution is said to be satisfiable; otherwise it is said to be unsatisfiable.
Example 1. (CSP) Let P be the CSP instance graphically represented in Figure 1. Formally, P = (X, D, C), with
, {(0, 1), (0, 2), (0, 3), (1, 2), (1, 3)}), ((x 1 , x 3 ), {(1, 1), (1, 2)}), ((x 2 , x 3 ), {(1, 1), (1, 2)})}. Figure 1 represents P taking into account its variables and constraint scopes (top) and its variable domains and constraint relations (bottom). The arrows denote the order of the variable values in the conflict tuples.
We should note that the constraints of the previous example could be alternatively defined in terms of allowed assignments, i.e. the supports. In some cases such approach has the advantage of requiring less tuples. For example, c 1 would become ((x 1 , x 2 ), {(1, 1)}) instead. But in other cases it may be the contrary. For example, c 3 would become ((x 2 , x 3 ), {(2, 1), (2, 2), (3, 1), (3, 2)}). Definition 2. (UC) An unsatisfiable core (UC) of an unsatisfiable CSP P = (X, D, C) is a CSP instance P = (X , D , C ) such that (1) P is unsatisfiable and (2) X ⊆ X, D ⊆ D is the set of domains of variables in X and C ⊆ C is the set of constraints with their scopes in X .
An unsatisfiable core (UC) of an unsatisfiable CSP instance is a CSP instance that is a subset of the former one with respect to its variables, domains and constraints, and is still unsatisfiable. An unsatisfiable CSP instance has at least one UC corresponding to itself.
An unsatisfiable core is expected to be minimal as it should be as precise as possible when identifying the causes of unfeasibility, thus extracting minimal unsatisfiable cores (MUCs). An UC has at least one MUC, and in case it is unique then the MUC is equal to the UC. Removing one constraint per MUC restores satisfiability. A smaller number of constraints suffices when constraints are shared by different MUCs. Definition 3. (MUC [5]) A minimal unsatisfiable core (MUC) of an unsatisfiable CSP instance P is an UC of P , say P , such that removing any of the constraints of P makes the resulting CSP instance satisfiable.
Providing the user with explanations of unsatisfiability of CSPs has been first addressed with QuickXplain [8]. Moreover, the extraction of MUCs in CSPs has been recently made feasible [5]. The proposed algorithm performs successive runs of a complete backtracking search, using weights, in order to isolate an inconsistent subset of constraints.
Another approach for explaining unfeasibility consists in dealing with the tuples of constraint relations (in the sequel called tuples) rather than constraints defined as a pair with their scopes and relations [7]. This approach has clear advantages. Instead of identifying a set of constraints as the cause of unsatisfiability, a set of tuples is identified. Consequently, restoring satisfiability when considering tuples implies removing tuples rather than constraints, which may have a minor impact on the encoding. This assumes that, when making the encoding of a CSP instance, errors have been introduced when encoding a few tuples rather than when encoding a few constraints (including all its tuples). It is worth mentioning that tuples in a MUST do not necessarily belong to constraints in a MUC. An illustrative example is given below. x 1
x 2
x 3 Satisfiability of a CSP can be restored by removing one tuple of each MUST. Similarly to MUCs, a smaller number of tuples may be removed when tuples are shared by different MUSTs. For the running example, removing a tuple representing either the conflict between assignments x 1 = 0 and x 2 = 2 or assignments x 1 = 0 and x 2 = 3 suffices to restore satisfiability.
We assume the reader is familiar with the SAT problem that consists in deciding whether there exists a satisfying assignment to a set of Boolean variables such that a given CNF formula is satisfied. A CNF formula is a conjunction of clauses, where a clause is a disjunction of literals and a literal is a Boolean variable or its complement (a positive or a negative literal, respectively).
A large body of research in SAT has been devoted to explaining unfeasibility of CNF formulas in the last decade. These explanations have many different applications and are of the utmost importance in model checking using SAT solvers. For each iteration, if the call to the SAT solver returns no solution, then an explanation is extracted to be incorporated in the next iteration. Clearly, this explanation should be as precise as possible. Explanations including irrelevant clauses are expected to have a negative impact in the subsequent iterations.
The design of tools to identify unsatisfiable subformulas (USes) in SAT formulas has been early addressed by Bruni [2] who used an heuristic approach to identify a subset of clauses that are still unsatisfiable. Later on, Zhang [18] and Goldberg [4] proposed a similar idea of extracting unsatisfiability proofs based on the resolution steps taken for deriving the empty clause. These resolution steps are implicitly behind the conflict clauses added to the formula as a result of the analysis of conflicts during the search. The identification of all the minimal unsatisfiable subformulas (MUSes) in a systematic way was first developed by Liffiton [11,12] and later used for identifying the smallest MUS in an efficient way [10]. The identification of MUSes has also shown to be competitive recurring to a local search procedure as a preprocessing step to reduce the number of clauses that may be part of the MUS [6].
The MaxSAT problem consists in finding the largest number of clauses that can be satisfied in a CNF formula. The partial MaxSAT problem distinguishes between hard and soft clauses: hard clauses must be satisfied by any solution, while the number of soft clauses satisfied by a solution must be maximized. Partial MaxSAT can be seen as a compromise between SAT and MaxSAT where the hard clauses are treated as a SAT problem and the soft clauses are treated as a MaxSAT problem.
The goal of restoring satisfiability of a CSP instance with a minimal impact can be achieved by identifying the smallest size set of tuples to be removed from the CSP constraint relations. Removing these tuples guarantees that the instance is no longer unsatisfiable, whereas adding any of the removed tuples makes the instance unsatisfiable.
With the aim of restoring CSPs satisfiability, recent work by Grégoire et al. [7] This paper suggests restoring CSP satisfiability with MaxSAT. This is a clear advantage with respect to Muster, which only removes one MUST. The proposed algorithm involves three steps: (1) encoding the problem into partial MaxSAT, (2) solving the partial MaxSAT instance and (3) identifying the tuples to be removed from the CSP instance given the partial MaxSAT solution. The pseudo code for this procedure is illustrated in Algorithm 2. For each partial MaxSAT instance P encoding a CSP instance P , there is a mapping between each MaxSAT variable and each domain value of a CSP variable. A partial MaxSAT solver is then called to solve P . Its solution is used to identify the set of constraint tuples of P to be removed. In this section, we will explain how to encode a CSP instance into a partial MaxSAT instance to restore satisfiability.
We recall that given a CSP instance P = (X, D, C) for which the constraints represent conflicts, it is encoded into a SAT instance P as follows1 :
• For each variable x ∈ X and each value in the corresponding domain d(x) ∈ D is created a Boolean variable.
• • For each tuple t ∈ R of each constraint c = (S, R) ∈ C is created a clause with |S| negative literals to ensure that the corresponding values are disallowed. In what follows, these clauses will be called conflict clauses.
We should note that there exist alternative encodings for guaranteeing that exactly one value is assigned to each CSP variable (see for example [13,16]). The CSP to SAT encoding used by Muster does not include the at most one clauses. Provided that every at least one clause belongs to the MUST, computing one MUST amounts to compute one MUS in the CNF formula.
Consider an unsatisfiable CSP instance P = (X, D, C) with constraints representing conflicts and for which the minimum set of tuples to be removed in order to restore satisfiability is to be found. This problem is encoded into a partial MaxSAT instance P as follows:
• Each at least one clause produced by an encoding of P into SAT is a hard clause of P .
• Each conflict clause produced by an encoding of P into SAT is a soft clause of P .
Remark 1. When using the MaxSAT encoding to restore satisfiability of a CSP instance, there is no need of adding at most one clauses to guarantee a one-to-one correspondence between Boolean variables and CSP variable values.
Proof. We assume that the CSP instance is unsatisfiable. The hard clauses guarantee that at least one value is assigned to each CSP variable. The soft clauses guarantee the smallest number of violated constraints. Having more than one value assigned to a CSP variable, which means that any of those values can be selected to be in the solution, cannot reduce the number of violated constraints.
Proposition 1. A solution to the MaxSAT instance P corresponds to the minimum set of tuples to be removed from P in order to restore satisfiability.
Proof. The hard clauses guarantee that any solution to the partial MaxSAT instance corresponds to a CSP complete assignment. Each soft clause represents one tuple in a constraint. Hence, a solution to the partial MaxSAT instance satisfies the largest number of tuples, which is equivalent to unsatisfying the smallest number of tuples.
Remark 2. No more than one tuple of each constraint has to be removed to restore the satisfiability of a CSP instance.
Proof. Restoring the satisfiability of a CSP instance corresponds to finding an assignment such that no constraint is violated. One assignment can violate at most one tuple in a constraint. Hence, no more than one tuple per constraint needs to be removed.
As an additional remark, observe that MaxSAT has been used in the past to solve the MaxCSP problem [1], thus allowing to know which constraints have to be removed to restore satisfiability of a CSP. Although the motivation of this use of MaxSAT clearly differs from the one proposed here, the encoding is similar. Proposition 2. (From [1]) A MaxCSP solution may be obtained from identifying the smallest set of tuples to be removed to restore the satisfiability of a CSP instance.
Unsatisfiability-based MaxSAT solvers [3,15,14] represent an approach for solving MaxSAT problem instances, which contrasts with the traditional MaxSAT solvers based on branch and bound algorithms [9]. Unsatisfiabilitybased MaxSAT solvers iteratively identify Unsatisfiable Subformulas (USes), not necessarily minimal, which are relaxed after being identified. Clauses are relaxed by adding one relaxation variable per clause. The use of cardinality constraints on the variables used to relax clauses in USes guarantees that a minimum number of clauses is relaxed. Hence, the MaxSAT solution is computed. The identification of clauses in USes is iterated until the resulting formula is satisfiable. In this case, one clause from each identified US is relaxed. A number of variants of MaxSAT algorithms have been proposed [3,15,14], which differ on the actual organization of the algorithm, and the way cardinality constraints are encoded to clausal form.
The use of unsatisfiability-based MaxSAT solvers has the advantage of having a solver which identifies unsatisfiable cores while running. Hence, in case a solution is not found within the allowed CPU time, there is still relevant information for restoring satisfiability.
In this paper we will be using the unsatisfiability-based MSUnCore [15,14] version of April 2009. For this reason, we will use the name MSUnCore to denote the MaxSAT-based algorithm for restoring CSPs satisfiability.
A few interesting remarks are made below in order to stress that MSUn-Core should be considered as an alternative approach to Muster.
We should first clarify how the Muster algorithm could be instrumented to restore CSPs satisfiability. First, a MUC is identified in a CSP. Second, MUSTs in the MUC are identified to restore satisfiability, i.e. the required tuples are removed from the MUC such that it becomes satisfiable. Now these same tuples are removed from the CSP and the whole process is repeated.
Remark 3. The solution provided by MSUnCore removes a number of tuples that is equal or smaller than the iterated application of Muster.
Proof. Muster first identifies a MUC and then MUSTs within the MUC. This does not guarantee removing tuples shared by MUSTs belonging to different MUCs. (Figure 2 illustrates this issue: unless Muster is lucky enough to remove tuple (0, 2) or tuple (0, 3), Muster will remove two tuples in two iterations, while MSUnCore will remove only one tuple.) Remark 4. The number of Unsatisfiable Sets of Tuples (USTs) identified by MSUnCore during the search provides a lower bound for the number of tuples to be removed to restore satisfiability.
Proof. Unsatisfiability-based MaxSAT solvers (of which MSUnCore is a concrete example), iteratively identify and relax unsatisfiable subformulas (USes). Moreover, for each iteration for which a US is found, the number of clauses to relax is increased by 1. Consequently, at each step of the MSUnCore algorithm, the number of identified USes represents a lower bound on the MaxSAT solution, and so represents a lower bound on the number of tuples to be removed to restore satisfiability.
This section illustrates the feasibility of the proposed approach, i.e. the use of MaxSAT to restore CSP satisfiability removing the smallest number of tuples. With this purpose, MUSTs are eliminated although not directly identified. This approach is clearly different from the one implemented in Muster as we end up restoring the satisfiability of a CSP instance. In contrast, Muster identifies one MUST in a MUC. Restoring satisfiability would require running Muster iteratively and removing tuples to eliminate MUSTs until the problem instance becomes satisfiable. Note that this procedure does not guarantee that the smallest number of tuples is removed because MUSTs with tuples in constraints in more than one MUC are not given priority. Figure 2 illustrates this feature. Suppose you first identify c 1 and c 2 as a MUC and then you eliminate the MUST in the figure (bottom, left) by removing tuple (0, 1). This does not eliminate the other MUST in the figure, but having removed either tuple (0, 2) or (0, 3) would have done so.
The proposed approach and Muster should therefore be regarded as complementary approaches. Even though, we have performed an experimental evaluation running both approaches (Muster and MSUnCore) on the same set of instances from the First CSP Competition2 , which corresponds to the set of instances used to test Muster in [7]. These instances range from random binary CSP instances (named composed) to instances of the queens-knights problem (qk), instances of the radio link frequency assignment problem (graph and scen), one instance of the queen attacking problem (qa) and 3-SAT instances encoded using the dual method (dual ehi).
Note that the results are not intended to provide a winner or a loser, but rather to identify strengths and weaknesses of different approaches used to achieve different albeit complementary goals. Table 1 provides the characterization and results for each instance. Each instance is characterized in terms of the number of CSP variables (#vars) and constraints (#constr). In addition, the CPU time required by Muster to identify one MUC and one MUST in that MUC is given (1MUC+1MUST), as well as the CPU time required by an unsatisfiability-based MaxSAT solver (MSUnCore [14]) to identify the first UST (1UST), which is not necessarily minimal. Additional information gives the CPU time required by MSUnCore to restore satisfiability (AllMUSTs), which implies eliminating all MUSTs, as well as the total number of tuples to be removed to restore satisfiability (RmTup). The CPU time was limited to 1000 seconds (TO means timeout). In case only a few USTs are identified, it is given a lower bound on the number of tuples to be removed to restore satisfiability. Both Muster and MSUnCore were run on a Intel Xeon 5160 3GHz under RedHat Enterprise Linux WS4.
First of all, the results illustrate the feasibility of the proposed approach. Many times MSUnCore is able to restore satisfiability faster than Muster is able to identify one MUST in a MUC. Also interesting is to note that most instances are restored in terms of satisfiability by removing very few tuples. This supports the claim that removing tuples has a very little impact. For the cases where MSUnCore is not able to completely restore satisfiability, it is able to identify a few USTs though, which gives a lower bound on the number of tuples to be removed. In any case, the identification of the first UST by MSUnCore is always faster than using Muster. Also, MSUn-Core seems to require more time when the number of tuples to be removed is larger.
This paper suggests the use of MaxSAT to restore CSP satisfiability by removing the smallest number of constraint tuples. This solution contrasts with a MaxCSP solution as tuples instead of constraints are removed. We argue that removing tuples is more adequate for most of the problems due to having a minor impact.
Future work includes adapting MSUnCore for identifying minimal unsatisfiable cores. This will have the advantage of identifying MUSTs instead of USTs, which are more relevant in case the search does not terminate in the given timeout.
This research is partially funded by Fundação para a Ciência e Tecnologia under research projects SHIPs (PTDC/EIA/64164/2006) and BSOLO (PTDC/EIA/76572/2006).