The extraction of a Minimal Unsatisfiable Core (MUC) in a Constraint Satisfaction Problem (CSP) aims to identify a subset of constraints that make a CSP instance unsatisafible. Recent work has addressed the identification of a Minimal Set of Unsatisafible Tuples (MUST) in order to restore the CSP satisfiability with respect to that MUC. A two-step algorithm has been proposed: first, a MUC is identiefid, and second, a MUST in the MUC is identiefid. This paper proposes an integrated algorithm for restoring satisfiability in a CSP, making use of an unsatisfiability-based MaxSAT solver. The proposed approach encodes the CSP instance as a partial MaxSAT instance, in such a way that solving the MaxSAT instance corresponds to identifying the smallest set of tuples to be removed from the CSP instance to restore satisafibility. Experimental results illustrate the feasibility of the approach.
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 rfist is considered to be a nfier-grained explanation as unsatisafible sets of tuples may eventually not contain as many tuples as unsatisafible sets of constraints.
Let us get back again to the configuration of a product. Suppose you
have two configuration requirements for your new car: (
This paper addresses the problem of repairing an unsatisafible 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 denfied as conflicts, with no need of rfist extracting a MUC. Using an unsatisafibility-based MaxSAT solver has the advantage of identifying unsatisfiable sets of tuples while restoring satisafibility.
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. 2 2.1
In what follows we assume that CSP variables have finite domains and that the constraints over variables correspond to conflicts rather than supports. Definition 1. (CSP) A CSP instance is a triple (X, D, C) where X = {x1, . . . , xn} is a set of n variables, D = {d(x1), . . . , d(xn)} is a set of n domains, where each domain d(x) corresponds to the domain of variable x ∈ X, and C = {c1, . . . , cm} is a set of m constraints. Each constraint c ∈ C is a pair c = (S, R) where S is a sequence of variables of X, called the constraint scope, and R is a |S|-ary relation over D, called the constraint relation.
An assignment to a CSP instance is a set {(v1, a1), . . . , (vk, ak)} where {v1, . . . , vk} ⊆ X is a set of variables and ai ∈ d(vi) for all i with 1 ≤ i ≤ 1 2 3 x2 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 X = {x1, x2, x3}, D = {d(x1) =
{0, 1}, d(x2) = {1, 2, 3}, d(x3) = {1, 2}} and C = {c1, c2, c3} = {((x1, x2),
{(
We should note that the constraints of the previous example could be
alternatively denfied in terms of allowed assignments, i.e. the supports. In
some cases such approach has the advantage of requiring less tuples. For
example, c1 would become ((x1, x2), {(
Definition 2. (UC) An unsatisfiable core (UC) of an unsatisfiable CSP
P = (X, D, C) is a CSP instance P 0 = (X0, D0, C0) such that (
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 unsatisafible 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 0, such that removing any of the constraints of P 0 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 unsatisafibility, a set of tuples is identified. Consequently, restoring satisafibility 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).
Definition 4. (MUST [7]) A minimal unsatisfiable set of tuples (MUST)
of an unsatisfiable CSP P = (X, D, C), with C = {(S1, R1), . . . , (Sm, Rm)},
is a CSP P 0 = (X0, D0, C0) such that (
It is worth mentioning that tuples in a MUST do not necessarily belong to constraints in a MUC. An illustrative example is given below. 1 2 x3 Example 2. (MUC and MUST) Figure 2 illustrates MUCs and MUSTs of the CSP instance P introduced in Example 1. P has two MUCs: one with c1 and c2 and another one with c1 and c3. An intuitive explanation is the following: c1 implies the assignment {(x1, 1), (x2, 1)}, whereas c2 forbids the assignment {(x1, 1)} and c3 forbids the assignment {(x2, 1)}. Any of these MUCs contains seven tuples. Several MUSTs can be identified in P but only two of them are illustrated in the figure (bottom). One of them (left) corresponds to the smallest MUST and contains only five tuples. The point is that not all tuples from constraint c1 are required to make the instance unsatisfiable when considering also c2. The other MUST (right) contains six tuples with the particularity of covering all the constraints.
Satisafibility 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 coniflct between assignments x1 = 0 and x2 = 2 or assignments x1 = 0 and x2 = 3 suffices to restore satisafibility. 2.2
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 satisefid. 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 unsatisafible. 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 coniflcts during the search. The identification of all the minimal unsatisafible 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 identicfiation 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 satisefid 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 satisefid 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. 3
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 unsatisafible, whereas adding any of the removed tuples makes the instance unsatisfiable.
With the aim of restoring CSPs satisfiability, recent work by Gerg´oire et
al. [7] introduced a two-step algorithm: (
This paper suggests restoring CSP satisafibility with MaxSAT. This is a
clear advantage with respect to Muster, which only removes one MUST.
The proposed algorithm involves three steps: (
We recall that given a CSP instance P = (X, D, C) for which the constraints represent coniflcts, it is encoded into a SAT instance P 0 as follows 1: • For each variable x ∈ X and each value in the corresponding domain d(x) ∈ D is created a Boolean variable. • For each set of Boolean variables {b1, . . . , b|d(x)|} associated with the same CSP variable x ∈ X create one clause (b1 ∨ . . . ∨ b|d(x)|) to ensure that each CSP variable is assigned at least one value, and a set of binary clauses (¬bi ∨ ¬bj ) with 1 ≤ i < j ≤ | d(x)| to ensure that no more than one value is assigned to a CSP variable. In what follows, these clauses will be called at least one clauses and at most one clauses, respectively. • 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]).
Example 3. (CSP to SAT) Consider a CSP instance P = (X, D, C) =
({x1, x2}, {d(x1) = {1, 2}, d(x2) = {1, 3}}, {((x1, x2), {(
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 unsatisafible CSP instance P = (X, D, C) with constraints representing coniflcts and for which the minimum set of tuples to be removed in order to restore satisafibility is to be found. This problem is encoded into a partial MaxSAT instance P 0 as follows: • Each at least one clause produced by an encoding of P into SAT is a hard clause of P 0. 1Details about encoding CSP into SAT and vice versa can be found in [17]. • Each conflict clause produced by an encoding of P into SAT is a soft clause of P 0.
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 0 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 satisefis 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 satisafibility of a CSP instance corresponds to nfiding 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 satisafibility 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. 3.2
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 satisafible. In this case, one clause from each identiefid 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 unsatisafible 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 satisafibility. 3.3
Muster vs MSUnCore A few interesting remarks are made below in order to stress that MSUnCore should be considered as an alternative approach to Muster.
We should first clarify how the Muster algorithm could be instrumented to restore CSPs satisafibility. First, a MUC is identified in a CSP. Second, MUSTs in the MUC are identified to restore satisafibility, i.e. the required tuples are removed from the MUC such that it becomes satisafible. 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 identiefis 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 (
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 satisafibility.
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 rfist identify c1
and c2 as a MUC and then you eliminate the MUST in the figure (bottom,
left) by removing tuple (
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 unsatisafibility-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 satisafibility. 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 satisafibility, 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, MSUnCore 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 unsatisafible 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 Fundac¸˜ao para a Ciˆencia e Tecnologia under research projects SHIPs (PTDC/EIA/64164/2006) and BSOLO (PTDC/EIA/76572/2006). [18] L. Zhang and S. Malik. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Design, Automation and Test in Europe Conference, pages 10880–10885, 2003.
CSP