Inverse Circumscription

1 Introduction

The relationship between implicit and explicit descriptions of information is a central theme in knowledge representa­ tion and reasoning. For example, the core reasoning task of propositional satisfiability is to decide, given a propositional formula, whether or not the explicit set of models described implicitly by the formula is non-empty.

Recently, Kavvadias and Sideri [1998] studied a comple­ mentary task, which they called inverse satisfiability: given a set of models, is there a propositional formula with exactly the given set as its satisfying assignments? Without any re­ strictions on the class of formulas considered, the question is trivial, since for a given set of models M, it is always possible to create a formula in disjunctive normal form (DNF) captur­ ing exactly M . Kavvadias and Sideri consider this question with respect to the class of formulas expressible by a pre­ specified constraint language - a set of relations which can be used to express constraints. Their intriguing main result is that the complexity of the inverse satisfiability problem re­ flects exactly that of the classical satisfiability problem: for a fixed constraint language, inverse satisfiability is intractable if and only if satisfiability is intractable! For instance, INVERSE 3-SAT is intractable, as 3-SAT is intractable; but, INVERSE 2-SAT is tractable, as 2-SAT is tractable.

The inverse satisfiability problem is akin to the identifica­ tion problems studied by Dechter and Pearl [1992], which involve deciding whether or not explicitly given relational data in the form of tuples has an implicit description as a constraint network with particular features. Studying such inverse or identification problems is valuable for a vari­ ety of reasons, as articulated in [Dechter and Pearl, 1992; Kavvadias and Sideri, 1998]. First, certain restricted forms of propositional formulas, such as Hom formulas, facilitate efficient reasoning. Hence, the ability to decide when an ex­ plicitly given set of models can be represented in such a re­ stricted form, is desirable. Second, model-based represen­ tations of information have been proposed as a viable alter­ native to formula-based representations [Kautz et al., 1995; Khardon and Roth, 1996]; inverse problems address the rel­ ative expressibility of these two types of representations. Third, discovering structure in empirical data is a crucial component of scientific activity, and so understanding when structure discovery is computationally feasible sheds light on the nature of such activity.

In this paper, we further investigate the relationship be­ tween implicit and explicit descriptions of data by consid­ ering the complexity of inverse circumscription, an analog of the inverse satisfiability problem for circumscription. Cir­ cumscription is a well-studied non-monotonic reasoning for­ malism intended to embody common sense, and provides an alternative semantics for propositional formulas [McCarthy, 1980]. Intuitively, the models of the circumscription of a for­ mula are those models of the original formula which make as few "assumptions" as necessary. The inverse circumscription problem addresses the expressiveness of circumscription: this problem involves deciding, roughly speaking, if a set of mod­ els can be described by a circumscribed formula (over some constraint language). Studying the complexity of this prob­ lem is natural not only for the aforementioned reasons, but also because circumscribed formulas are more space-efficient than uncircumscribed formulas : knowledge can be repre­ sented more succinctly with the former than with the latter, in a sense made precise in [Cadoli et al., 1997].

There are at least two generalizations of the inverse satis­ fiability problem to the context of circumscription. One gen­ eralization is the problem of deciding, given a set of models, whether or not there exists a circumscribed formula (over a specified constraint language) with exactly the input set as its models. A second generalization is the problem of deciding, given a set of models, whether or not there exists a formula such that all models of the input set are models of the circum­ scribed formula- in other words, the problem is to decide the existence of an approximating formula whose circumscribed models covers the input set of models. We note that the tight­ ness of the approximating formula is not what is at stake. In our formulation of this problem, it is possible to efficiently compute a candidate formula 1/J such that if there is any for­ mula ¢ covering the input set of models, then 1/J also covers the input set and 1/J has fewer models than ¢ (that is, the model set of 1/J is a subset of the model set of¢).

As we will show, the complexity of the first generaliza­ tion, for almost all constraint languages, can be characterized fairly easily using previous results. Consequently, the focus of this paper is on the complexity of the second generaliza­ tion, which we call the inverse circumscription problem. Our main result is a dichotomy theorem in the complexity of in­ verse circumscription, which states that for all constraint lan­ guages, inverse circumscription is either in P, or is co-NP­ complete.

