On Exact Selection of Minimally Unsatisfiable Subformulae.
A minimally unsatisfiable subformula (MUS) is a subset of clauses of a given CNF formula which is unsatisfiable but becomes satisfiable as soon as any of its clauses is removed. The selection of a MUS is of great relevance in many practical applications. This expecially holds when the propositional formula encoding the application is required to have a well-defined satisfiability property (either to be satisfiable or to be unsatisfiable). While selection of a MUS is a hard problem in general, we show classes of formulae where this problem can be solved efficiently. This is done by using a variant of Farkas' lemma and solving a linear programming problem. Successful results on real-world contradiction detection problems are presented.
The satis?ability problem (SAT) consists in determining whether there
exists a truth assignment {True,False} for the variables such that F
evaluates to True. Extensive references can be found in (Chandru and
Hooker, 1999; Gu et al., 1997; Kleine Bu?ning and Lettman, 1999;
Truemper, 1998).
Generally, when an instance F encodes a system or a structure one
must design, F should have a well-de?ned solution property (either to
be satis?able or to be unsatis?able). When F is unsatis?able, but it
should be satis?able, we would like to modify the underlying system
in order to make F satis?able. Conversely, when F is unsatis?able and
it should be so, if the underlying system needs to be re-designed, we
would like to keep F unsatis?able. The ?rst problem can sometimes be
c Kluwer Academic Publishers. Printed in the Netherlands.
approached by solving the maximum satis?ability problem (Max-SAT),
see e.g. (Battiti and Protasi, 1998). This consists in ?nding a truth
assignment for the variables maximizing the number of clauses Cj which
evaluates to True. So far, satis?ability can be restored by removing
from the underlying system all elements corresponding to clauses which
could not be satis?ed. However, such approach is not desirable in many
practical cases. Very often, in fact, we cannot just delete a part of our
system, because we need the functionalities contained in that part.
Instead, we would like to locate and understand the problem, and,
basing on this information, re-design only the small part of the system
causing the problem. As for the second problem, we typically would like
to know which part of the underlying system should not be changed,
and which one can be modi?ed (or possibly removed). Both of the above
problems can be approached by looking for a minimally unsatis?able
subset of clauses (MUS) within an unsatis?able F (see Sect. 2).
An algorithm for selecting an approximation of a MUS is proposed
in (Bruni, 2002). The problem of deciding whether a CNF formula
contains a minimally unsatis?able (MU) subformula of ?xed de?ciency
?, for all ?, is proved NP-complete in (Kleine Bu?ning and Zhao, 2002).
Related works in the ?eld of propositional formulae are those on decomposition
of a CNF with maximal de?ciency ? ? k (where k is a
constant) into the union of all MUS and the intersection of all maximally
satis?able subformulae in polynomial time (Kullmann, 2000), and
on recognition of MU formulae with ?xed de?ciency ? in polynomial
time (Fleischner et al., 2002).
The problem of the selection of an irreducible infeasible subsystem
(IIS), which is the analogous of a MUS in the case of systems of linear
inequalities, has been studied with regard to infeasibility analysis
(Amaldi et al., 1999; Chinneck, 2001; Tamiz et al., 1996). In the case
of systems of linear inequalities having real variables, the problem has
been approached both by means of heuristics (Chinneck, 2001) and
exact algorithms (Gleeson and Ryan, 1990). In the case of systems
of linear inequalities having integer variables (more computationally
demanding), the problem has been approached by means of additive or
subtractive heuristics (Guieu and Chinneck, 1999).
A procedure for the exact selection of a MUS is here presented (Sect.
4). It is based on Farkas? lemma (Sect. 3) adapted from the linear
to the binary case. While selection of a MUS is a hard problem in
general, we show (Sect. 5) classes of formulae for which this can be done
e?ciently by solving a linear programming problem. This depends on
the structure of the polytope de?ned by the linear relaxation of SAT.
A compendium of studies on such structure is for instance in (Chandru
and Hooker, 1999). This procedure is applied to real-world data mining
exact.tex; 1/04/2003; 14:40; p.
Exact Selection of Minimally Unsatis?able Subformulae 3
problems (Sect. 6), where logical rules are encoded into clauses (Bruni
and Sassano, 2001). A contradiction in the set of rules corresponds to a
set of clauses jointly unsatis?able. Checking the rules for inconsistencies
produces a series of MUS selection problems, where all the con?icting
rules should be located, and it would not help deleting some of them.
2. Minimally Unsatis?able Subformulae
De?nition 1. A minimally unsatis?able subformula (MUS) of a CNF
formula F is a set M of clauses having the following properties:
?M?F(in the sense of clause-subset, i.e. Cj ?M ? Cj ?F).
?Mis unsatis?able.
Every proper clause-subset of M is satis?able.
Clearly, F contains a MUS if and only if F is unsatis?able. Therefore,
the problem of deciding whether a formula F contains a MUS is co-
NP-complete, since SAT is well-known NP-complete. A MUS may be
a proper subformula of F or coincide with F. Sometimes in litera-
ture, adverb ?minimally? is replaced, with same meaning, by adjective
?minimal?.
De?nition 2. Given a CNF formula F,theMUS selection problem
consists in ?nding a minimally unsatis?able subformula M?For
proving that such a subformula does not exist.
In the general case, more than one MUS can be contained in the same
F. Some of them can overlap, in the sense that they can share some
clauses, but they cannot be fully contained one in another. Formally, the
collection of all MUS of F is a clutter. Relations between the structures
of Max-SAT solution and MUS are investigated in (Bruni, 2002). Note
that the MUS selection problem is di?erent, although closely related,
from the minimal unsatis?able subformula problem of deciding whether
a CNF formula contains a subformula in MU(k), see (Kleine Bu?ning
and Zhao, 2002). Besides, empirical experience suggests that ?nding
a MUS typically requires much more time than just solving the SAT
problem, just like ?nding an IIS requires much more time than just
solving the feasibility of a system of linear inequalities (Guieu and
Chinneck, 1999).
The problems depicted in Sect. 1 correspond to the problem of selecting
a MUS, as follows. In the case we want to restore satis?ability
exact.tex; 1/04/2003; 14:40; p.
by locating only the small part of the underlying system causing the
problem, this actually can be solved by locating a MUS. Re-design of
that part is another issue, and, typically, requires again the work of the
original (human or not) designer of the system. Postinfeasibility analy-
sis, in fact, often needs ?cooperation of algorithmic engine and human
intelligence? (Chinneck and Dravnieks, 1991). The process could need
to be repeated until all MUS are removed from the formula.
Conversely, in the case when unsatis?ability should be kept while
modifying the underlying system, this again can be solved by locating
a MUS. That is the part of the system that should not be changed.
3. The Linear Case
In the case of systems of linear inequalities, when we are interested in
real-valued solutions, the following result on infeasibility holds:
THEOREM 1. (Farkas? lemma, 1894) Let A be an h ? k real matrix
and let b be a real h-vector. Then there exists a real k-vector x ? 0 with
only if yT b ? 0 for each real h-vector y with yT A ? 0.
A proof is for instance in (Schrijver, 1986). Geometrically, this means
that if an h-vector b does not belong to the cone generated by the
h-vectors a1,.,ak (columns of A), there exists a linear hyperplane
separating b from a1,.,ak.
There are several other equivalent forms of Farkas? lemma, and we
now convert it in one which is more suitable to our purposes. It can
be put as the alternative feasibility of two linear systems by requiring
yT b<0 instead of yT b ? 0. Moreover, removing the limitation x ? 0,
we have for the alternative system yT Finally, asking for Ax ? b,
we have for the alternative system y ? 0 (for details, see e.g. Bertsimas
and Tsitsiklis, 1997). The following variant is therefore obtained: given
amatrixA ? IR h?k and a vector b ? IR h, consider the system of linear
inequalities:

and the new system of linear inequalities obtained from the former one:
y b<0
(2)
We have that exactly one of the two following possibilities holds:
Exact Selection of Minimally Unsatis?able Subformulae 5
? (1) is feasible, i.e. there exists x ? IR k verifying all its inequalities.
? (2) is feasible, i.e. there exists y ? IR h verifying all its inequalities.
An irreducible infeasible subsystem (IIS) is a subset of the inequalities
of an infeasible system that is itself infeasible, but for which any proper
subset is feasible. Clearly, it constitutes the analogous of a MUS in the
case of systems of linear inequalities. An IIS can be selected within (1)
by solving the following new system:
The support of a vertex denotes the indices of its non-zero components;
respectively denote vectors of zeroes and ones of appropriate
dimension.
THEOREM 2. (Gleeson and Ryan, 1990) Consider two systems of
linear inequalities in the form (1) and (3). If (3) is infeasible, (1)
is feasible. On the contrary, if (3) is feasible, (1) is infeasible, and,
moreover, each IIS of (1) is given by the support of each vertex of the
polyhedron (3).
The proof is based on polyhedral arguments using properties of extreme
rays, see (Gleeson and Ryan, 1990). Therefore, checking the feasibility
of (1), and, if infeasible, identifying one of its IIS, becomes the problem
of ?nding a vertex of a polyhedron.
4. Propositional Formulae: the General Case
In the case of propositional formulae, it is well-known that a clause

i?? i??
can be expressed as a linear inequality by using n binary variables xi ?
{0, 1} corresponding to the propositional variables ?i ?{False , True },
and by de?ning the incidence m-vectors of the set of its positive literals
b? and of that one of its negative literals b?
Equivalently, by denoting with |?| the number of negative literals in
the clause, this can be rewritten as
Denote now with B the {0, ?1}m?n matrix whose rows correspond to
clauses as shown above (each element is -1 if the corresponding propositional
variables is positive, 1 if it is negative, 0 otherwise). Denote
also with ?(B)them-vector of all the |?j|. The following system of
linear inequalities with binary variables represents a CNF propositional
formula.
In order to use the results given for the linear case, let us consider the
linear relaxation of such system.
We will suppose that our formula always contains at least a unit clause,
i.e. a clause containing a single literal, since in the absence of that the
linear relaxation (7) is always feasible. Note that, in practical applica-
tions, such assumption is generally veri?ed. The above system (7) is now
in the form of (1). The ?rst group of inequalities of type (5) are called
clausal inequalities. In particular, the matrix A ?{0, ?1}(m+2n)?n and
the vector b ? Zm+2n are composed as follows.
Therefore, a system which plays the role of (3) can now be written.
exact.tex; 1/04/2003; 14:40; p.
Exact Selection of Minimally Unsatis?able Subformulae 7
So far, the following result on the couple of systems (6) and (8) holds.
The restriction of the support of a vertex to clausal inequalities will denote
the indices of its non-zero components among those corresponding
to clausal inequalities.
THEOREM 3. Consider two systems of linear inequalities in the form
and (8). In this case, if (8) is feasible, (6) is infeasible, and the
restriction of the support of each vertex of the polyhedron (8) to clausal
inequalities contains a MUS of (6). On the contrary, if (8) is infeasible,
(7) is feasible, but it cannot be decided whether (6) is feasible or not.
Proof. We ?rst prove that the restriction of the support of a vertex
of (8) to clausal inequalities contains a MUS of (6). Assume (8) is
feasible, and let v1 be the vertex found. Therefore, (7) is infeasible
(from Theorem 2), and an IIS in (7), called here IIS1,isgivenby
the support of v1. Such IIS1 is in general composed by a set CI 1 of
clausal inequalities (inequalities of the type (5)) and a set BC1 (possibly
empty) of box constraints (the ones imposing 0 ? xi ? 1). The set
of inequalities CI 1 has no {0, 1} solutions, since removing the
from IIS1, while imposing the more strict integer constraints IC1 (the
ones imposing xi ?{0, 1}), keeps IIS1 unsatis?able. Therefore, a MUS
is contained into the clauses corresponding to CI 1. Such MUS can
still be a subset of the clauses corresponding to CI 1, because, though
imposing the more strict
integer constraints can make CI 1 ? IC1 not minimal.
On the other hand, not all MUS in (6) can be obtained by such
procedure. This because, if (8) is infeasible, (7) is feasible (by Theorem
2). When imposing the more strict integer constraints instead of the
box constraints, however, nothing can be said on the feasibility of (6).
Example. Consider F1 composed by the four following clauses.
A and b can easily be obtained, in the following manner.
Therefore, the system to be solved, in the form of (8), is the following.
MUS in F1 is given by the set of clauses {C1,C2,C3} (and F1 is proved
unsatis?able).
From the practical point of view, for the motivations reported above,
we are interested in MUS composed by a small number of clauses.
Moreover, it may happen that not all clauses are equally preferable for
the composition of the MUS that we are selecting. When this can be
evaluated, a cost cj for taking each clause Cj into the MUS that is being
selected can be assigned. Such costs cj for the clauses corresponds to
costs for the variables of system (8). Therefore, a cost h-vector is com-
puted. Its ?rst m components will correspond to clausal inequalities,
while the last 2n components will correspond to box constraints. So far,
the solution of the following linear program produces a MUS having
the desired clause composition.
?I
The result of Theorem 3 is not completely analogous to the linear case.
In order to obtain more analogy, let us de?ne the following property.
An integral point will denote a point having all integer components.
Integral-point property: A class of polyhedra which, if non-empty, contain
at least one integral point, has the integral-point (IP) property.
THEOREM 4. If the polyhedron (7), which is the linear relaxation of
(6), has the integral-point property, the following holds. If (8) is infea-
sible, (6) is feasible. On the contrary, if(8)isfeasible,(6)isinfeasible
exact.tex; 1/04/2003; 14:40; p.
Exact Selection of Minimally Unsatis?able Subformulae 9
and each MUS is given by the restriction of the support of each vertex
of polyhedron (8) to clausal inequalities.
Proof. We ?rst prove that (8) infeasible ? (6) feasible.
When (8) is infeasible, (7) is feasible (by Theorem 3). Since we assumed
that the IP-property holds for (7), it contains at least one integral
point. Since the box constraints hold for (7), such integer point must
have {0,1}-components, hence (6) is feasible.
We now prove that (8) feasible ? a MUS in (6) is given by the
restriction of the support of a vertex in (8) to clausal inequalities.
Denote such set of clausal inequalities by CI1, and denote also by BC1
and IC1 respectively the box constraints and the integer constraints
on the variables appearing in CI1. It was already proved that, if (8)
is feasible, CI1 corresponds to an unsatis?able subset of clauses. We
prove, by contradiction, that the set of clauses corresponding to CI 1
is minimal. Assuming CI 1 ? IC1 not minimal, there is a smaller set of
clausal inequalities CI 1 ? CI 1 such that CI 1 ? IC 1 is infeasible. On
the other hand, CI Theorem 2), so the set of
inequalities CI 1?BC1 must be feasible. However, we assumed that the
IP-property holds for (7), so contains at least one integral
point having {0,1}-components, which is the contradiction.
Therefore, CI1 corresponds to a MUS.
far, when the IP property holds, solving a linear programming
problem solves the MUS selection problem. There are several classes of
formulae for which the linear relaxation (7) de?nes a polyhedron having
the integral-point property. This is discussed in next section. The following
Table I reports, for a number of known classes of propositional
CNF, whether such property holds or not.
Table

