We compare the concepts of the INVQX algorithm for computing a Preferred Minimal Diagnosis vs. Partial Weighted MAXSAT in the context of Propositional Logic. In order to restore consistency of a Constraint Satisfaction Problem w.r.t. a strict total order of the user requirements, INVQX identifies a diagnosis. Partial Weighted MAXSAT aims to find a set of satisfiable clauses with the maximum total weight. It turns out that both concepts have similarities, i.e., both deliver a correction set. We point out these theoretical commonalities and prove the reducibility of both concepts to each other, i.e., both problems are FPNP-complete, which was an open question. We evaluate the performance on problem instances based on real configuration data of the automotive industry from three different German car manufacturers and we compare the time and quality tradeoff.
Constraint programming is successfully applied in many different
areas, e.g., planning, scheduling, and configuration. Besides the usage
of Constraint Satisfaction Problem (CSP) based knowledge bases,
the usage of the more restrictive Propositional Logic has been
successfully established in the context of automotive configuration and
verification [
In many practical use cases the knowledge base can become
overconstrained, e.g., by overly restrictive rules or user requirements. In
the context of automotive configuration the knowledge base can
become over-constrained, too [
One approach to restore consistency is to guide the user by computing minimal unsatisfiable cores (conflicts), which can be considered as a problem explanation. However, more than one conflict is involved in general. Another approach is to try to satisfy as many of the constraints as possible, i.e., finding a maximal satisfiable subset (MSS) or, the opposite, finding a minimum correction subset (MCS) which can be considered as a repair suggestion. The constraints of an MCS have to be removed or altered in order to restore consistency.
An MCS can be calculated in different ways: (i) MAXSAT is
a generalization of the well-known SAT problem and computes
the MCS of minimum cardinality; (ii) the Inverse QUICKXPLAIN
(INVQX) algorithm (also denoted as FASTDIAG) [
To the best of our knowledge, it has not been proven before, that the computation of a preferred minimal diagnosis in the context of
The remainder of the paper is structured as follows: Section 2 introduces the formal background. Section 3 discusses related work. In Section 4 and Section 5 we introduce both approaches (MINUNSAT and INVQX) and give an overview of solving techniques, respectively. Section 6 points out the theoretical relationships and Section 7 shows how to reduce one problem to the other. In Section 8 we present experimental evaluations. Finally, Section 9 concludes the paper. 2
Within the scope of this paper we focus on Propositional Logic over the standard operators :; ^; _; !; $ with constants ? and >, representing false and true, respectively. For a Boolean formula ' we denote its evaluation by k'kv 2 f0; 1g for a variable assignment v. A Boolean formula is in CNF normal form iff it consists of a conjunction of clauses, where a clause is a disjunction of literals. A literal is a variable or its negation. A formula in CNF can be interpreted as a set of clauses and further a clause can be interpreted as a set of literals. The NP-complete SAT problem asks whether a Boolean formula is satisfiable or not.
Definition 1. (MSS/MCS) Let ' be a set of clauses. A set ' is a Maximal Satisfiable Subset (MSS) iff is satisfiable and every 0 ' with 0 is unsatisfiable.
A set ' is a Minimal Correction Subset (MCS) iff ' is satisfiable and for all 0 ' with 0 the set difference ' 0 is unsatisfiable.
The definition of an MSS (resp. MCS) can be naturally extended by taking into account a set of hard clauses which have to be satisfied.
Clearly, for a given MSS (resp. MCS) of ', the complement ' is an MCS (resp. MSS) of '.
Analogous to [
We define the lexicographical order <lex as follows: For two sets 1; 2 ' we say set 1 is lexicographically preferred to 2, denoted as 2 and 1 <lex 2, iff 91 k m : ck 2 1 1 \ fc1; : : : ; ck 1g = 2 \ fc1; : : : ; ck 1g.
Furthermore, we define the anti-lexicographical order <antilex as follows: For two sets 1; 2 ' we say set 1 is antilexicographically preferred to 2, denoted as 2, iff 2 1 and
1 <antilex 1 \ fck+1; : : : ; cmg = 1 is L-preferred (resp. A-preferred) if for all 1, 1 <lex 2 (resp. 1 <antilex 2).
The lexicographical order appears to be the more intuitive one. Whereas the most L-preferred set includes the most preferred clauses, the most A-preferred set excludes the most non-preferred clauses. We denote the inverse order of < by < 1.
If is an L-preferred (resp. A-preferred) MSS/MCS of ' w.r.t. to the order < , then ' is an A-preferred (resp. L-preferred)
in [
Note that we use the standard notation for the complexity class
deterministic polynomial time using a polynomial (resp. logarithmic)
number of calls to an NP oracle [
The authors of [
The INVQX algorithm (also known as FASTDIAG) [
The complexity of computing preferred sets is studied in [
The authors of [
The definition of a Preferred Minimal Diagnosis (PMD) used in [
Definition 3. (CR Diagnosis) Let (CKB; CR) be a CR diagnosis problem. A set CR is a CR Diagnosis if CKB [ (CR n ) is consistent. Furthermore, is called minimal if no diagnosis 0 exists where CKB [ (CR n 0) is consistent.
In the context of Propositional Logic a CR diagnosis corresponds to the MCS problem with an additional hard part. The definitions for L- and A-Preference can analogously be defined for CSP. We will not write them out here.
Finally, we can define a preferred minimal diagnosis: Definition 4. (Preferred Minimal Diagnosis) Let (CKB; CR = fc1; : : : ; cmg) be a CR diagnosis problem with a strict total order s.t. c1 < : : : < cm. A minimal diagnosis is called a Preferred Minimal Diagnosis (PMD) if is A-preferred w.r.t. the order < 1.
The strict total order in [
Remark 1. In the context of Propositional Logic we assume, without
loss of generality, that CKB and CR are clause sets:
1. CR: Let si be a fresh variable. For each constraint ci 2 CR we
add the clause set CNF(si ! ci) to the hard part and the unit
clause fsig replaces ci within CR (cf. [
question arises whether computing an A-preferred MCS is also
4.1
A straightforward approach is Linear Search. We iterate in descending order through all constraints and check whether they conflict with the hard constraints and the previously added constraints or not. If there is a conflict, the constraint is part of the A-preferred MCS. Otherwise, the constraint will be added. The complexity of Linear
m = jCj.
Algorithm 1 shows the procedure presented in [
Remark 2. (Exploiting inc-/decremental SAT interface) Modern SAT solvers often provide an inc-/decremental interface for adding clauses and removing them afterwards. This can be useful, e.g., when Algorithm 1: INVQX Algorithm Input: C AC, AC = fc1; : : : ; ctg Output: Preferred minimal diagnosis if isEmpty(C) or inconsistent(AC
return ; else return FD(;; C; AC) C) then we have a huge formula representing the configuration model and small test instances to check against the configuration model.
Therefore we can improve Algorithm 1 by adding all constraints AC C first and do the consistency checks by using the inc/decremental interface. Another improvement can be made for the second recursive call D2 = FD(D1; C1; AC D1). All constraints in C2 D1 have to be satisfied for this call. We add all constraints C2 D1 before and remove them afterwards. We evaluated this improvement, see Section 8.
Definition 5. (MINUNSAT) Let Hard be a set of propositional clauses. Let Soft = f(c1; w1); : : : ; (cm; wm)g a set of tuples where ci is a propositional clause and wi 2 N 1 is a weight for all i = 1; : : : ; m. Let ' = (Hard; Soft) and n be the number of variables in Hard [ Soft. The Partial Weighted Minimum Unsatisfiable Problem (MINUNSAT) is defined as follows:
MINUNSAT(') := min ( m
X wi(1 i=1 kcikv) v 2 f0; 1gn )
Partial Weighted MINUNSAT and Partial Weighted MAXSAT are closely connected: MaxSAT(Hard; Soft) = Pim=1 wi MINUNSAT(Hard; Soft). A solution for one problem directly leads to a solution for the other one and vice verca. The Partial Weighted
The unweighted (partial) MAXSAT (resp. MINUNSAT) problem is
In the context of this paper, we will refer to Partial Weighted MINUNSAT just as MINUNSAT to simplify reading. Please note that in the literature often the name MAXSAT is used to refer to MINUNSAT. But we will use its original name to make the dinstinction clear. 5.1
MINUNSAT solvers make use of SAT solvers as a black box. A
basic approach is to add a blocking variable to each soft clause,
iteratively checking the instance for satisfiability and restricting the
blocking variables further each time. Also binary search is possible
this way. Nowadays solvers make usage of SAT solvers delivering an
unsatisfiable core, which was first presented in [
Algorithm 2: WPM1 Algorithm Input: (Hard; Soft = f(c1; w1) : : : ; (cm; wm)g) Output: Sum of minimal unsatisfied weights: cost if UNSAT(Hard) then
return No solution cost 0 while true do (st; 'c) SAT(Hard [ f(ci; wi) 2 Softg) if st = SAT then
return cost BV
; wmin minfwi j ci 2 'c ^ ci is softg foreach ci 2 'c \ Soft do bi fresh blocking variable Soft Soft BV f(ci; wi)g[f(ci; wi
BV [ fbig Hard cost
Hard [ CNF(Pb2BV b = 1) cost + wmin wmin)g[f(ci _bi; wmin)g 6
We want to identify and discuss similarities of the PMD problem and the MINUNSAT problem. As we have already shown in Remark 1 in the context of Propositional Logic the PMD problem can be interpreted as an A-preferred MCS problem. The hard parts of both problems are equal in terms of expressive power, since both are sets of clauses.
The interesting part is the set CR with its strict total ordering < and the set Soft of weighted clauses. Both can be defined as a special case of an MCS problem: The PMD problem can be interpreted as an A-preferred MCS problem (cf. Remark 1):
min fS j S is MCS of CR w.r.t. CKBg <an1tilex Whereas the MINUNSAT problem is also an MCS with the minimum sum of weights:
min Pc2S weight(c)
S S is MCS of Soft w.r.t. Hard Where weight(c) denotes the weight of clause c.
Different approaches to solve the MINUNSAT problem have been
developed: Branch-and-Bound for general optimization problems
has been adopted to MINUNSAT, e.g., [
Solvers for the A-preferred MCS problem can be used to approximate the MINUNSAT problem. Let be a permutation of the indices 1; : : : ; m such that the weights are sorted, i.e., if i < j then w (i) < w (j). We set:
CKB := Hard
CR := Soft
< := c (1); : : : ; c (m) This transformation is actually an approximation: An A-preferred MCS will prefer to satisfy a clause with a high weight value more than to satisfy multiple clauses with low weight values. Whereas a MINUNSAT solution will minimize the sum of the weights of unsatisfied clauses in total. The transformation can be done in polynomial time: We sort the clauses w.r.t. their weights, which can be done in
this approximation, see Section 8.
Example 1. Consider Hard = ; and Soft = f(x; 6); (:x _ y; 5); (:y; 4); (:x; 3)g. With a strict total ordering relying on the weights of the soft clauses (see above), the A-preferred MCS is = f(:y; 4); (:x; 3)g resulting in costs of 7. But the MINUNSAT solution f(x; 6)g has costs of 6. 6.2
We can also use MINUNSAT to approximate the A-preferred MCS problem. The crucial question is which weights to assign to the soft clauses. We can assume CR to be a set of clauses, see Remark 1. We set:
Hard := CKB
Soft := CR weight(ci) := m (i 1) With this weight assignment, the most preferred clause is assigned to weight m, the next one to weight m 1 and so on. The lexicographical order will be imitated somewhat but not sufficiently to be exact. The greater the distances of the weights of consecutive constraints ci and ci+1 the better the approximation gets. Above we set the distance to 1. In Subsection 7.1 we will show how to determine distances that help to reach an exact reduction. The transformation can be done in polynomial time, too.
Example 2. Consider CR with x _ y < :x < :y < x < z. The A-preferred MCS is = f:y; xg, but MINUNSAT(f(x _ y; 5); (:x; 4); (:y; 3); (x; 2); (z; 1)g) = 4, because :x with weight 4 is less than clauses x and :y with weights 2 + 3 = 5. 7
In this section we will show how to polynomially reduce one problem to each other and finally see that both problems are FPNP-complete and are therefore equally hard to solve. 7.1
Let (CKB ; CR) be an A-preferred MCS problem with CR = fc1; : : : ; cmg and a total strict order s.t. c1 < : : : < cm. We can assume CR to be a set of clauses, see Remark 1. We can reduce the problem to a MINUNSAT problem by: with weight wi defined recursively:
Hard := CKB
Soft := CR wi := m X j=i+1
! wj + 1 With these weights assigned we achieve two important properties: (1) the ascending order of the constraints ci and more important (2) the lexicographical ordering, because constraint ci with weight Pm
j=i+1 wj + 1 = wi+1 + : : : + wm + 1 is greater than the sum of weights of all previous and less preferred constraints ci+1; : : : ; cm.
Each step requires polynomial time. But the downside of the above reduction is the exponential growth of the search space. It can be shown by induction that (Pm
j=i+1 wj ) + 1 = 2m i. The most preferred clause has weight 2m 1, so the weights are in O(2m). 7.2
Firstly, we show how we can reduce the MINUNSAT problem easily to the A-preferred MCS problem if the weights comply with the following property: Proposition 1. Let ' = (Hard; Soft) be a MINUNSAT problem as defined in Definition 5 with Soft = f(c1; w1); : : : ; (cm; wm)g. If there exists a permutation of the indices f1; : : : ; mg such that: w (i) >
w (j) m X j=i+1 then the strict total ordering < with c (1) < : : : < c (m) with CKB = Hard and CR = fc (1); : : : ; c (m)g is a reduction to the A-preferred MCS problem.
Proof. The reduction is correct since (1) it preserves the order of the soft clauses w.r.t. their weights and (2) the weights are in such a relation that for each clause c (i) a MINUNSAT solution will try to satisfy c (i) before satisfying all clauses c (i+1); : : : ; c (m) and so will a solution of A-preferred MCS due to the strict total clause ordering.
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 for complexity O(m log m), (2) Iterating through the sorted list and checking each clause ci whether the inequality holds for complexity O(m).
The property of Proposition 1 is sufficient but not necessary. There are other classes of MINUNSAT instances without this property which are reducible in polynomial time, too.
Example 3. Soft = f(x1; m); : : : ; (xm; 1)g, i.e., a descending weight for each clause. We assume atMost(x1; : : : ; xm) Hard, i.e., at most one soft clause is allowed to be true. MINUNSAT will try to satisfy the clause with the highest weight. The A-preferred MCS problem with the strict total ordering x1 < : : : < xm will be a diagnosis which contains clauses except for the most preferred one in the ordering which can be satisfied under Hard. Since at most one of the clauses can be true, the result is the same.
Next we will show the newly result that actually any MINUNSAT instance is polynomially reducible to the A-preferred MCS problem, i.e., the A-preferred MCS is FPNP-hard.
Theorem 1. The A-preferred MCS problem is FPNP-hard.
Proof. Consider the Maximum Satisfying Assignment (MSA)
problem: For a Boolean formula ' over the variables x1; : : : ; xn find a
satisfying assignment with the lexicographical maximum of the word
x1 xn 2 f0; 1gn or 0 if not satisfiable. This problem is
FPNPcomplete as proved in [
We can polynomially reduce the MSA problem to the A-preferred MCS problem:
CKB := Tseitin(')
CR := ffx1g; : : : ; fxngg
< := x1; : : : ; xn Since the Tseitin-transformed formula Tseitin(') has the same models on the set of the original variables x1; : : : ; xn as the original formula (see Remark 1), our reduction is sound. Let APreMCS(CKB; CR) be the solution of the constructed A-preferred
corresponding L-preferred MSS, which is ' APreMCS(CKB; CR) w.r.t. the order <, is the solution for the MSA problem. Therefore, the A-preferred MCS problem is FPNP-hard.
Corollary 1. The A-preferred MCS problem is FPNP-complete.
Remark 4. With similar arguments one can prove that the
Lpreferred MSS problem is FPNP-complete, too. Assuming P 6= NP,
then FPNP[log n] FPNP holds [
Theorem 1 negatively answers the open question whether
computing L-preferred MSSes and A-preferred MCSes could be in
FPNP[log n] or not stated in Remark 1 in [
A practical encoding of a MINUNSAT problem instance as an Apreferred MCS problem could be to encode each soft clause as an unit clause with variable si (similiar to Remark 1) and to build the binary representation of the sum:
X wi si = 2l+1 cl+1 + : : : + 20 c0
i Where wi is the weight of the unit soft clause fsig. Then, design an adder-network of this sum with the output variables cl+1; : : : ; c0 and set CR := fcl+1; : : : ; c0g. The strict total order is given by the order of the coefficients of the binary representation from the most significant bit cl+1 to the least significant bit c0. Set CKB is the union of the set of the hard clauses, the encoding of the soft clauses as unit clause and the encoding of the adder-network of the sum. We will not go into more detail in this work. 8
We evaluate both problems, the A-preferred MCS problem and the
MINUNSAT problem, with real industrial datasets from the
automotive domain. In the next subsections we describe the benchmark
data and the considered use cases in more detail, afterwards we
describe the used solver settings and finally discuss the results.
For our benchmarks we use test instances based on real automotive
configuration data from three different major German car
manufacturers. The configuration model of constructable cars is given as a
product overview formula (POF) in Propositional Logic [
We consider two use cases of re-configuration problems (see [
Since not all user requirements are consistent w.r.t. the POF in general, such a random selection easily gets inconsistent. The goal is to optimize the user selections.
By this use case we try to realistically imitate a user behavior when configuring a custom car.
Re-Configuration of Rules: The constraints of the POF are considered as soft constraints. We choose user requirements (variables) at random.
Similarly to the previous use case, such a random user selection easily leads to inconsistency. But in contrast to the previous use case, we want to optimize the POF constraints instead of the user selections.
By this use case we try to realistically imitate, for example, an
engineering situation where new hard requirements are given and
the corresponding engineer wants to be guided by an optimized
repair suggestion to adjust the rules.
Additionally, we considered three different levels of the user
selections: 30%, 50% and 70%. Each level represents the percentage of
components chosen from the families, where 100% are all families.
By this distinction we want to compare the performance impact of
less configured cars in contrast to highly configured cars. A more
detailed description of these use cases can be found in [
IQB 0.55 0.23 0.07 1.00 0.07 1.09 1.07 0.75 1.46 1.23
IQBO native long data type. The MaxSAT competition format3 permits a top weight lower than 263. Table 7 is missing an evaluation for MINUNSAT solvers for the same reason.
For instances where an encoding is possible, both MINUNSAT solvers can keep up with the native A-preferred MCS solvers. IQBO performs significantly better than IQB for the second use case. 9
In this work, we compared the problem of finding a minimal preferred diagnosis (A-preferred MCS in the context of Propositional Logic) with the problem of finding a diagnosis of minium cardinality (MINUNSAT in the context of Propositional Logic). We proved the FPNP-hardness of the A-preferred MCS problem and therefore showed, that both problems are equally hard to solve and reducible to each other.
Both optimization approaches (A-preferred MCS and MINUNSAT) complement each other. For use cases which can be expressed as an A-preferred MCS problem one should use INVQX as solving engine. For the other use cases, one should use MINUNSAT.
For instances where MINUNSAT is not able to find the solution in within a reasonable time or where fast responses are needed, we can fall back to INVQX if an approximated answer is reasonable for the considered use case.
We evaluated the performance of both problems with benchmarks based on real automotive configuration data. We assumed a uniform distribution of the soft formulas to simulate the interaction of the user. These benchmarks can be improved by choosing a more realistic distribution of the soft formulas.
For an exhaustive evaluation of both problems, we need to
consider more complex benchmark data, e.g. unsatisfiable instances of
the SAT4 or MaxSAT5 competitions. Also, we need to evaluate all
solvers based on the same SAT solving engine, i.e. MINISAT [
Another interesting evaluation could be the reduction of the MINUNSAT problem to an A-preferred MCS problem by using an adder-network encoding as described in Subsection 7.2. With such an encoding, we could use every A-preferred MCS solver, like INVQX, to solve MINUNSAT problem instances.
INVQX and MINUNSAT in their original form compute only a single diagnosis. Both approaches can be extended to compute a set of all diagnoses. We plan to investigate the relationship of these extensions and to evaluate them, too. 104