Complexity dichotomy theorems are important because they demonstrate a full understanding of the complexity of a problem, with respect to a particular form of problem re­ striction (in our case, a restriction on the constraint language). The first dichotomy theorem was obtained by Schaefer, who showed that the propositional satisfiability problem over a fixed constraint language is either in P, or is NP-complete. The non-trivial tractable cases of satisfiability given by this result are 2-SAT, HORN SAT, and XOR-SAT (where each constraint is a linear equation in the field with two elements). Since Schaefer's result, many other dichotomy theorems have been established [Creignou et al., 2001].

Kirousis and Kolaitis [2001a] very recently established a dichotomy theorem in the complexity of model checking for circumscription. The model checking problem is to decide, given an assignment and a formula, whether or not the assign­ ment is a model of the circumscribed formula. Their theorem states that, for any constraint language, the model checking problem is either in P or is co-NP-complete. Interestingly, we show that (for any constraint language) the complexity of inverse circumscription is exactly the complexity of this model checking problem, giving a correspondence analogous to that between the complexity of inverse satisfiability and the complexity of satisfiability. In fact, to establish hardness of inverse circumscription, we will reduce from the model checking problem.

2 Preliminaries

In this section, we present the definitions and notation that will be used throughout the paper. We first introduce the no­ tation of a constraint; constraints will be the building blocks of the propositional formulas we consider.

Definition 2.1 A subset of {0, 1 }k (for some k ~ 1) is called a logical relation, and is said to have arity k.

A constraint over variable set V is a logical relation R paired with a list of variables XI, ... , Xk E V where k is the arity of R, and is written R( XI, ... , Xk ).

A constraint with constants over variable set V is a logical relation R and a list of variables or constants YI , ... , Yk E V U {0, 1} where k is the arity of R, and is written R(yi, ... , Yk)·

We next introduce the notion of a 5-formula, which is a propositional formula built using the relations of a constraint language 5 as "templates."

Definition 2.2 A constraint language 5 is a finite set of log­ ical relations (which may contain relations of different ar­ ities). 1 The maximum arity of 5 is the maximum over the arities of the relations in 5.

An 5-formula over variable set V is a set of constraints (over V) where the logical relation of each constraint is in 5 .

An 5-formula with constants over variable set Vis a set of constraints with constants (over V) where the logical relation of each constraint is in 5.

We move on to describe the set of models associated with a formula. Intuitively, a model of a formula is an assignment to the variable set which obeys all constraints.

Definition 2.3 Let ¢ be an 5-formula (possibly with con­ stants) over variable set V .

An assignmentto ¢is a function f : V ---> {0, 1 }. When W is a subset ofV, f1w denotes the restriction off to W; and, f : V U {0, 1} ---> {0, 1} denotes the extension off where f(O) = 0, ](1) = 1, andf(v) = f(v)forallv E V.

The assignment f satisfies a constraint R(xi, ... , Xk) of¢ if the tuple (](xi), ... , f(xk)) is in R.

The assignment f satisfies ¢ if it satisfies all constraints in ¢; in this case, it is said to be a satisfying assignment or model of¢.

Define Models(¢) to be the set containing all models of¢.

For a fixed 5, the problem of deciding whether or not an in­ put 5-formula has a satisfying assignment is in NP, since in non-deterministic polynomial time, a satisfying assignment can be guessed and verified. The following example demon­ strates that there is an 5 for which this satisfiability problem is equivalent to that for 3-SAT, and hence NP-complete.