I. When does the Integral-point property hold.
Class of Propositional Formulae IP Property
Horn (Dowling and Gallier, 1984; Scutell'a, 1990) yes
Renamable Horn (Lewis, 1978; Aspvall, 1980) yes
Q-Horn (Boros et al., 1990) no
Extended Horn (Chandru and Hooker, 1991) yes
Balanced (Conforti and Cornu?ejols, 1995; Truemper, 1998) yes
Quadratic (Aspvall et al., 1979) no
(Extended) Nested (Knuth, 1990; Hansen et. al., 1993) no
SLUR solvable (Schlipf et al., 1995) no
Matched (Franco and Van Gelder, 2002) yes
Linear Autarkies (van Maaren, 2000; Kullmann, 2000) no
considered above are already known to be easy cases for the
satis?ability problem. Not surprisingly, no easy classes for the MUS
selection problem which were not known to be easy classes for the
Satis?ability problem appear here. This because, since MUS selection
gives the answer to SAT, that would be an easy class for SAT as well.
However, considerable research e?ort has been spent on searching easy
classes for SAT for at last two decades, hence discovering entirely new
ones does not seem an easy task.
5. Special Classes of Propositional Formulae
Two interesting classes of propositional CNF formulae verify the integral-
point property: formulae which are extended Horn, which include Horn
and renamable Horn, and formulae which are balanced.Moreover,two
other classes of formulae share the IP property, and are incomparable
with the above ones. The ?rst is the class of matched formulae (Franco
and Van Gelder, 2002). The second is the class of satis?able quadratic
CNF (and consequently satis?able Q-Horn, etc.), since quadratic formulae
are renamable Horn if and only if they are satis?able. However,
the last two classes are always satis?able, so they are not of practical
interest with respect to the MUS selection problem.
Extended Horn formulae are characterizable as follows:
THEOREM 5. (Rounding theorem, Chandrasekaran, 1990) Given a
system Ax ? b, x ? 0,withA being a h ? k integral matrix and b an
integral h-vector. If there exist a k ? k matrix T such that:
Exact Selection of Minimally Unsatis?able Subformulae 11
? T and T?1 are integral;
? each row of T?1 has at most one negative entry, and it is -1;
? each row of AT?1 has at most one negative entry, and it is -1;
if x is a (fractional) solution to the above system, so is T?1Tx.
The proof, in (Chandrasekaran, 1990), is based on properties of polyhedra
having an integral largest element. In the case of a CNF, the above
can be particularized as follows (Chandru and Hooker, 1991). Consider
again the Satis?ability problem, written using inequalities in the form
(4). Denote with D the {0, ?1}m?n matrix whose rows correspond to
clauses (its elements are 1 if the corresponding propositional variables
is positive, -1 if it is negative, 0 otherwise), and with d the opportune
right-hand-side m-vector.
Its linear relaxation, when put in the form of Theorem 5, becomes:
?I ?1
Conditions required in Theorem 5, in the case of CNF formulae, translate
as follows. Each row of T?1 should have at most one +1 and at
most one -1. By adding a new {0, ?1} column vector r to T?1,whose

values are such that the {0, ?1}(n+1)?n matrix T?1|r has exactly one
+1 and one -1 per row, we obtain the arcs-nodes incidence matrix of
a direct graph with (nodes correspond to the columns of

T?1|r ). Such digraph should be a rooted arborescence, i.e. a rooted
directed tree in which all arcs point away from the root r.Arcsof
such digraph corresponds to variables of the formula. The rows of D
(i.e. the clauses) can be interpreted as ?ows on the de?ned digraph:
a positive [negative] literal is a unit ?ow going along [opposite to]
the arc corresponding to that variable. If the ?ow has the so-called
extended star-chain property (Chandru and Hooker, 1991), that is it
can be partitioned into a (possibly empty) set of unit ?ows going into
the root on an extended star, and a (possibly empty) unit ?ow on one
chain, all the conditions of Theorem 5 are veri?ed, and the CNF is
called extended Horn.
Therefore, if (11) has a fractionary solution, (10) has an integral
solution, so extended Horn formulae verify the IP property. Recognition
of extended Horn formulae is not known to be solvable in polynomial
time. The problem of the arborescence realization arise (Swaminathan
and Wagner, 1986). However, formulae can be build in order to be
extended Horn, by checking (in linear time) if each new clause de?nes
an acceptable ?ow in the arborescence (Chandru and Hooker, 1991).
Therefore, the entire procedure of MUS selection can be done in polynomial
time, if our application supports to be designed by testing each
new clause, and accepting it only when extended-Horn.
The second class is composed by balanced formulae, de?ned below.
De?nition 3. A {0, ?1} matrix is balanced if every square submatrix
with exactly two nonzeroes entries in each row and column sums to a
multiple of four.
The class of balanced matrices contains the classes of totally unimodular
matrices and network matrices (see Truemper, 1998). Note that the
property of balancedness is a general property, in the sense that it
does not requires the matrix to represent a CNF formula. When such
property is veri?ed by a matrix representing a CNF formula (in the
form (10), or, equivalently, in the form (6)), the following result holds.
THEOREM 6. (Conforti and Cornu?ejols, 1995) If the matrix representing
the CNF instance in form (10) is balanced, the polytope is
integral, i.e. has all integral extreme points.
The proof, not immediate, is developed using polyhedral theory. The
problem of recognition of balanced matrix has polynomial-time com-
plexity. The algorithm which solves it is based on decomposition results,
and proceeds by decomposing the given matrix, and checking if all the
obtained submatrices are balanced (Conforti et al., 1994). Therefore,
the entire procedure for MUS selection requires polynomial time on
balanced matrices.
One can observe that another procedure to ?nd a MUS could be
based on additive or subtractive ?lters. Such methods would at ?rst test
if formula F is unsatis?able. If so, additive methods would generate a
new formula F by adding clauses form F until F is unsatis?able. So
far, F is the selected IIS. The algorithm proposed in (Bruni, 2002) is
an evolution on additive methods. Subtractive methods would instead
remove from F each clause Cj not needed for unsatis?ability by testing
if the formula remains unsatis?able when removing Cj. What remains
of F is the selected IIS. Such methods can therefore guarantee to ?nd
a MUS when it exists. However, they require to solve (at
exact.tex; 1/04/2003; 14:40; p.
Exact Selection of Minimally Unsatis?able Subformulae 13
times the base problem (satis?ability for MUS selection, feasibility for
IIS selection). When this can be done in polynomial time, the whole
procedure would be theoretically polynomial. However, similar ?brute
force? approach are recognized to be quite computationally demanding
(Chinneck and Dravnieks, 1991; Gleeson and Ryan, 1990). Moreover,
the proposed approach allows a more powerful manner of choosing the
clause composition of selected MUS, by using the cost function in (9).
Example. Consider the following CNF formula F2.
Suppose also that the following T?1 matrix could be obtained.
abcd r
The rooted arborescence corresponding to T?1 is now as follows. The
?ow corresponding to the ?rst [second] clause is given by the shorter
arrows drown over [under] the arcs.

a


d

The ?ow corresponding to the third [forth] clause is given by the shorter
arrows drown over [under] the arcs.

a


Such ?ows have the extended star-chain property. Therefore, although
neither Horn nor renamable Horn, F2 is extended Horn, so we are in
the conditions of Theorem 4.
Suppose now that we are unable to obtain a suitable T?1 matrix. In
this case, the following matrix, corresponding to F2 in form (10), must
exact.tex; 1/04/2003; 14:40; p.
be tested for balancedness.
easy to see that every square submatrix with two nonzeroes per
row and per column sums to 0, hence it is balanced, so we are again
assured to be in the conditions of Theorem 4. So far, A and b are built
as follows. ?
Since the IP property is veri?ed, the MUS selection problem is completely
solved by solving the following system.
This system is infeasible. Hence, we are guaranteed that no MUS is
present in F2, which is therefore satis?able.
6. Implementation and Computational Experience
Many problems of error detection or classi?cation into large data-sets
are solved by using rules (Fellegi and Holt, 1976). By encoding the
rules into clauses, an inconsistency,orcontradiction, in the set of rules
exact.tex; 1/04/2003; 14:40; p.
Exact Selection of Minimally Unsatis?able Subformulae 15
corresponds to a set of clauses jointly unsatis?able (Bruni and Sassano,
2001). Since rules should be free from contradiction, this is one of the
cases when the resulting logic formula should be satis?able. Therefore,
checking the rules for inconsistencies produces MUS selection problems.
Note that all the con?icting rules should be located, and it would not
help deleting some of them. In particular, detection of partial inconsistencies
(which are inconsistencies having e?ect only for some values of
the data) produces a series of instances which are very similar. CNF
generated for the validation of rules used for a real-world
census are here considered.
The proposed algorithm is implemented in C++ and runs on a Pentium
IV PC. After the initial routine converting rules into clauses and
generating the CNF formulae, the procedure composes the above shown
matrix A and vector b as in (8). By adding an opportune objective
function, a problem in the form (9) is then passed to a standard routine
for solving linear programming (ILOG Cplex 1) implementing the simplex
algorithm. When a vertex is found, its support is used to produce
the MUS which is given in output. Although the simplex method has
exponential-time complexity, and there are polynomial-time complexity
methods for solving the same problem (e.g. barrier?s method) and then
?nding a vertex, the former alternative is generally reckoned to be
faster in practice (see for instance Bertsimas and Tsitsiklis, 1997 for
a description). When the problem in form (9) is infeasible, either we
check that we are in one of the described special classes (such check
depending on the problem), and in such case no MUS exist, or we
need to solve the satis?ability problem for the original CNF formula.
However, for all considered real problems, when (9) is infeasible, the
original formula turn out to be satis?able.

Table

II reports number of variables (n) and number of clauses (m)
both for the original formula and for the selected MUS, in addition to
computational times (in seconds). We report only instances corresponding
to partial inconsistencies, hence formulae containing a MUS. Those
results are intended to give an example of application, rather than
exploring all the computational possibilities of the proposed procedure,
since the latter is not the focus of present paper.
information available at www.cplex.com.
Table

II. Real-world contradiction detection problems.
Original formula Selected MUS
Name nmnmtime
In the majority of the cases, only one MUS was present in the CNF,
that means only one inconsistency was present in the set of rules. If,
however, after repairing the found inconsistency, the new CNF still
contains a MUS, that is another inconsistency, and should as well
be repaired independently. The whole procedure, according to human
experts having the charge of writing the rules, turn out to be a very
satisfactory tool for the design of a contradiction-free set of rules.
7. Conclusions
The problem of MUS selection is formally de?ned. Such problem is
computationally hard and arises in several applicative ?elds. This typically
happens when the application is encoded into a propositional
formula which should have a well-de?ned satis?ability property (either
to be satis?able or to be unsatis?able).
A procedure for solving the MUS selection problem is here presented.
Under special conditions, the proposed procedure is able to exactly
solve such problem by simply solving a linear programming problem,
which can be done with polynomial-time or simplex based algorithms.
Known classes of CNF formulae are studied with respect to veri?cation
of such special conditions. The largest classes of CNF formulae verifying
the above conditions result to be extended Horn and balanced formulae.
Computational experience on real-world data mining problems is very
encouraging.
Exact Selection of Minimally Unsatis?able Subformulae 17

Acknowledgements

The author whish to thank Carlo Mannino for helpful discussions.


--R


Recognizing disguised NR(1) instance of the satis?
A linear time algorithm for testing the truth of certain quanti
Approximate Algorithms and Heuristics for MAX-SAT
Introduction to Linear Optimization.
time inference of all valid implications for Horn and related formulae.
Approximating Minimal Unsatis?
Detection and Correction in Large Scale Data Collecting.
Integer programming problems for which a simple rounding type of algorithm works.
Extend Horn clauses in propositional logic.
Optimization Methods for Logical Inference.
Fast Heuristics for the Maximum Feasible Subsystem Problem.
Locating Minimal Infeasible Constraint Sets in Linear Programs.




A Perspective on Certain Polynomial Time Solvable Classes of Satis?
Computers and Intractability.
Minimally Infeasible Subsystems of Inequalities.
Algorithms for the Satis?- ability (SAT) Problem: A Survey
Analyzing Infeasible Mixed-Integer and Integer Linear Programs INFORMS Journal on Computing 11 (1)
An extension of nested satis?


Nested
An application of matroid theory to the SAT Problem.
Renaming a set of clauses as a Horn set.
A Short Note on Some Tractable Cases of the Satis?
On Finding Solutions for Extended Horn Formulas.
Theory of Linear and Integer Programming.
The arborescence-realization problem
A note on Dowling and Gallier?
Detecting IIS in Infeasible Linear Programs using Techniques from Goal Programming.

--TR

--CTR
ric Grgoire , Bertrand Mazure , Cdric Piette, Local-search Extraction of MUSes, Constraints, v.12 n.3, p.325-344, September 2007
UnSatisfiability;MUS selection;infeasibility analysis