We introduce the stable model semantics for fuzzy propositional formulas, which generalizes both fuzzy propositional logic and the stable model semantics of classical propositional formulas. Combining the advantages of both formalisms, the introduced language allows highly configurable default reasoning involving fuzzy truth values. We show that several properties of Boolean stable models are naturally extended to this formalism, and discuss how it is related to other approaches to combining fuzzy logic and the stable model semantics.
Answer set programming (ASP) [
Both the stable model semantics and fuzzy logic are generalizations of classical
propositional logic in different ways. While they do not subsume each other, it is clear
that many real-world problems require both their strengths. This led to the body of work
on combining fuzzy logic and the stable model semantics, known as fuzzy answer set
programming (e.g., [
Unlike existing work on fuzzy answer set semantics, in this paper, we extend the
general stable model semantics from [
The paper is organized as follows. Section 2 reviews the syntax and the semantics of fuzzy propositional logic we discuss in the paper, as well as the stable model semantics of classical propositional formulas. Section 3 presents the stable model semantics of fuzzy propositional formulas along with examples, followed by Section 4 that formalizes the trust example above in the proposed language. Section 5 shows how the fuzzy stable model semantics is related to the Boolean stable model semantics, and Section 6 shows how our fuzzy stable model semantics is related to other approaches to fuzzy ASP. Section 7 shows that several well-known properties of the Boolean stable model semantics can be easily extended to our fuzzy stable model semantics. 2 2.1
We review the definition of a stable model from [
Let be a classical propositional signature, p = (p1; : : : ; pn) be a list of distinct atoms belonging to , and let q = (q1; : : : ; qn) be a list of new propositional atoms not in .
For two interpretations I and J of , I [ Jqp denotes the interpretation of [ q that agrees with I and J on all atoms not in p [ q, and – for each p 2 p, (I [ Jqp)(p) = I(p); – for each q 2 q, (I [ Jqp)(q) = J (p).1
For any classical propositional formula F of signature , F (q) is a classical propositional formula of signature [ q that is defined recursively as follows: – pi = qi for each pi 2 p; – F = F for any atom F 62 p; – ? = ?; > = >; – (:F ) = :F ; – (F ^ G) = F – (F ! G) = (F ^ G ; (F _ G) = F ! G ) ^ (F ! G).
_ G ; 1 I(p) denotes the truth value of p under I. We identify a list with a set if there is no confusion.
Let I and J be two interpretations of , and let p be a subset of . We say J if – J and I agree on all atoms not in p, and – for all p 2 p, if J j= p, then I j= p.
We say J <p I if J
p I and J 6= I.
Definition 1. An interpretation I is a stable model of F relative to p (denoted I j= SM[F ; p]) – if I j= F , and – there is no interpretation J such that J <p I and I [ Jqp j= F (q).
p not q; q
not p
F1 = (:q ! p) ^ (:p ! q): which is understood as an alternative notation for propositional formula F1 (u; v) is
(:q ! u) ^ (:q ! p) ^ (:p ! v) ^ (:p ! q): We check that I1 = fpg (that is, p is TRUE and q is FALSE) 2 is a stable model of F1 (relative to fp; qg): I1 satisfies F1, and ; is the only interpretation J such that J <pq I1. However, I1 [ Jupvq = fpg does not satisfy F1 (u; v) because it does not satisfy the first conjunctive term of F1 (u; v).
Similarly, we can check that fqg is another stable model of F1. 2.2
Let be a fuzzy propositional signature, which is a set of symbols called fuzzy atoms. In addition, we assume the presence of a set C of fuzzy conjunction symbols, a set D of fuzzy disjunction symbols, a set N of fuzzy negation symbols, and a set I of fuzzy implication symbols.
A fuzzy (propositional) formula of is defined recursively as follows. – every fuzzy atom p 2 is a fuzzy formula; – every numeric constant c where c is a real number in [0; 1] is a formula; – if F is a formula, then :F is a formula, where : 2 N; – if F and G are formulas, then F G, F G and F ! G are formulas, where 2 C, 2 D, and ! 2 I. 2 We identify a propositional interpretation with the set of atoms that are true in it.
The models of a fuzzy formula are defined as follows [
The fuzzy operators are functions mapping one or two truth values into a truth value. Among the operators, : denotes a function from [0; 1] into [0; 1]; , , and ! denote functions from [0; 1] [0; 1] into [0; 1]. The actual mapping performed by each operator can be defined in many different ways, but all of them satisfy the following conditions, which imply that they are generalizations of the corresponding classical propositional connectives:3 – a fuzzy negation : is decreasing, and satisfies :(0) = 1 and :(1) = 0; – a fuzzy conjunction is increasing, commutative, associative, and (1; x) = x for all x 2 [0; 1]; – a fuzzy disjunction is increasing, commutative, associative, and (0; x) = x for all x 2 [0; 1]; – a fuzzy implication ! is decreasing in its first argument and increasing in its second argument; and ! (1; x) = x and ! (0; 0) = 1 for all x 2 [0; 1]. !r the residual implicator of m !s the S-implicator induced by :s and
Definition l(x; y) = max (x + y l(x; y) = min (x + y; 1) m(x; y) = min (x; y) m(x; y) = max (x; y) p(x; y) = x y p(x; y) = x + y x y :s(x) = 1 x
(1 if x y !r (x; y) =
y otherwise m !s (x; y) = max (1 x; y) 1; 0)
The truth value of a formula F under I, denoted F I , is defined recursively as follows: – for any atom p 2 , pI = I(p); – for any numeric constant c, cI = c; – (:F )I = :(F I ); – (F G)I = (F I ; GI ); (F
G)I = (F I ; GI ); (F ! G)I = ! (F I ; GI ). 3 We say that a function f of arity n is increasing in its i-th argument (1 i n) if f (arg1; : : : ; argi; : : : ; argn) f (arg1; : : : ; argi0; : : : ; argn) for all arguments such that argi argi0; f is said to be increasing if it is increasing in all its arguments. The definition of decreasing is similar. (For simplicity, we identify the symbols for the fuzzy operators with the truth value functions represented by them.) Definition 2. We say that a fuzzy interpretation I satisfies a fuzzy formula F w.r.t. a threshold y 2 [0; 1] if F I y, and denote it by I j=y F . We call I a fuzzy y-model of F .
3
We extend the notion of J <p I in Section 2.1 as follows. For any two fuzzy interpretations J and I of the same signature and any subset p of , we say J p I if – J and I agree on all fuzzy atoms not in p, and – for all p 2 p, pJ pI .
We say J <p I if J p I and J 6= I.
As before, we assume a list q of new, distinct fuzzy atoms, and define I [ Jqp in the same way. That is, I [ Jqp denotes the interpretation of [ q that agrees with I and J on all atoms not in p [ q, and
The definition of F is also extended in a straightforward way: For any fuzzy formula F of signature , F (q) is defined as follows.
– for each p 2 p, (I [ Jqp)(p) = I(p); – for each q 2 q, (I [ Jqp)(q) = J (p). – pi = qi for each pi 2 p; – F = F for any atom F 62 p; – c = c for any numeric constant c; – (:F ) = :F ; – (F G) = F G ; – (F ! G) = (F ! G ) (F G) = F m (F ! G).
G ; Definition 3. An interpretation I is a y-stable model of F relative to p (denoted I j=y SM[F ; p]) if – I j=y F , and – there is no interpretation J such that J <p I and I [ Jqp j=y F (q).
We often omit the threshold y when it is 1, and omit p if it contains all atoms in .
Clearly, when p is empty, Definition 3 reduces to the definition of a fuzzy model in Definition 2 because there is no J such that J <; I.
Also, Definition 3 is very similar to the definition of a stable model for classical propositional formulas in Definition 1. The main difference is that simply in the latter, atoms may have various degrees of truth, and accordingly the notion of J <p I is more general. The precise relationship between the definitions is discussed in Section 5. Example 2. Consider the formula F = :sp !r q and the interpretation I = f(p; 0); (q; 0:6)g. F (u; v) is ((:sp) !r q ) m (:s p !r q) = (:sp !r v) m (:sp !r q): I j=0:6 SM[F ; p; q]. First, it is easy to see that I j=0:6 F , as Suppose there exists J <pq I such that I [ Jupvq j=0:6 F , i.e.,
F I =!r ((:sp)I ; qI ) =!r (1
pI ; qI ) =!r (1; 0:6) = 0:6: F (u; v)I[Jupvq = min
!r (:s(pI ); vJupvq ); !r (:s(pI ); qI ) = min v!Jurpvq(;10;:v6Jupvq ); 0:6 = min 0:6: So vJupvq 0:6. Since vJupvq qI = 0:6, we conclude that vJupvq = 0:6. However, this contradicts the assumption that J <pq I . Therefore, such J does not exist, and I is a 0.6-stable model of F .
Example 3. p and :s:sp have the same fuzzy models, but their stable models are
different. This is similar to the fact that p and ::p have different stable models according
to the semantics from [
Clearly, any interpretation I = f(p; y)g, where y is any positive real number in [0; 1], is a y-stable model of p relative to fpg. On the other hand, I = f(p; y)g is not a y-stable model of F = :s:sp relative to fpg. Formula F (q) is :s:sF , and although I j=y F , we have I [ Jqp j=y F (q) regardless of any J .
Example 4. Let F1 = p !s p and F2 = :sp m p. Their fuzzy models are the same, but their stable models are not. This is similar to the relation between p ! p and :p _ p in the Boolean stable model semantics. Indeed, observe that F1 (q) = (p !s p) m (q !s q) and F2 (q) = :sp m q.
The interpretation I = f(p; 1)g is not a 1-stable model of F1 relative to p, as witnessed by J = f(p; 0)g. However, I is a 1-stable model of F2 relative to p: for any J p, q F2 (q)I[Jqp = max 1 pI ; qJqp = max 0; qJqp = qJqp : So, for I [ Jqp to satisfy F2 (q) to degree 1, qJqp should be 1, or equivalently, pJ should be 1. Consequently, it is not possible to have J <p I .
The following example illustrates how the commonsense law of inertia involving fuzzy truth values can be represented.
Example 5. Let be fp; p; q; qg 4 and let F be F1 m F2, where F1 represents that p and p are complementary, i.e., the sum of their truth values is 1:
F1 = :s(p l p) m :s:s(p l p):
is not a connective; it is just a part of the symbol representing an atom. F2 represents that by default p has the truth value of q, and p has the truth value of q: m :s:sp) !r p) m (( q m :s:s p) !r p): Let p = fp; pg and u = fu; ug. F (u) is :s(p l p) m :s:s(p l p) m((q m :s:sp) !r u) m ((q m(( q m :s:s p) !r u)
m :s:sp) !r p) m (( q m :s:s p) !r p): One can check that the interpretation I1 = f(p; x); ( p; 1 x); (q; x); ( q; 1 x)g (x is any value in [0; 1]) is a 1-stable model of F relative to (p; p); The interpretation I2 = f(p; y); ( p; 1 y); (q; x); ( q; 1 x)g, where y > x, is not. Similarly, if y < x, I2 is not a 1-stable model of F relative to (p; p).
On the other hand, if we conjoin F with y !r p to yield F m (y !r p), then the default behavior is overridden, and I2 is a 1-stable model of F m (y !r p) relative to (p; p).
This behavior is useful in expressing the commonsense law of inertia involving fuzzy values. Suppose q represents some fluent at time t, and p represents the fluent at time t + 1. Then F states that, “by default, the fluent retains the previous value.” The default value is overridden if there is an action that sets p to a different value. 4
The trust example in the introduction can be formalized in the fuzzy stable model semantics as follows. Below x, y, z are schematic variables ranging over people, and t is a schematic variable ranging over time steps. Trust(x; y; t) is a fuzzy atom representing that “x trusts y at time t.” Similarly, Distrust(x; y; t) is a fuzzy atom representing that “x distrusts y at time t.”
The trust relation is reflexive:
F1 = Trust(x; x; t):
The trust and distrust degrees are complementary, i.e., their sum is 1 (similar to Example 5):
F2 = :s(Trust(x; y; t) l Distrust(x; y; t));
F3 = :s:s(Trust(x; y; t) l Distrust(x; y; t)):
Initially, if x trusts y to degree d1 and y trusts z to degree d2, then x trusts z to degree d1 d2; further the initial distrust degree is 1 minus the initial trust degree.
F4 = Trust(x; y; 0) p Trust(y; z; 0) !r Trust(x; z; 0);
F5 = :sTrust(x; y; 0) !r Distrust(x; y; 0):
F6 = Trust(x; y; t) F7 = Distrust(x; y; t) m :s:sTrust(x; y; t+1) !r Trust(x; y; t+1);
m :s:sDistrust(x; y; t+1) !r Distrust(x; y; t+1): A conflict increases the distrust degree by the conflict degree:
F8 = Conflict(x; y; t) l Distrust(x; y; t) !r Distrust(x; y; t+1);
F9 = :s(Conflict(x; y; t) l Distrust(x; y; t)) !r Trust(x; y; t+1):
Let FT W be F1 m F2 m m F9. Suppose we have the formula FF act = Fact1 m Fact2 that gives the initial trust degree.
Fact1 = 0:8 !r Trust(Alice; Bob; 0);
Fact2 = 0:7 !r Trust(Bob; Carol; 0): Although there is no fact about how much Alice trusts Carol, any 1-stable model of FT W m FF act assigns value 0:56 to the atom Trust(Alice; Carol; 0). On the other hand, the 1-stable model assigns value 0 to Trust(Alice; David; 0) due to the closed world assumption under the stable model semantics.
When we conjoin FT W FF act with 0:2 ! Conflict(Alice; Carol; 0), the 1-stable model of FT W m FF act m (0:2 ! Conflict(Alice; Carol; 0)), manifests that the trust degree between Alice and Carol decreases to 0:36 at time 1. More generally, if we have more actions that change the trust degree in various ways, by specifying the entire history of actions, we can determine the evolution of the trust distribution among all the participants. Useful decisions can be made based on this information. For example, Alice may decide not to share her personal pictures to those whom she trusts less than degree 0:48.
Note that this example, like Example 5, uses nested connectives, such as :s:s, that
are not available in previous fuzzy ASP semantics, such as [
The Boolean stable model semantics in Section 2.1 can be embedded into the fuzzy stable model semantics as follows:
For any classical propositional formula F , define F fuzzy to be the fuzzy propositional formula obtained from F by replacing ? with 0, > with 1, : with :s, ^ with m, _ with m, and ! with !s. We identify the signature of F fuzzy with the signature of F . Also, for any interpretation I, we define the corresponding fuzzy interpretation Ifuzzy as – Ifuzzy (p) = 1 if I(p) = TRUE; – Ifuzzy (p) = 0 otherwise.
The following theorem tells us that the Boolean-valued stable model semantics can be viewed as a special case of the fuzzy stable model semantics.
Theorem 1 For any classical propositional formula F and any classical propositional interpretation I, I is a stable model of F relative to p iff Ifuzzy is a 1-stable model of F fuzzy relative to p. :sp !s q.
Example 6. Let F be the classical propositional formula :p ! q. F has only one stable model I = fqg. Clearly Ifuzzy = f(p; 0); (q; 1)g is a 1-stable model of F fuzzy =
Theorem 1 does not hold for an arbitrary choice of operators, as illustrated by the following example.
Example 7. Let F be the classical propositional formula p _ p. Classical interpretation I = fpg is a stable model of F . However, Ifuzzy = f(p; 1)g is not a stable model of F 0 = p l p because there is J = f(p; 0:5)g such that I [ Jqp j=1 q l q.
However, one direction of Theorem 1 holds for arbitrary choice of fuzzy operators. Theorem 2 For any classical propositional formula F , let F fuzzy be the formula ob1 tained from F by replacing ? with 0, > with 1, : with any fuzzy negation symbol, ^ with any fuzzy conjunction symbol, _ with any fuzzy disjunction symbol, and ! with any fuzzy implication symbol. For any classical propositional interpretation I, if Ifuzzy is a 1-stable model of F1fuzzy relative to p, then I is a stable model of F relative to p. 6 6.1
A normal FASP program is a finite set of rules of the form a b1 : : : bm :bm+1 : : : :bn; where n m 0, a; b1; : : : ; bn are fuzzy atoms or numeric constants in [0; 1], and is any fuzzy conjunction. We identify the rule with the fuzzy implication b1 : : : bm :sbm+1 : : : :sbn !r a:
We say that a fuzzy interpretation I of signature satisfies a rule R if RI = 1. I
satisfies an FASP program if I j= R for every rule R in . According to [
Theorem 3 For any normal FASP program = fr1; : : : ; rng, let F be the formula
r1 m : : : m rn. An interpretation I is a fuzzy answer set of in the sense of [
Example 8. Let
be the following program
p
:q;
q
:p:
The answer sets of according to [
Like our fuzzy stable model semantics, fuzzy equilibrium logic [
We review the definition of fuzzy equilibrium logic in the absence of strong negation. For any fuzzy propositional signature , a (fuzzy N5) valuation is a mapping from fh; tg to subintervals of [0; 1] such that V (t; a) V (h; a) for each atom a 2 . For V (w; a) = [u; v], where w 2 fh; tg, we write V (w; a) to denote the lower bound u and V +(w; a) to denote the upper bound v. The truth value of a formula under V is defined as follows.
– V (w; c) = [c; c] for any numeric constant c; – V (w; F G) = [V (w; F ) V (w; G); V +(w; F ) V +(w; G)]; 6 – V (w; F G) = [V (w; F ) V (w; G); V +(w; F ) V +(w; G)]; – V (h; :F ) = [1 V (t; F ); 1 V (h; F )]; – V (t; :F ) = [1 V (t; F ); 1 V (t; F )]; – V (h; F ! G) = [min(V (h; F ) ! V (h; G); V (t; F ) ! V (t; G)); V (h; F ) ! V +(h; G)]; – V (t; F ! G) = [V (t; F ) ! V (t; G); V (t; F ) ! V +(t; G)].
A valuation V is a (fuzzy N5) model of a formula F if V (h; F ) = 1, which implies V +(h; F ) = V (t; F ) = V +(t; F ) = 1. For two valuations V and V 0, we say V 0 V if V 0(t; a) = V (t; a) and V (h; a) V 0(h; a) for all atoms a. We say V 0 V if V 0 V and V 0 6= V . We say that a model V of F is h-minimal if there is no model V 0 of F such that V 0 V . An h-minimal fuzzy N5 model V of F is a fuzzy equilibrium model of F if V (h; a) = V (t; a) for all atoms a.
For two fuzzy interpretations I, J of signature such that J I, define the N5 fuzzy valuation VJ;I as VJ;I (h; a) = aJ ; 1 , VJ;I (t; a) = aI ; 1 for all atoms a in . Since J I, we have aJ aI , and VJ;I (t; a) VJ;I (h; a) for all atoms a.
As in [
The following proposition relates the notions used in the fuzzy equilibrium models and the fuzzy stable models.
Proposition 1 (a) I j=1 F if and only if VI;I is a model of F . (b) For p = , I [ Jqp j=1 F (q) if and only if VJ;I is a model of F . (c) For two interpretations I and J , we have VJ;I VI;I if and only if J < I.
The theorem below shows that the fuzzy stable model semantics can be reduced to fuzzy equilibrium logic semantics.
Theorem 4 For any fuzzy formula F (that contains no strong negation) and any fuzzy interpretation I, I is a 1-stable model of F if and only if VI;I is a fuzzy equilibrium model of F . 5 Strong negation can be simulated in our semantics using new atoms as illustrated in Example 5. 6 For readability, we write the infix notation (x y) in place of (x; y).
Next we show the other direction, i.e., reducing fuzzy equilibrium logic to the fuzzy stable model semantics. For any valuation V , define the fuzzy interpretation IV as aIV = V (h; a) for all atoms a.
Theorem 5 For any fuzzy formula F (that contains no strong negation) and any valuation V , we have that V is an equilibrium model of F if and only if (i) V +(h; a) = V +(t; a) = 1 for all atoms a, and (ii) IV is a 1-stable model of F relative to .
Theorem 5 tells us that in the absence of strong negation, the upper bounds of both worlds in any equilibrium model are always 1. 7
In this section, we show that several well-known properties of the Boolean stable model semantics can be naturally extended to the fuzzy stable model semantics. 7.1
Proposition 2 For any fuzzy formula F and any fuzzy interpretations I, J with J p I, – I [ Jqp j=y :F (q) m :F iff I [ Jqp j=y :F . – I [ Jqp j=y (F G )(q) m (F G) iff I [ Jqp j=y (F – I [ Jqp j=y (F G )(q) m (F G) iff I [ Jqp j=y (F G )(q).
G )(q).
This proposition tells us that F in Section 3 can be equivalently defined by treating the fuzzy operators in the uniform way: – (:F ) = :F – (F G) = (F m :F ;
G ) 7.2
m (F
In answer set programming, constraints—rules with ? in the head—play an important
role in view of the fact that adding a constraint eliminates the stable models that
“violate” the constraint. The following theorem is the counterpart of Theorem 3 from [
Theorem 6 For any fuzzy formulas F and G, I is a 1-stable model of F :G (relative to p) if and only if I is a 1-stable model of F (relative to p) and I j=1 :G. Example 9. Consider F = (:sp !r q) m (:sq !r p) m :sp. Formula F has only one 1-stable model I = f(p; 0); (q; 1)g, which is the only 1-stable model of (:sp !r q) m (:sq !r p) that satisfies :sp to degree 1.
If we consider a more general y-stable model, then only one direction holds. Theorem 7 For any fuzzy formulas F and G, if I is a y-stable model of F (relative to p), then I is a y-stable model of F (relative to p) and I j=y :G. :G Example 10. The other direction, that is, “if I is a y-stable model of F and I j=y :G, then I is a y-stable model of F :G,” does not hold in general. For example, consider F = G = p and to be l, and interpretation I = f(p; 0:4)g. Clearly I is a 0:4-stable model of p and I j=0:4 :p, but I is not a 0:4-stable model of p l :p. In fact, I is not even a 0:4-model of the formula. In the Boolean stable model semantics, formulas of the form p _ :p are called choice formulas, and adding them to the program makes atoms p exempt from minimization. Choice formulas have been shown to be useful in composing a program in the “Generate-and-Test” method. This section shows their counterpart in the fuzzy stable model semantics.
For any fuzzy atom p, Choice(p) stands for p l :sp. For any list p = (p1; : : : pn) of fuzzy atoms, Choice(p) stands for
Choice(p1) : : :
Choice(pn); where is any fuzzy conjunction.
The following proposition tells that choice formulas are tautological.
Proposition 3 For any fuzzy interpretation I and any list p of fuzzy atoms, I j=1 Choice(p).
Theorem 8 (a) If I is a y-stable model of F relative to p [ q, then I is a y-stable model of F relative to p. (b) I is a 1-stable model of F relative to p iff I is a 1-stable model of F Choice(q) relative to p [ q.
Theorem 8 (b) does not hold for arbitrary threshold y (i.e., if “1 ” is replaced with “y ”). For example, consider F = :s:sq and I = f(q; 0:5)g. Clearly I is a 0:5-model of F , and thus I is a 0:5-stable model of F relative to ;. However, I is not a 0:5-stable model of F m Choice(q) = :s:sq m (q l :sq) relative to ; [ fqg, as witnessed by J = f(q; 0)g.
Since the 1-stable models of F relative to ; are the models of F , it follows from Theorem 8 (b) that the 1-stable models of F Choice( ) relative to are exactly the 1-models of F .
Corollary 1 Let F be a formula of a finite signature . I is a 1-model of F relative to iff I is a 1-stable model of F Choice( ).
Example 11. Consider the formula F = :sp !r q. Although any interpretation I that satisfies 1 pI qI is a 1-model of F , among them only f(p; 0); (q; 1)g is a 1-stable model of F . However, we check that all 1-models of F are exactly the 1-stable models of G = F m Choice(p) m Choice(q): G (u; v) is So, for K to satisfy G (u; v) to degree 1, uK should be at least pK and vK should be at least qK . So there does not exist J <pq I such that I [ Jupvq j=1 G (u; v), from which it follows that I is a 1-stable model of G.
We introduced a general stable model semantics for fuzzy propositional formulas, which generalizes both the Boolean stable model semantics and fuzzy propositional logic. The syntax is the same as the syntax of fuzzy propositional logic, but the semantics defines stable models instead of models. The formalism allows highly configurable default reasoning involving fuzzy truth values. Our semantics, when we restrict threshold to be 1 and assume all atoms to be subject to minimization, is equivalent to fuzzy equilibrium logic in the absence of strong negation, but is much more simpler. To the best of our knowledge, our representation of commonsense law of inertia involving fuzzy values is new. The representation uses nested fuzzy operators, which are not available in earlier fuzzy ASP semantics for a restricted syntax.
We showed that several traditional results in answer set programming can be
naturally extended to this formalism, and expect that more results can be carried over. Future
work includes implementing this language using mixed integer programming solvers or
bilevel programming solvers [
Acknowledgements We are grateful to Joseph Babb, Michael Bartholomew, Enrico Marchioni, and the anonymous referees for their useful comments and discussions related to this paper. This work was partially supported by the National Science Foundation under Grant IIS-1319794 and by the South Korea IT R&D program MKE/KIAT 2010-TD-300404-001.