Example 2.4 Let 5 3 = {Ro, RI, R2, R3}, where Ro = {0, 1P \ {(0, 0, 0)}, RI = {0, 1P \ {(1 , 0, 0)}, R2 = {0,1P\{(1,1,0)},andR3 = {0, 1P \ {(1 , 1, 1)}. Every 3-SATformula can be efficiently converted into a 53-formula with exactly the same set of satisfying assignments, and vice­ versa. For example, the 3-SATformula

is equivalent to the 5 3-formula

We generalize the definition of 5 3 in Example 2.4 as fol­ lows.

Definition 2.5 Let 5k (for k ~ 1) be the set of relations {R~: i E {O, ... ,k}} where R~ = {0, 1}k \ {tn. and t~ E { 0, 1 }k is the tuple with 1 in the first i coordinates, and 0 in the remaining k - i coordinates.

1 Throughout this paper, we assume that all logical relations and constraint languages are non-empty.

Having defined the notion of a model of a formula, we now define what it means for a model to be minimal. The circum­ scription of a formula is considered to have, as its models, the minimal models of the original formula [McCarthy, 1980]. We consider minimality with respect to a subset P of the vari­ able set: a model is minimal if there is no model "below" it in a comparison based on the variables in P.

Definition 2.6 Let ¢ be an S-formula (possibly with con­ stants) over variable set V, and let P be a subset ofV. Let ~ denote the standard total ordering on { 0, 1} where 0 ~ 1.

Suppose that a : V ---> {0, 1} and f3 : V ---> {0, 1} are both assignments over the same variable set V. We write a =p f3 if for all v E P, a(v) = f3(v). We write a ~P f3 if for all v E P, a(v) :s; f3(v) . We write a <p f3 if a ~P f3 and it is not the case that a = p (3. We write al_pf3 if neither a :s;p f3 nor f3 :s; p a holds. When the set Pis equal to V (the entire domain of a and (3), we sometimes omit it when writing the above relations.

We say that f3 is a minimal satisfying assignment (or min­ imal model) of¢ with respect to P if f3 is a model of¢; and, for all models a of¢, a :s;p f3 implies a = p (3.

Define MinModels( ¢ , P) to be the set containing all mini­ mal models of¢ with respect to P.

We now introduce some terminology that can be used to describe constraint languages; this terminology will prove to be quite wieldy in describing many of the complexity di­ chotomy theorems presented in the next section. As usual, we define a CNF-SAT formula over variable set V to be a con­ junction of clauses, where each clause is the disjunction of literals from V. (A literal from variable set V is either a vari­ able v E V itself, or the negation of a variable ·v. Literals of the former type are called positive, whereas those of the latter type are called negative.) An assignment f : V ---. {0, 1} satisfies a CNF-SAT formula ¢ if every clause of ¢ contains a literal evaluating to true under f.

Definition 2.7 A bijunctive formula is a CNF-SAT formula where each clause contains exactly two literals.

A (dual) Horn formula is a CNF-SATformula where each clause contains at most one positive (negative) literal.

An affine formula is a conjunction of equations of the form X1 EB · · · EB Xm = c, where the Xi are variables and c E { 0, 1} is a constant. (The symbol EB denotes the logical "exclusive or.")

Definition 2.8 Let R be a logical relation of arity n, and S be a constraint language.

The relation R is 0-valid if it contains the all-zeroes tuple (0, ... , 0) of arity n, and is 1-valid if it contains the all-ones tuple (1, . . . , 1) ofarity n.

The relation R is bijunctive (Horn, dual Horn, affine) if there exists a bijunctive (respectively Horn, dual Horn, affine) formula over {v1, ... , Vn} with the same set of satisfying as­ signments as the { R}-formula { R( V1, . .. , Vn)}.

The constraint language S is 0-valid ( 1 -valid, bijunctive, Horn, dual Horn, affine) if every relation contained in S is 0-valid (respectively ]-valid, bijunctive, Horn, dual Horn, affine).

The constraint language S is Schaefer if at least one of the following four conditions hold: S is bijunctive, S is Horn, S

is dual Horn, S is affine. The constraint language S is non­ Schaefer if it is not Schaefer.

3 Related Work

This section reviews relevant work done previously; through­ out, S is used to denote a constraint language. We first men­ tion the seminal work of Schaefer, who proved a complex­ ity dichotomy theorem on the satisfiability problem for S­ formulas.

Definition 3.1 The SAT(S) decision problem.

Input: An S-formula ¢.

Question: Is ¢ satisfiable?

The SATc(S) decision problem is identical, except the in­ putS-formula can have constants.

In other words, the SAT(S) problem is to decide, for a givenS-formula¢, if the set Models(¢) is non-empty. Re­ markably, Schaefer proved that for any constraint language S, SAT(S) is either in P or is NP-complete; in addition, he gave a precise description of which constraint languages yield a tractable satisfiability problem, and which do not.

Theorem 3.2 [Schaefer, 1978] Let S be a constraint lan­ guage.

If Sis 0-valid, ]-valid, or Schaefer, then SAT(S) is in P; otherwise, SAT(S) is NP-complete.

If Sis Schaefer, then SATc(S) is in P; otherwise, SATc(S) is NP-complete.

Kavvadias and Sideri [1998] studied the "inverse satisfia­ bility problem" (denoted here by INVERSE SATc(S)). In the "standard" satisfiability problem the goal is to decide, given a formula, whether or not there exists a satisfying assignment. In the "inverse" problem, the given input is a set of assign­ ments, and the goal is to determine whether or not there ex­ ists a formula with exactly the given assignments as its set of satisfying assignments.

Definition 3.3 The INVERSE SATe( B) decision problem.

Input: Set A of assignments over the same variable set V . Question: Is there an S-formula ¢with constants such that A= Models(¢ )?

A dichotomy theorem was established by Kavvadias and Sideri, which shows that the inverse satisfiability problem is always in P, or is co-NP-complete. Intriguingly, the com­ plexity of the inverse problem reflects exactly the complexity of the satisfiability problem: SATc(S) is intractable if and only ifiNVERSE SATc(S) is intractable!

Theorem 3.4 [Kavvadias and Sideri, 1998] LetS be a con­ straint language.

If S is Schaefer, then INVERSE SATc(S) is in P; other­ wise, INVERSE SATc(S) is co-NP-complete.

We now formalize the model checking problem for cir­ cumscription, which was called "minimal satisfiability" in [Kirousis and Kolaitis, 2001a].

Definition 3.5 The MIN SAT(S) decision problem.

Input: An S -formula ¢over variable set V , an assignment a : V---> {0, 1} satisfying¢, and a subset P ofV.

Question: Is the assignment a a minimal model of¢ with respect to P?

The MIN SATc(S) decision problem is identical, except the input S -formula can have constants.

The MIN SAT(S) problem is in co-NP, as deciding whether or not a is a minimal model of a formula amounts to verifying - for all assignments (3 - that if (3 is a model, then (3 is not strictly below a in the ordering ~p. Cadoli [1992] showed that this problem is co-NP-complete in gen­ eral, and also identified some tractable cases. More recently, the following full dichotomy theorem was proved concerning the complexity of MIN SAT(S).

Theorem 3.6 [Kirousis and Kolaitis, 200Ja, Theorem 4.2P Let S be a constraint language.

If S is Schaefer, then MIN SATc(S) is in P; otherwise, MIN SATc(S) is co-NP-complete.

If Sis 0-valid or Schaefer, then MIN SAT(S) is in P; oth­ erwise, MIN SAT(S) is co-NP-complete.

4 The Inverse Circumscription Problem

The inverse satisfiability problem (defined formally in the previous section) is to decide, given a set of assignments, whether or not there is a formula with precisely the given input set as its models. The inverse circumscription problem, denoted by INVERSE MIN SAT(S), is similar in that the input is also a set of assignments and the task is to decide whether or not there is a formula describing the input set. However, in the inverse circumscription problem, the question is whether there exists a formula ¢ such that all of the given assignments are minimal models of¢.

Definition 4.1 The INVERSE MIN SAT(S) decision prob­ lem.

Input: Set A of assignments over the same variable set V, and a subset P ofV.

Question: Is there an S-formula ¢ such that A c::;; MinModels( ¢, P)?

The INVERSE MIN SATc(S) decision problem is identi­ cal, except the question is to decide if there is an S -formula with constants satisfying the stated condition.

As mentioned in the introduction, there is a natural variant of the INVERSE MIN SATc(S) problem which has an iden­ tical description, except the c::;; symbol is replaced with an = symbol in the "question." Let us denote this variant by INVERSE EXACT MIN SATc(S). We have the following re­ sults concerning this question.

Theorem 4.2 LetS be a constraint language. If S is bijunctive or Horn, then

INVERSE EXACT MIN SATc(S) is in P.

2 We note that the notation of [Kirousis and Kolaitis, 200la] is different from ours. In particular, their decision problem MIN SAT(S) involves checking, given an assignment and formula, if the assignment is minimal with respect to all variables. It is eas­ ily verified that our definition of MIN SATe (S) is equivalent to their (P; Q; Z)- MIN SAT(S), and that our definition of MIN SAT(S) is equivalent to their (P; 0; Z) - MIN SAT(S) . The theorem is stated here with respect to our notation.

If Sis non-Schaefer, then INVERSE EXACT MIN SATc(S) is co-NP-complete.

For non-Schaefer constraint languages S, hardness of INVERSE EXACT MIN SATc(S) can be shown by first es­ tablishing the hardness of INVERSE EXACT MIN SATc(S 3 ) by reduction from INVERSE SATc(S 3 ), and then re­ ducing from INVERSE EXACT MIN SATc(S 3 ) to INVERSE EXACT MIN SATc(S), using a technique in [Kavvadias and Sideri, 1998]. For Schaefer constraint languages S, the existence of an output polynomial time algorithm for computing minimal models of a S-formula implies the tractability of INVERSE EXACT MIN SATc(S); see [Kavvadias et al., 2000] for such algorithms in the case of constraint languages S that are bijunctive or Hom.

For the remainder of this paper, we focus on the INVERSE MIN SAT(S) decision problem. Given an input set A of this problem, it is possible to efficiently compute a "can­ didate formula" having the property that if there is any for­ mula containing A in its set of minimal models, then the can­ didate formula is such a formula. That is, the candidate for­ mula serves to witness that "yes" is the answer to the decision question of Definition 4.1 -so long as some formula does.

Definition 4.3 Suppose that S is a constraint language and that A is a set of assignments over the same variable set V. Define the candidateS-formula for A to be the set containing all constraints (over V and with relation in S) that are satis­ fied by every assignment in A. Similarly, define the candidate S-formula for A with constants to be the set containing all constraints with constants (over V and with relation in S) that are satisfied by every assignment in A.

Lemma 4.4 Suppose that S is a constraint language and that A is a set of assignments over a variable set V. Let P be a subset of V, and let 'lj;c be the candidate S -formula (with constants) for A. There exists an S-formula (with con­ stants) ¢ such that A c::;; MinModels(¢, P) if and only if A c::;; MinModels('lj;c, P).

For a fixed constraint language S, the candidate S­ formula for a set of assignments A can be computed in polynomial time (measured with respect to the size of the representation of A). By the key property of the candidate formula (Lemma 4.4), it follows that INVERSE MIN SAT(S) is in co-NP: an assignment (3 which is not included in A, satisfies the S-candidate formula of A, and is strictly below an assignment in A (with respect to ~p), serves as a succinct and efficiently checkable proof that A is a "no" instance of INVERSE MIN SAT(S). (By similar reasoning, INVERSE SATc(S) and INVERSE EXACT MIN SATc(S) can be shown to be in co-NP, as discussed in [Kavvadias and Sideri, 1998].)

Whenever the model checking problem MIN SAT(S) is in P, the inverse problem INVERSE MIN SAT(S) will be in P. This is because deciding whether or not an input set A to the INVERSE MIN SAT(S) problem is a "yes" instance amounts to verifying that every assignment in A is a min­ imal model of the candidate formula for A; clearly, this can be done in polynomial time when MIN SAT(S) is in P. To prove a full dichotomy theorem on the complexity of INVERSE MIN SAT(8), it remains to describe the complex­ ity of INVERSE MIN SAT(8) for the constraint languages 8 such that MIN SAT(8) is not in P.

5 Dichotomy Theorem

In this section, we describe completely the complexity pro­ file of the "inverse circumscription problem." In partic­ ular, we show that for those constraint languages 8 such that MIN SAT(8) is co-NP-hard, INVERSE MIN SAT(8) is also co-NP-hard (and similarly for MIN SATc(8) and INVERSE MIN SATc(8)).

Our first step is to prove hardness of the INVERSE MIN SAT(8) problem for 9-SAT formulas , where the circumscription is performed with respect to all of the variables. This initial hardness result is then used to establish the hardness of INVERSE MIN SAT(8) for other constraint languages 8.

Theorem 5.1 The problem INVERSE MIN SAT(8 9 ) is co-NP-hard, even with the restriction that the subset P must be equal to the entire variable set.

The proof of this theorem is sketched in Appendix A; the hardness result claimed by the theorem is achieved by re­ duction from the MIN SAT(S) problem. The hardness of INVERSE MIN SAT(8 9 ) can then be leveraged to establish the hardness of INVERSE MIN SATc(8), for the remaining constraint languages 8.

Theorem 5.2 Let S be a constraint language. If 8 is non­ Schaefer, then INVERSE MIN SATc(8) is co-NP-hard.

Then, constants can be "removed" in such a way that allows the hardness of INVERSE MIN SAT(8) to be estab­ lished, based on the hardness ofiNVERSE MIN SATc(8).

Theorem 5.3 Let S be a constraint language. If 8 is neither 0-valid nor Schaefer, then INVERSE MIN SAT(8) is co-NP­ hard.

Collecting together the theorems of this section as well as the discussion at the end of Section 4, we have the following dichotomy theorem.

Theorem 5.4 Let 8 be a constraint language.

If 8 is Schaefer, then INVERSE MIN SATc(8) is in P; oth­ erwise, INVERSE MIN SATe( B) is co-NP-complete.

If 8 is 0-valid or Schaefer, then INVERSE MIN SAT(8) is in P; otherwise, INVERSE MIN SAT(8) is co-NP-complete.

6 Conclusions and Future Work

In this paper, we formalized and studied inverse circumscrip­ tion. We established a full dichotomy theorem in the com­ plexity of this problem (Theorem 5.4). A fascinating phe­ nomenon is that the complexity of inverse circumscription reflects exactly the complexity of model checking for circum­ scription (Theorem 3.6). This correspondence in complex­ ity parallels the intimate relationship between the complexity of inverse satisfiability (Theorem 3.4) and that of satisfiabil­ ity (Theorem 3.2). The resemblance between the results on circumscription and those on propositional logic seems quite strong, as the hardness of inverse circumscription is estab­ lished by reduction from model checking for circumscription -just as the hardness of inverse satisfiability is established by reduction from satisfiability [Kavvadias and Sideri, 1998].

It would be of great interest to investigate further the re­ lationship between "inverse" problems (mapping an explicit description to an implicit description) and more classical "for­ ward" problems (mapping an implicit description to an ex­ plicit description). A concrete goal for future work is to study inverse problems for other non-monotonic reasoning formalisms.

Acknowledgements. The author wishes to thank Bart Sel­ man for useful discussions and suggestions, and Joe Halpern for his advice on the preparation of the final version of this paper.

A Proof Sketch of Theorem 5.1

Definition A.l Let A be a set of assignments over the vari­ able set V. For k ~ 1, we say that an assignment b : V -+ {0, 1} is k-compatible with A if for every size k subset W of V, there exists an assignment a E A such that a1w = b1w·

Lemma A.2 Let 8 be a constraint language with maximum arity k, and let A be a set of assignments over the variable set V. Suppose that '1/Jc is the candidate 8-formulafor A (with k ~ 1). If b is r-compatible with A for all r = 1, ... , k, then b satisfies '1/Jc. Moreover, the converse holds if 8 = 8k.

Definition A.3 Let 8 be a constraint language. For r ~ 1, an r-pattern of an 8-formula ¢over Vis a pair (W, T) such that JWJ = r, W ~ V, T : W -+ {0, 1} is an assignment to the variables of W, and for all clauses R(x1. . . . , Xk) E ¢, ifT is defined on the variables of R(x1, ... , Xk) (that is, {x1, ... , xk} ~ W), then T satisfies R(x1 , ... , Xk).

In other words, an r-pattem for a formula¢ is a subset W of the variable set of¢ of size r along with an assignment to W which does not falsify any clause of¢.

Before giving the proof, we introduce the following nota­ tion. A vector x of length k is an ordered list of variables (x1, .. . ,xk)· If8 is a bit vector (bi. ... ,bk) E {0, 1}k and x is a vector of length k, we let 8(x) denote the function map­ pingxitobiforalli = 1, ... ,k. IfJ.L: V1-+ {0,1}and v : v2 -+ {0, 1} are assignments with disjoint domains (that is, vl n v2 = 0), by J.L u v we denote the function with do­ main V1 U V2 equal to J.L on V1, and equal to von V2. When i is a vector of variables and f is an assignment defined on the variables of i, we let f1z denote the restriction off to the variables of i. For a positive integer k, we let [k] denote the set { 1, ... , k}.

Proof. By [Kirousis and Kolaitis, 2001a, Theorem 3.8], the version of MIN SAT( 8 3 ) where the variable set Pis promised to be the entire variable set is co-NP-complete. To prove hardness of INVERSE MIN SAT(8 9 ), we give a reduction from this version of MIN SAT(8 3 ) . In particular, given a 5 3 - formula ¢ and an assignment a satisfying ¢, we create a set of assignments A over a variable set X such that there is an 8 9 formula '1/J with A ~ MinModels( '1/J, X) if and only if a is a minimal model of¢. (By a minimal model of¢, we mean a minimal model with respect to the entire variable set of¢.)

We let V = { v1 , ... , Vn} denote the variable set of ¢, and we assume without loss of generality that n > 9. For all i E [n], let x1, x1 , and xJ be vectors of length 3. For all i E [n] and j E [m], let y{ be a vector of length 2. Let X i denote the set containing all 9 + 2m variables in the vectors x1,x1,x1 andyf, ... ,yf'. Let X= UiE[n]Xi.

Let a = (0, 0, 1), f3 = (1, 0, 1), and"'( = (0, 1, 0). Let cr = (0, 1) and T = (1, 0). The essential properties of these vectors that we will use are that for any vector z of length 3, a(Z) < f3(Z), a(Z)..l"'((Z), and f3(Z)..l"'((Z); and, for any vector zoflength 2, cr(Z)..lT(Z) .

For i E [n], define ai : Xi ---+ {0, 1} to be { a(x1 ), a(x1), a(x1n u ukE[m] T(y1) . Similarly, for i E [n], define f3i : x i ---+ {0, 1} to be {f3(x1 ), f3(x1), f3(x1)} u UkE[m] T(y1). For i E [n] and j E [mj, define "'f{ : x i ---+ {0, 1} to be {"Y(x1),"Y(x1),"'f(x1)} u {cr(yf)} u ukE[m] ,k;>fj T(y1) .

Let (W1, T1) , . . . , (Wm, Tm) be all of the 9-patterns of¢. Our set of assignments A will be of size m + 1: it will have one assignment ai : X ---+ {0, 1} for each of the 9-patterns (Wi, Ti), as well as one assignment a : X ---+ {0, 1} encoding the assignment a : V ---+ {0, 1}. The partial assignments { "Y{}, { ai}, and {f3i} will be used as building blocks to define the assignments in A.

Define

Define ai = uiE[nja{.

Also, for any assignment f : V ---+ {0, 1}, define j: X---+ {0,1} to be the assignment uiE[n],/(v,)=Oai u uiE[n],J(vi)=l f3i·

Define A, the output of the reduction, to be the set {a 1 , ... ,am}u{ii}.

Let us say that a pair of assignments ( d : X ---+ { 0, 1}, c : X ---+ { 0, 1}) is a violating pair if the following four con­ ditions are met: 1) d rf. A, 2) c E A, 3) d < c, and 4) d is 9-compatible with A. Intuitively, a violating pair (d, c) is evidence that there is no S 9 -formula 'ljJ such that A ~ MinModels( 'lj;, X).

More formally, observe that a violating pair exists if and only if there exists a d rf. A and c E A such that d < c and d satisfies the candidate S 9 -formula 'l/Jc for A, by Lemma A.2. This occurs if and only if it is not the case that A ~ MinModels('l/Jc, X), since (as is easily verified) the assignments in A are pairwise incomparable. By Lemma 4.4, it is not the case that A ~ MinModels('l/Jc, X) if and only if for all S 9 -formulas 'lj;, it is not the case that A ~ MinModels('lj;, X). Hence, a violating pair exists if and only if there is no S 9 -formula 'ljJ such that A ~ MinModels( 'ljJ, X).

The remainder of the proof, omitted due to space con­ straints, establishes that a violating pair exists if and only if a is not a minimal model of ¢. This implies the correctness of our reduction, as then we have that there exists no S 9 -formula 'ljJ such that A ~ MinModels( 'lj;, X) if and only if a is not a minimal model of ¢. 0