=Paper=
{{Paper
|id=Vol-1453/15_WalterFelfernigKuechlin_InverseQuickxplainVsMaxsat_Confws-15_p97
|storemode=property
|title=Inverse QuickXplain vs. MaxSAT — a comparison in theory and practice
|pdfUrl=https://ceur-ws.org/Vol-1453/15_WalterFelfernigKuechlin_InverseQuickxplainVsMaxsat_Confws-15_p97.pdf
|volume=Vol-1453
|dblpUrl=https://dblp.org/rec/conf/confws/WalterFK15
}}
==Inverse QuickXplain vs. MaxSAT — a comparison in theory and practice==
https://ceur-ws.org/Vol-1453/15_WalterFelfernigKuechlin_InverseQuickxplainVsMaxsat_Confws-15_p97.pdf
Inverse Q UICK X PLAIN vs. M AX SAT —
A Comparison in Theory and Practice
Rouven Walter1 and Alexander Felfernig2 and Wolfgang Küchlin1
Abstract. We compare the concepts of the I NV QX algorithm the MCS of minimum cardinality; (ii) the Inverse Q UICK X PLAIN
for computing a Preferred Minimal Diagnosis vs. Partial Weighted (I NV QX) algorithm (also denoted as FAST D IAG) [4] delivers a pre-
M AX SAT in the context of Propositional Logic. In order to restore ferred minimal diagnosis w.r.t. a total order on the user requirements.
consistency of a Constraint Satisfaction Problem w.r.t. a strict total Both approaches can be considered as an optimal repair suggestion
order of the user requirements, I NV QX identifies a diagnosis. Partial w.r.t. their definition of optimum. In this paper, we study both ap-
Weighted M AX SAT aims to find a set of satisfiable clauses with the proaches by giving the following contributions:
maximum total weight. It turns out that both concepts have similari-
ties, i.e., both deliver a correction set. We point out these theoretical 1. We point out theoretical similarities and suggest an improvement
commonalities and prove the reducibility of both concepts to each for I NV QX.
other, i.e., both problems are FPNP -complete, which was an open 2. We show that both problems, the computation of a preferred min-
question. We evaluate the performance on problem instances based imal diagnosis (I NV QX) and the computation of an MCS of min-
on real configuration data of the automotive industry from three dif- imum cardinality (MaxSAT), are reducible to each other and that
ferent German car manufacturers and we compare the time and qual- both are FPNP -complete.
ity tradeoff. 3. We provide experimental evaluations based on real automotive
configuration data.
1 Introduction To the best of our knowledge, it has not been proven before, that
Constraint programming is successfully applied in many different ar- the computation of a preferred minimal diagnosis in the context of
eas, e.g., planning, scheduling, and configuration. Besides the usage Propositional Logic is FPNP -hard.
of Constraint Satisfaction Problem (CSP) based knowledge bases, The remainder of the paper is structured as follows: Section 2 in-
the usage of the more restrictive Propositional Logic has been suc- troduces the formal background. Section 3 discusses related work. In
cessfully established in the context of automotive configuration and Section 4 and Section 5 we introduce both approaches (M IN UNSAT
verification [11]. and I NV QX) and give an overview of solving techniques, respec-
In many practical use cases the knowledge base can become over- tively. Section 6 points out the theoretical relationships and Section 7
constrained, e.g., by overly restrictive rules or user requirements. In shows how to reduce one problem to the other. In Section 8 we
the context of automotive configuration the knowledge base can be- present experimental evaluations. Finally, Section 9 concludes the
come over-constrained, too [23]. A typical situation would be a cus- paper.
tomer configuring a car up to his wishes conflicting with the knowl-
edge base. Another typical situation would be an engineer given the
task that new features should be constructable for an existing type 2 Preliminaries
series by now which were not constructable before. In both situa-
tions we would like to have an automatic reasoning procedure for Within the scope of this paper we focus on Propositional Logic over
assistance in order to restore consistency. the standard operators ¬, ∧, ∨, →, ↔ with constants ⊥ and >, rep-
One approach to restore consistency is to guide the user by com- resenting false and true, respectively. For a Boolean formula ϕ we
puting minimal unsatisfiable cores (conflicts), which can be consid- denote its evaluation by kϕkv ∈ {0, 1} for a variable assignment v.
ered as a problem explanation. However, more than one conflict is A Boolean formula is in CNF normal form iff it consists of a conjunc-
involved in general. Another approach is to try to satisfy as many of tion of clauses, where a clause is a disjunction of literals. A literal is a
the constraints as possible, i.e., finding a maximal satisfiable subset variable or its negation. A formula in CNF can be interpreted as a set
(MSS) or, the opposite, finding a minimum correction subset (MCS) of clauses and further a clause can be interpreted as a set of literals.
which can be considered as a repair suggestion. The constraints of an The NP-complete SAT problem asks whether a Boolean formula is
MCS have to be removed or altered in order to restore consistency. satisfiable or not.
An MCS can be calculated in different ways: (i) M AX SAT is
a generalization of the well-known SAT problem and computes Definition 1. (MSS/MCS) Let ϕ be a set of clauses. A set ψ ⊆ ϕ
is a Maximal Satisfiable Subset (MSS) iff ψ is satisfiable and every
1 Symbolic Computation Group, WSI Informatics, Universität Tübingen,
ψ 0 ⊆ ϕ with ψ ⊂ ψ 0 is unsatisfiable.
Germany, www-sr.informatik.uni-tuebingen.de
2 Institute for Software Technology, Graz University of
A set ψ ⊆ ϕ is a Minimal Correction Subset (MCS) iff ϕ − ψ is
Technology, Graz, Austria, www.felfernig.eu, email: satisfiable and for all ψ 0 ⊆ ϕ with ψ 0 ⊂ ψ the set difference ϕ − ψ 0
alexander.felfernig@ist.tugraz.at is unsatisfiable.
97 Juha Tiihonen, Andreas Falkner and Tomas Axling, Editors
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
The definition of an MSS (resp. MCS) can be naturally extended 4 Preferred Minimal Diagnosis
by taking into account a set of hard clauses which have to be satisfied.
Clearly, for a given MSS (resp. MCS) ψ of ϕ, the complement The definition of a Preferred Minimal Diagnosis (PMD) used in [4]
ϕ − ψ is an MCS (resp. MSS) of ϕ. is in the context of a Constraint Satisfaction Problem (CSP). We will
Analogous to [16] we introduce the following definitions: recap the essential definitions briefly. Let CKB and CR be sets of
CSP constraints. The set CKB (resp. CR ) represents the constraints
Definition 2. (L- and A-Preference) Let < be a strict total order over of the knowledge base (resp. the user requirements).
a set ϕ = {c1 , . . . , cm } of clauses with ci < ci+1 for 1 ≤ i < m,
i.e., clause ci is preferred to clause ci+1 . Definition 3. (CR Diagnosis) Let (CKB , CR ) be a CR diagnosis
We define the lexicographical order wπ(j)
j=i+1
Hard := CKB
then the strict total ordering <π with cπ(1) < . . . < cπ(m) with
Soft := CR CKB = Hard and CR = {cπ(1) , . . . , cπ(m) } is a reduction to the
weight(ci ) := m − (i − 1) A-preferred MCS problem.
With this weight assignment, the most preferred clause is assigned to Proof. The reduction is correct since (1) it preserves the order of
weight m, the next one to weight m − 1 and so on. The lexicograph- the soft clauses w.r.t. their weights and (2) the weights are in such
ical order will be imitated somewhat but not sufficiently to be exact. a relation that for each clause cπ(i) a M IN UNSAT solution will try
The greater the distances of the weights of consecutive constraints ci to satisfy cπ(i) before satisfying all clauses cπ(i+1) , . . . , cπ(m) and
and ci+1 the better the approximation gets. Above we set the distance so will a solution of A-preferred MCS due to the strict total clause
to 1. In Subsection 7.1 we will show how to determine distances that ordering.
help to reach an exact reduction. The transformation can be done in
polynomial time, too. We can check whether such a permutation can be found by: (1)
Sorting soft clauses c1 , . . . , cm in ascending order w.r.t. their weights
Example 2. Consider CR with x ∨ y < ¬x < ¬y < x < z. for complexity O(m log m), (2) Iterating through the sorted list and
The A-preferred MCS is ∆ = {¬y, x}, but M IN UNSAT({(x ∨ checking each clause ci whether the inequality holds for complexity
y, 5), (¬x, 4), (¬y, 3), (x, 2), (z, 1)}) = 4, because ¬x with weight O(m).
4 is less than clauses x and ¬y with weights 2 + 3 = 5. The property of Proposition 1 is sufficient but not necessary. There
are other classes of M IN UNSAT instances without this property
which are reducible in polynomial time, too.
7 Reduction
Example 3. Soft = {(x1 , m), . . . , (xm , 1)}, i.e., a descend-
In this section we will show how to polynomially reduce one problem ing weight for each clause. We assume atMost(x1 , . . . , xm ) ⊆
to each other and finally see that both problems are FPNP -complete Hard, i.e., at most one soft clause is allowed to be true.
and are therefore equally hard to solve. M IN UNSAT will try to satisfy the clause with the highest weight.
The A-preferred MCS problem with the strict total ordering x1 <
7.1 From A-preferred MCS to M IN UNSAT . . . < xm will be a diagnosis which contains clauses except for
the most preferred one in the ordering which can be satisfied un-
Let (CKB , CR ) be an A-preferred MCS problem with CR = der Hard. Since at most one of the clauses can be true, the result
{c1 , . . . , cm } and a total strict order s.t. c1 < . . . < cm . We can is the same.
Juha Tiihonen, Andreas Falkner and Tomas Axling, Editors 100
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
Next we will show the newly result that actually any M IN UNSAT
Table 1. Statistics about the considered POFs
instance is polynomially reducible to the A-preferred MCS problem,
i.e., the A-preferred MCS is FPNP -hard.
Rules Families
Theorem 1. The A-preferred MCS problem is FPNP -hard.
POF #Var. Qty. Avg. #Var. Qty. Avg. #Var.
Proof. Consider the Maximum Satisfying Assignment (MSA) prob- M1_1 996 11,627 5.9 188 6.3
lem: For a Boolean formula ϕ over the variables x1 , . . . , xn find a M1_2 612 4,465 5.3 174 5.3
satisfying assignment with the lexicographical maximum of the word M2_1 483 495 4.3 60 8.7
x1 · · · xn ∈ {0, 1}n or 0 if not satisfiable. This problem is FPNP - M3_1_1 1,772 2,074 33.8 35 56.7
complete as proved in [10]. M3_1_2 1,586 1,496 4.6 35 48.9
We can polynomially reduce the MSA problem to the A-preferred M3_1_3 1,993 2,281 32.9 35 61.6
MCS problem: M3_2_1 2,087 2,430 34.0 42 57.2
M3_3_1 880 1,137 19.6 31 29.3
CKB := Tseitin(ϕ)
M3_3_2 884 1,121 55.1 31 29.4
CR := {{x1 }, . . . , {xn }} M3_3_3 885 1,198 47.8 31 29.4
< := x1 , . . . , xn
8.1 Benchmark Data
Since the Tseitin-transformed formula Tseitin(ϕ) has the same
models on the set of the original variables x1 , . . . , xn as the For our benchmarks we use test instances based on real automotive
original formula ψ (see Remark 1), our reduction is sound. Let configuration data from three different major German car manufac-
APreMCS(CKB , CR ) be the solution of the constructed A-preferred turers. The configuration model of constructable cars is given as a
MCS problem w.r.t. the order <−1 . Using Proposition 12 of [16], the product overview formula (POF) in Propositional Logic [11]. A POF
corresponding L-preferred MSS, which is ϕ−APreMCS(CKB , CR ) is satisfiable and each satisfying assignment represents a valid con-
w.r.t. the order <, is the solution for the MSA problem. Therefore, figurable car. If the POF is over-constrained (unsatisfiable), then no
the A-preferred MCS problem is FPNP -hard. cars are constructable. We denote a POF by Mx_y_z, where each x
is a different car manufacturer, each y is a different type series and
Corollary 1. The A-preferred MCS problem is FPNP -complete.
each z is a different model type. Each satisfying variable assignment
Proof. The A-preferred MCS problem is FPNP -hard (Theorem 1) is a constructable car configuration. Table 1 shows statistics about
and in FPNP [16]. each used POF instance. Column #Var. shows the total variable num-
ber of each instance. Rules are Boolean formulas (not necessarily
Remark 4. With similar arguments one can prove that the L- clauses) describing the dependencies between components. Column
preferred MSS problem is FPNP -complete, too. Assuming P 6= NP, Qty. shows the number of rules and column Avg. #Var. shows the
then FPNP[log n] ⊂ FPNP holds [10]. Hence FPNP -complete prob- average number of variables of a rule. Families are groups of compo-
lems are strictly harder than problems in FPNP[log n] . nents where usually one element has to be chosen, e.g., one motor has
Theorem 1 negatively answers the open question whether com- to be chosen of the family of motors. But the condition of a family
puting L-preferred MSSes and A-preferred MCSes could be in depends on the car manufacturer. Column Qty. shows the number of
FPNP[log n] or not stated in Remark 1 in [16]. families and column Avg. #Var. shows the average number of com-
ponents of a family.
A practical encoding of a M IN UNSAT problem instance as an A- We consider two use cases of re-configuration problems (see [23]
preferred MCS problem could be to encode each soft clause as an for a detailed description of use cases regarding optimization and re-
unit clause with variable si (similiar to Remark 1) and to build the configuration in the context of automotive configuration):
binary representation of the sum:
X • Re-Configuration of Selections: The constraints of the POF are
wi · si = 2l+1 · cl+1 + . . . + 20 · c0 considered as hard constraints. We choose soft user requirements
i
(variables) at random.
Where wi is the weight of the unit soft clause {si }. Then, design Since not all user requirements are consistent w.r.t. the POF in
an adder-network of this sum with the output variables cl+1 , . . . , c0 general, such a random selection easily gets inconsistent. The goal
and set CR := {cl+1 , . . . , c0 }. The strict total order is given by the is to optimize the user selections.
order of the coefficients of the binary representation from the most By this use case we try to realistically imitate a user behavior when
significant bit cl+1 to the least significant bit c0 . Set CKB is the union configuring a custom car.
of the set of the hard clauses, the encoding of the soft clauses as unit • Re-Configuration of Rules: The constraints of the POF are con-
clause and the encoding of the adder-network of the sum. We will sidered as soft constraints. We choose user requirements (vari-
not go into more detail in this work. ables) at random.
Similarly to the previous use case, such a random user selection
easily leads to inconsistency. But in contrast to the previous use
8 Experimental Evaluation
case, we want to optimize the POF constraints instead of the user
We evaluate both problems, the A-preferred MCS problem and the selections.
M IN UNSAT problem, with real industrial datasets from the auto- By this use case we try to realistically imitate, for example, an
motive domain. In the next subsections we describe the benchmark engineering situation where new hard requirements are given and
data and the considered use cases in more detail, afterwards we de- the corresponding engineer wants to be guided by an optimized
scribe the used solver settings and finally discuss the results. repair suggestion to adjust the rules.
101 Juha Tiihonen, Andreas Falkner and Tomas Axling, Editors
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
Table 2. Results of M IN UNSAT use case “Re-Configuration of Selections” (in seconds)
30% 50% 70%
Problem WPM1 msu4 LSB IQB IQBO WPM1 msu4 LSB IQB IQBO WPM1 msu4 LSB IQB IQBO
M1_1 3.19 1.33 0.51 0.47 0.48 t/o 4.97 0.50 0.55 0.49 t/o 47.96 0.51 0.62 0.50
M1_2 2.13 0.04 0.24 0.23 0.20 0.77 0.05 0.23 0.23 0.22 5.20 0.08 0.25 0.24 0.24
M2_1 0.10 0.53 0.09 0.07 0.09 0.11 0.75 0.08 0.07 0.08 0.12 1.08 0.08 0.07 0.08
M3_1_1 1.13 0.53 0.89 1.01 0.89 1.19 0.75 0.95 1.00 1.00 1.24 1.08 0.91 0.98 1.04
M3_1_2 0.12 0.05 0.09 0.07 0.09 0.11 0.07 0.08 0.07 0.08 0.12 0.08 0.08 0.08 0.08
M3_1_3 1.34 0.63 1.16 1.08 1.17 1.36 0.96 1.19 1.09 1.17 1.43 1.30 1.18 1.11 1.15
M3_2_1 1.38 0.71 1.13 1.03 1.16 1.39 0.92 1.21 1.07 1.47 1.48 1.40 1.43 1.05 1.24
M3_3_1 0.88 0.46 1.00 0.75 1.16 0.87 0.45 0.88 0.75 0.94 0.90 0.61 0.89 0.79 0.89
M3_3_2 1.59 0.78 1.60 1.43 1.62 1.57 0.90 1.41 1.46 1.45 1.69 1.41 1.59 1.76 1.46
M3_3_3 1.34 0.63 1.22 1.23 1.18 1.25 0.93 1.18 1.23 1.18 1.31 0.88 1.20 1.22 1.21
Table 3. Results of M IN UNSAT use case “Re-Configuration of Rules” (in seconds)
30% 50% 70%
Problem WPM1 msu4 LSB IQB IQBO WPM1 msu4 LSB IQB IQBO WPM1 msu4 LSB IQB IQBO
M1_1 10.98 t/o 80.45 13.01 4.97 48.15 t/o 79.33 22.16 8.01 31.69 t/o 79.26 25.25 9.32
M1_2 3.24 35.08 7.43 1.78 0.72 4.24 89.95 7.36 2.47 0.89 5.88 64.91 7.10 3.23 1.13
M2_1 0.20 0.11 0.25 0.15 0.16 0.19 0.19 0.25 0.18 0.15 0.23 0.34 0.25 0.19 0.16
M3_1_1 1.88 13.35 9.36 1.97 1.85 2.17 41.86 9.49 2.30 2.04 1.89 14.00 9.13 2.42 2.18
M3_1_2 0.39 0.59 1.48 0.41 0.27 0.50 4.98 1.54 0.55 0.33 0.33 2.15 1.56 0.51 0.34
M3_1_3 2.11 23.69 12.95 2.25 2.08 2.44 59.11 12.32 2.75 2.37 2.17 32.55 12.51 2.84 2.57
M3_2_1 2.40 36.57 11.47 2.56 2.22 2.37 71.15 14.16 2.99 2.50 2.29 65.02 13.95 3.17 2.70
M3_3_1 1.10 2.07 5.14 1.24 1.22 1.18 10.80 5.24 1.49 1.36 1.09 5.26 5.18 1.44 1.36
M3_3_2 2.04 5.92 7.78 2.08 2.10 2.03 14.19 8.76 2.38 2.27 3.08 8.11 8.54 2.30 2.48
M3_3_3 1.58 4.62 6.41 1.79 1.78 1.61 5.54 6.72 1.89 1.83 1.57 6.41 6.73 2.00 1.98
Additionally, we considered three different levels of the user selec- assume a uniform distribution of the soft formulas to simulate the in-
tions: 30%, 50% and 70%. Each level represents the percentage of teraction of the user. For each POF, each use case and each percent-
components chosen from the families, where 100% are all families. age level we created 10 instances to get a reasonable distribution.
By this distinction we want to compare the performance impact of
less configured cars in contrast to highly configured cars. A more 8.2 Implementation Techniques
detailed description of these use cases can be found in [22].
On the M IN UNSAT side we used the following solvers for our eval-
uation:
Table 4. Avg. approx. quality of “Re-Config. of Selections”
• MSU 4: An unsat core-guided approach with iterative SAT calls
using a reduced number of blocking variables [15].
Problem 30% 50% 70%
• WPM1: An unsat core-guided with iterative SAT calls, see Algo-
M1_1 93.39 % 93.60 % 91.78 % rithm 2 and [1]. In each iteration a new blocking variable will be
M1_2 95.79 % 95.94 % 95.76 % added to each soft clause within the unsat core.
M2_1 100 % 99.47 % 98.79 %
M3_1_1 99.43 % 99.29 % 97.61 % Whereas for the A-preferred MCS side we used:
M3_1_2 100 % 100 % 97.49 %
M3_1_3 99.67 % 100 % 96.62 % • LSB: Linear search with backbone improvement plus usage of the
M3_2_1 100 % 98.21 % 96.43 % in-/decremental SAT-Solving interface.
M3_3_1 99.57 % 99.44 % 99.17 % • IQB: Basic I NV QX with backbone improvement plus usage of
M3_3_2 100 % 97.56 % 98.85 % the first part of Remark 2.
M3_3_3 100 % 95.64 % 97.62 % • IQBO: Optimized I NV QX with backbone improvement plus full
usage of Remark 2.
Avg. 98.79 % 97.92 % 97.01 %
Solver MSU 4 is an external one due to [15]. All other solvers were
We consider two problem categories: implemented on top our uniform logic framework, which we use for
commercial applications within the context of automotive configu-
• Category I: M IN UNSAT ration. Our SAT solver provides an inc-/decremental interface. We
• Category II: A-preferred MCS maintain two versions (Java and .NET) and decided to implement
the solvers in C# using .NET 4.0.
For M IN UNSAT the weights were chosen between 1 to 10 by ran- Our experiments were run on the following settings: Processor:
dom and for A-preferred MCS the order was chosen by random. We Intel Core i7-3520M, 2.90 GHz; Main memory: 8GB. All our .NET
Juha Tiihonen, Andreas Falkner and Tomas Axling, Editors 102
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
Table 6. Results of A-preferred MCS use case “Re-Configuration of Selections” (in seconds)
30% 50% 70%
Problem WPM1 msu4 LSB IQB IQBO WPM1 msu4 LSB IQB IQBO WPM1 msu4 LSB IQB IQBO
M1_1 0.76 2.15 0.41 0.41 0.44 – – 0.42 0.47 0.49 – – 0.52 0.56 0.52
M1_2 0.36 0.64 0.18 0.20 0.21 – – 0.19 0.22 0.19 – – 0.26 0.23 0.22
M2_1 0.10 0.05 0.06 0.06 0.06 0.11 0.04 0.06 0.06 0.05 0.11 0.06 0.06 0.07 0.05
M3_1_1 1.20 0.62 0.75 0.81 0.72 1.34 0.88 0.82 0.89 0.73 1.18 1.10 0.76 0.91 0.85
M3_1_2 0.10 0.05 0.06 0.06 0.06 0.11 0.06 0.06 0.06 0.06 0.11 0.08 0.06 0.07 0.06
M3_1_3 1.27 0.69 0.86 0.94 0.86 1.48 0.73 0.87 1.00 0.85 1.42 1.23 0.93 1.03 0.88
M3_2_1 1.31 0.84 0.76 0.98 0.85 1.33 1.10 0.85 0.96 0.84 1.39 1.44 0.93 0.99 0.93
M3_3_1 0.86 0.84 0.59 0.64 0.56 0.88 0.56 0.65 0.65 0.62 0.90 0.64 0.63 0.67 0.67
M3_3_2 1.63 0.83 1.08 1.19 1.07 1.59 1.13 1.07 1.15 1.08 1.62 1.08 1.10 1.17 1.09
M3_3_3 1.28 0.66 0.91 0.93 0.88 1.26 0.86 0.86 0.96 0.92 1.27 1.18 0.93 0.98 0.94
Table 7. Results of A-preferred MCS use case “Re-Configuration of Rules” (in seconds)
30% 50% 70%
Problem LSB IQB IQBO LSB IQB IQBO LSB IQB IQBO
M1_1 77.00 10.69 3.65 73.83 17.95 6.14 73.75 19.90 7.31
M1_2 6.40 1.54 0.56 6.30 1.81 0.67 5.96 2.12 0.81
M2_1 0.22 0.14 0.11 0.22 0.15 0.12 0.22 0.18 0.14
M3_1_1 8.41 1.88 1.62 8.10 2.05 1.63 8.35 2.12 1.71
M3_1_2 1.36 0.33 0.20 1.33 0.46 0.24 1.38 0.49 0.28
M3_1_3 11.03 1.95 1.69 11.04 2.34 1.94 11.53 2.35 2.07
M3_2_1 9.87 2.20 1.79 12.48 2.51 2.11 12.12 2.69 2.14
M3_3_1 4.24 1.19 1.02 4.29 1.31 1.08 4.46 1.34 1.16
M3_3_2 6.79 2.01 1.66 7.25 2.06 1.79 7.05 2.10 1.95
M3_3_3 5.41 1.61 1.42 5.65 1.68 1.55 5.70 1.79 1.61
based algorithms run under Windows 7 while MSU 4 runs under
Ubuntu 12.04.
8.3 Results
For all of the following result tables, each table entry shows the av-
erage time in seconds a solver needed to solve 10 different instances
of the considered use case and POF. We set a timeout (t/o) of 600
Table 5. Avg. approx. quality of “Re-Configuration of Rules” seconds. Each table is separated in three levels (30%, 50% and 70%)
which is the percentage of families where user selections were made
from.
Problem 30% 50% 70%
M1_1 99.90 % 99.91 % 99.93 %
8.3.1 Category I: Partial Weighted M IN UNSAT
M1_2 99.94 % 99.94 % 99.86 %
M2_1 99.82 % 99.56 % 99.70 % Table 2 and Table 3 show the results of both use cases, respectively.
M3_1_1 100 % 99.98 % 100 % MSU 4 performs well on the first use case, whereas IQBO performs
M3_1_2 100 % 99.96 % 99.99 % most often best on the second use case.
M3_1_3 99.98 % 99.99 % 99.99 % Table 4 and Table 5 show the average approximation quality of the
M3_2_1 100 % 99.99 % 99.97 % A-preferred MCS approaches used as M IN UNSAT approximation
M3_3_1 99.95 % 99.89 % 99.99 % (cf. Subsection 6.1), which turns out to be quite good. Percentage p
M3_3_2 99.96 % 99.94 % 99.97 % is calculated as follows:
M3_3_3 99.97 % 99.98 % 99.95 % ( m wi ) − approxOpt
P
p = Pi=1
Avg. 99.95 % 99.91 % 99.94 % ( m
i=1 wi ) − exactOpt
Where approxOpt is the optimum of the A-preferred MCS solver
and exactOpt is the optimum of the M IN UNSAT solver.
8.3.2 Category II: A-preferred MCS
Table 6 does not contain entries for M1_1 and M1_2 in the columns
50% and 70% because the encoding of the weights exceeds the
103 Juha Tiihonen, Andreas Falkner and Tomas Axling, Editors
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
native long data type. The MaxSAT competition format3 permits [4] Alexander Felfernig, Monika Schubert, and Christoph Zehentner, ‘An
efficient diagnosis algorithm for inconsistent constraint sets’, Artifi-
a top weight lower than 263 . Table 7 is missing an evaluation for
cial Intelligence for Engineering Design, Analysis, and Manufacturing,
M IN UNSAT solvers for the same reason. 26(1), 53–62, (February 2012).
For instances where an encoding is possible, both M IN UNSAT [5] Zhaohui Fu and Sharad Malik, ‘On solving the partial MAX-SAT prob-
solvers can keep up with the native A-preferred MCS solvers. IQBO lem’, in Theory and Applications of Satisfiability Testing—SAT 2006,
performs significantly better than IQB for the second use case. eds., Armin Biere and Carla P. Gomes, volume 4121 of Lecture Notes
in Computer Science, 252–265, Springer Berlin Heidelberg, (2006).
[6] Federico Heras, António Morgado, and João Marques-Silva, ‘Core-
guided binary search algorithms for maximum satisfiability’, in AAAI,
9 Conclusions and Future Work eds., Wolfram Burgard and Dan Roth, pp. 36 – 41. AAAI Press, (Au-
gust 2011).
In this work, we compared the problem of finding a minimal pre- [7] Federico Heras, António Morgado, and João Marques-Silva, ‘An empir-
ferred diagnosis (A-preferred MCS in the context of Propositional ical study of encodings for group MaxSAT’, in Canadian Conference
Logic) with the problem of finding a diagnosis of minium cardinal- on AI, eds., Leila Kosseim and Diana Inkpen, volume 7310 of Lecture
Notes in Computer Science, pp. 85–96. Springer, (2012).
ity (M IN UNSAT in the context of Propositional Logic). We proved
[8] Federico Heras, António Morgado, and João Marques-Silva, ‘Lower
the FPNP -hardness of the A-preferred MCS problem and therefore bounds and upper bounds for MaxSAT’, in Learning and Intelligent
showed, that both problems are equally hard to solve and reducible Optimization – 6th International Conference, LION 6, Paris, France,
to each other. January 16-20, 2012, Revised Selected Papers, eds., Youssef Hamadi
Both optimization approaches (A-preferred MCS and and Marc Schoenauer, volume 7219 of Lecture Notes in Computer Sci-
ence, pp. 402–407. Springer Berlin Heidelberg, (2012).
M IN UNSAT) complement each other. For use cases which [9] Ulrich Junker, ‘QUICKXPLAIN: Preferred explanations and relax-
can be expressed as an A-preferred MCS problem one should use ations for over-constrained problems’, in Proceedings of the 19th Na-
I NV QX as solving engine. For the other use cases, one should use tional Conference on Artificial Intelligence, pp. 167–172. AAAI Press
M IN UNSAT. / The MIT Press, (2004).
[10] Mark W. Krentel, ‘The complexity of optimization problems’, Journal
For instances where M IN UNSAT is not able to find the solution
of Computer and System Sciences, 36(3), 490–509, (June 1988).
in within a reasonable time or where fast responses are needed, we [11] Wolfgang Küchlin and Carsten Sinz, ‘Proving consistency assertions
can fall back to I NV QX if an approximated answer is reasonable for for automotive product data management’, Journal of Automated Rea-
the considered use case. soning, 24(1–2), 145–163, (2000).
We evaluated the performance of both problems with benchmarks [12] Adrian Kügel, ‘Improved exact solver for the weighted MAX-SAT
problem’, in POS-10. Pragmatics of SAT, ed., Daniel Le Berre, vol-
based on real automotive configuration data. We assumed a uniform ume 8 of EasyChair Proceedings in Computing, pp. 15–27. EasyChair,
distribution of the soft formulas to simulate the interaction of the (2012).
user. These benchmarks can be improved by choosing a more realis- [13] Chu Min Li and Felip Manyà, ‘MaxSAT, hard and soft constraints’, in
tic distribution of the soft formulas. Handbook of Satisfiability, eds., Armin Biere, Marijn Heule, Hans van
Maaren, and Toby Walsh, volume 185 of Frontiers in Artificial Intelli-
For an exhaustive evaluation of both problems, we need to con-
gence and Applications, chapter 19, 613–631, IOS Press, (2009).
sider more complex benchmark data, e.g. unsatisfiable instances of [14] João Marques-Silva, Federico Heras, Mikoláš Janota, Alessandro
the SAT4 or MaxSAT5 competitions. Also, we need to evaluate all Previti, and Anton Belov, ‘On computing minimal correction subsets.’,
solvers based on the same SAT solving engine, i.e. M INI SAT [3], in in IJCAI, ed., Francesca Rossi, pp. 615–622. IJCAI/AAAI, (2013).
order to build up an uniform environment. [15] João Marques-Silva and Jordi Planes, ‘Algorithms for maximum satis-
fiability using unsatisfiable cores’, in Proceedings of the Conference on
Another interesting evaluation could be the reduction of the Design, Automation and Test in Europe, DATE ’08, pp. 408–413. IEEE,
M IN UNSAT problem to an A-preferred MCS problem by using an (2008).
adder-network encoding as described in Subsection 7.2. With such an [16] João Marques-Silva and Alessandro Previti, ‘On computing preferred
encoding, we could use every A-preferred MCS solver, like I NV QX, MUSes and MCSes’, in Theory and Applications of Satisfiability Test-
ing – SAT 2014, eds., Carsten Sinz and Uwe Egly, volume 8561 of
to solve M IN UNSAT problem instances.
Lecture Notes in Computer Science, pp. 58–74. Springer International
I NV QX and M IN UNSAT in their original form compute only a Publishing, (July 2014).
single diagnosis. Both approaches can be extended to compute a set [17] Carlos Mencı́a and João Marques-Silva, ‘Efficient relaxations of over-
of all diagnoses. We plan to investigate the relationship of these ex- constrained CSPs’, in 2014 IEEE 26th International Conference on
tensions and to evaluate them, too. Tools with Artificial Intelligence, pp. 725–732. IEEE, (2014).
[18] António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and
João Marques-Silva, ‘Iterative and core-guided MaxSAT solving: A
survey and assessment.’, Constraints, 18(4), 478–534, (2013).
REFERENCES [19] Christos M. Papadimitriou, Computational complexity, Addison-
Wesley, Reading, Massachusetts, 1994.
[1] Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy, ‘Solving
[20] David A. Plaisted and Steven Greenbaum, ‘A structure-preserving
(weighted) partial MaxSAT through satisfiability testing’, in Theory
clause form translation’, Journal of Symbolic Computation, 2(3), 293–
and Applications of Satisfiability Testing - SAT 2009, ed., Oliver Kull-
304, (September 1986).
mann, volume 5584 of Lecture Notes in Computer Science, 427–440,
[21] Grigorii S. Tseitin, ‘On the complexity of derivations in the proposi-
Springer Berlin Heidelberg, (2009).
tional calculus’, Studies in Constructive Mathematics and Mathemati-
[2] Josep Argelich and Felip Manyà, ‘Exact Max-SAT solvers for over-
cal Logic, Part II, 115–125, (1968).
constrained problems.’, Journal of Heuristics, 12(4–5), 375–392,
[22] Rouven Walter and Wolfgang Küchlin, ‘ReMax – a MaxSAT aided
(September 2006).
product configurator’, in Proceedings of the 16th International Configu-
[3] Niklas Eén and Niklas Sörensson, ‘An extensible SAT-solver’, in The-
ration Workshop, eds., Alexander Felfernig, Cipriano Forza, and Albert
ory and Applications of Satisfiability Testing—SAT 2003, eds., Enrico
Haag, pp. 59–66, Novi Sad, Serbia, (September 2014).
Giunchiglia and Armando Tacchella, volume 2919 of Lecture Notes in
[23] Rouven Walter, Christoph Zengler, and Wolfgang Küchlin, ‘Applica-
Computer Science, 502–518, Springer Berlin Heidelberg, (2004).
tions of MaxSAT in automotive configuration’, in Proceedings of the
3 www.maxsat.udl.cat/13/requirements/index.html
15th International Configuration Workshop, eds., Michel Aldanondo
4 http://www.satcompetition.org/
and Andreas Falkner, pp. 21–28, Vienna, Austria, (August 2013).
5 www.maxsat.udl.cat
Juha Tiihonen, Andreas Falkner and Tomas Axling, Editors 104
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria