The Inverse Satisfiability Problem.
We study the complexity of telling whether a set of bit-vectors represents the set of all satisfying truth assignments of a Boolean expression of a certain type. We show that the problem is coNP-complete when the expression is required to be in conjunctive normal form with three literals per clause (3CNF).  We also prove a dichotomy theorem analogous to the classical one by Schaefer, stating that, unless P=NP, the problem can be solved in polynomial time if and only if the clauses allowed are all Horn, or all anti-Horn, or all 2CNF, or all equivalent to equations modulo two.
Introduction
. Logic deals with logical formulae, and more particularly with
the syntax and the semantics of such formulae, as well as with the interplay between
these two aspects [CK90]. In the domain of Boolean logic, for example, a Boolean
formula OE may come in a variety of syntactic classes-conjunctive normal form (CNF),
its subclasses 3CNF, 2CNF, Horn, etc.- and its semantics is captured by its models
or satisfying truth assignments, that is, the set -(OE) of all truth assignments that
satisfy the formula (see Figure 1 for an example).
Going back and forth between these two representations of a formula is therefore
of interest. One direction has been studied extensively from the standpoint of computational
complexity: going from OE to -(OE). In particular, telling whether
is the famous satisfiability problem (SAT), which is known to be NP-complete in its
generality and its special case 3SAT, among others, and polynomial-time solvable in
its special cases Horn, 2SAT, and exclusive-or [Co71, Sc78, Pa94]. All in all, this
direction is a much-studied computational problem. In this paper we study, and in a
certain sense completely settle, the complexity of the inverse problem, that is, going
from -(OE) back to OE. That is, for all the syntactic classes mentioned above, we identify
the complexity of telling, given a set M of models, whether there is a formula OE
in the class (3SAT, Horn, etc.) such that We call this problem inverse
satisfiability.
Besides its fundamental nature, there are many more factors that make inverse
satisfiability a most interesting problem. A major motivation comes from AI (in fact,
what we call here the inverse satisfiability problem is implicit in much of the recent AI
literature [Ca93, DP92, KKS95, KKS93, KPS93]). A set of models such as those in

Figure

1(b) can be seen as a state of knowledge. That is, it may mean that at present,
for all we know, the state of our three-variable world can be in any one of the three
states indicated. In this context, formula OE is some kind of knowledge representation.
In AI there are many sophisticated competing methods for knowledge representation
Received by the editors April 24, 1995; accepted for publication (in revised form) November
20, 1996; published electronically June 15, 1998. This work was partially supported by the Esprit
Project ALCOM II and the Greek Ministry of Research (\PiENE\Delta program 91E\Delta648).
http://www.siam.org/journals/sicomp/28-1/28511.html
y Department of Mathematics, University of Patras, Patras, Greece (djk@math.upatras.gr).
z Department of Computer Science, Athens University of Economics and Business, Athens, Greece
(mss@dias.aueb.gr).
(a)
(b)
Fig. 1. A Boolean formula in 3CNF (a), and the corresponding set of models (b).
(Boolean logic is perhaps the most primitive; see [GN87, Le86, Mc80, Mo84, Re80,
SK90]), and it is important to understand the expressibility of each. This is a form
of the inverse satisfiability problem.
The inverse satisfiability problem was also proposed in [DP92] as a form of discovering
structure in data. For example, establishing that a complex binary relation
is the set of models of a simple formula may indeed uncover the true structure and
nature of the heretofore meaningless table. [DP92] only address this problem in certain
fairly straightforward cases. The problem of learning a formula [AFP92] can be
seen as a generalization of the inverse satisfiability problem.
A recent trend in AI is to approximate complex formulae by simple ones, such as
Horn formulae [SK91, KPS93, GPS94]. Quantifying the quality and computational
feasibility of such approximations also involves understanding the inverse satisfiability
problem.
The basic computational problem we study is this: given a set of models M , is
there a CNF formula OE with at most three literals per clause, such that
We call this problem INVERSE 3SAT. Our first result is that INVERSE 3SAT is
coNP-complete (Theorem 1).
Note. INVERSE 3SAT, as well as all other problems we consider in this paper,
can be solved in polynomial time if the given m \Theta n table M has
if there are exponentially many models in M . The interesting cases of the problem
are therefore when
There are three well-known tractable cases of SAT: 2SAT (all clauses have two
literals), HORNSAT (all clauses are Horn, with at most one positive literal each,
and its symmetric case of anti-Horn formulae, in which all clauses have at most one
negative literal), and XORSAT (the clauses are equations modulo two). Schaefer's
elegant dichotomy theorem [Sc78] states that, unless P=NP, in a certain sense these
are precisely the only tractable cases of SAT. Interestingly, the inverse problem for
these three cases happens to also be tractable! That is, we can tell in polynomial
time if a set of models is the set of models of a Horn (or anti-Horn) formula, of a
2CNF formula, or of an exclusive-or formula (interestingly, the latter two results were
in fact pointed out by Schaefer himself [Sc78], while the first, left open in [Sc78], is
from [DP92, KPS93]). The question comes to mind: are there other tractable cases of
the inverse problem? Our Theorem 2 answers this in the negative; rather surprisingly,
a strong dichotomy theorem similar to Schaefer's holds for the inverse satisfiability
problem as well, in that the problem is coNP-complete for all syntactic classes of CNF
formulae except for the cases of Horn (and anti-Horn), 2CNF, and exclusive-or. The
proof of our dichotomy theorem draws from both that of Theorem 1 and Schaefer's
proof, and in fact strengthens Schaefer's main expressibility result (Theorem 3.0 in
[Sc78]).
154 DIMITRIS KAVVADIAS AND MARTHA SIDERI
2. Definitions. Most of the nonstandard terminology used in this paper comes
from [Sc78].
be a set of Boolean variables. A literal is a variable or its
negation. A model is a vector in f0; 1g n , intuitively a truth assignment to the Boolean
variables. We denote by - and - the logical or and and, respectively. We also extend
this notation to bitwise operations between models. If t is a model, we denote by t i
the constant (i.e., 0 or 1) in the ith position of t.
A k-place logical relation is a subset of f0; 1g k (k integer). We use the notation [OE],
where OE is a Boolean formula, to denote the relation defined by OE when the variables
are taken in lexicographic order. Let R be a logical relation. Call R Horn if it is
logically equivalent to a conjunction of clauses, each with at most one positive literal.
We call it anti-Horn if it is equivalent to a conjunction of clauses with at most one
negative literal. We call it 2CNF if it is equivalent to a 2CNF expression. Finally, we
call it affine if it is the solution of a system of equations in the two-element field.
be a set of Boolean relations. An S-clause (of arity
is an expression of the form R(a is a k-ary relation in S and the
a i 's are either Boolean literals or constants (0 or 1). Given a truth assignment, we
consider an S-clause to be true if the combination of the constants, if any, and the
values assigned to the variables form a tuple in R. Define an S-formula to be any
conjuction of S-clauses defined by the relations in S.
The generalized satisfiability problem is the problem of deciding whether a given
S-formula is satisfiable. Schaefer's dichotomy theorem [Sc78] states that the satisfiability
of an S-formula can be decided in polynomial time in each of the following
cases: (a) all relations in S are Horn, (b) all relations in S are anti-Horn, (c) all
relations in S are 2CNF, (d) all relations in S are affine. In all other cases the
problem is NP-complete. That is, Schaefer's result totally characterizes the complexity
of the CNF satisfiability problem where in addition, the clauses are allowed to
be arbitrary relations of bounded arity. It is interesting to note that several restricted
forms of SAT such as ONE-IN-THREE 3SAT, NOT-ALL-EQUAL 3SAT
etc., all follow as special cases of generalized satisfiability (see [GJ79, Pa94]). To
make this point more clear, notice that the problem ONE-IN-THREE 3SAT can be
considered as a set of four 3-ary relations g. The first relation is
and corresponds to the S-clause R 1
relation is ff0; 0; 0g; f1; 1; 0g; f1; 0; 1gg and corresponds to the S-clauses with one
negated literal, e.g., R 2
For any Boolean formula OE we denote by -(OE) its set of models. We say that a
set of models M is a 3CNF set (kCNF in general) if there is a formula OE in 3CNF
(respectively, kCNF) such that -(OE). Notice that for any model set M we can
construct a kCNF formula that has M as its model set, but in general, this may
require extra existentially quantified variables.
Based on the above we define the INVERSE SAT problem for a set of relations
S as follows.
Given a set M ' f0; 1g n , is there a conjunction of S-clauses over n variables that
has M as its set of models?
Our main result states that if the relations fall in each of the four cases above,
the INVERSE SAT problem is also polynomial. Otherwise it is coNP-complete.
Notice that we have excluded S from being part of the instance since we want to
emphasize that INVERSE SAT is actually a collection of infinitely many subproblems.
This means that all relations of S are of constant arity. Otherwise, relations of non-
constant arity could have exponentially many tuples and the problem becomes trivially
intractable.
In the next section we prove that the INVERSE SAT problem is coNP-complete
for 3CNF formulas. This proof includes the main construction that will be used in
the proof of the main theorem in the last section. This last proof makes use of an
expressibility result which is interesting on its own and partially relies on Schaefer's
main theorem but with several interesting extensions.
3. coNP-completeness of inverse 3SAT. We begin this section with a technical
definition that will be used throughout the paper.
Definition. Let n be a positive integer and let M ' f0; 1g n be a set of Boolean
vectors. For k ? 1, we say that a Boolean vector m 2 f0; 1g n is k-compatible with M
if for any sequence of k positions a vector in M
that agrees with m in these k positions.
The above definition implies that a vector m 2 f0; 1g n is not k-compatible with a
set of Boolean vectors M if there exists a sequence of k positions in m that does not
agree with any vector of M . The following is a useful characterization of kCNF sets.
Lemma 1. Let M ' f0; 1g n be a set of models. Then the following are equivalent.
(a) M is a kCNF set.
Proof. Let OE M be the conjuction of all possible kCNF clauses defined on n variables
and satisfied by all models in M . Notice that OE M is the most restricted kCNF
formula (in terms of its model set) which is satisfied by all models in M . Hence if
(a) holds,
does not satisfy at
least one clause of OE M and concequently disagrees with all models in M in the same k
positions corresponding to the variables in the clause, that is, m is not k-compatible
with M .
Conversely, assume that any model not in M is not k-compatible with M . Then
means m does not satisfy OE differs from all members of M in some k
positions, so the k-clause indicating the complement of m in those k positions is in
does not satisfy OE M . So is a kCNF set.
The INVERSE 3SAT problem is this: given a set of models M , is it a 3CNF set?
We now state our first complexity result.
Theorem 1. INVERSE 3SAT is coNP-complete.
Proof. Lemma 1 establishes that the problem is in coNP: given a set M of models,
in order to prove that it is not a 3CNF set, it suffices to produce a model
that is 3-compatible with M (obviously, 3-compatibility can be checked in polynomial
time). Alternatively, given M , we immediately have a candidate 3CNF formula OE
the conjunction of all 3CNF clauses that are satisfied by all models in M . Thus M is
not a 3CNF set iff there is a model not in M that satisfies OE M .
To prove coNP-completeness, we shall reduce the following well-known coNP-complete
problem to INVERSE 3SAT: given a 3CNF formula, is it unsatisfiable?
Given a 3CNF formula / with n - 4 variables and c clauses, we shall construct a set
of models M such that M is 3CNF iff / is unsatisfiable.
The set M will contain
models, one for each set W of three variables,
and each truth assignment T to these three variables that does not contradict a clause
of / (since we may assume that / consists of clauses that have exactly three literals
each). Let W be a set of three variables chosen among the variables fx of
formula /, and let T : W 7! f0; 1g be a truth assignment to the variables of W , such
that / does not contain a clause not satisfied by T . Consider some total order among
the pairs (W; T ), say the lexicographic one. The set M will contain a model mW;T
for each W and T and no other model.
Every boolean vector mW;T is a concatenation
of the
encodings - T
occuring in the formula /. The encoding - T
of a variable x is a Boolean vector of length and is defined as follows:
positions
z -
where (W; T ) is the ith pair in the total order mentioned above. Notice that if x 2 W ,
the value of x in T is determined by the first two positions of - T
the code 01 stands
for the value 1, and the code 10 stands for x being 0. In these two cases we call the
string - T
W (x) a value pattern. When x 62 W , the code 00 in the first two positions
denotes the absence of x from W , while the rest of the string uniquely determines
the pair (W; T ). In this case we call the string - T
W (x) a padding pattern. Notice that
by our construction in a vector
are exactly
occurences of the unique padding pattern for (W; T ), while the remaining three are
value patterns. Hence, the length of each Boolean vector mW;T is n(k
there is no exponential blow-up in the construction of the set M .
The proof of Theorem 1 now rests on the next claim.
Claim. There is a model not in M that is 3-compatible with M if and only if /
is satisfiable.
Proof of the claim. For the moment, consider a Boolean vector
where the length of each substring m i 2. It is obvious that if the model
m is 3-compatible with M , then it is 3-compatible in the positions restricted to one
substring That is, if we take three arbitrary positions of m i ,
there is a vector mW;T in M that agrees with m i in these three positions. The 3-
compatibility of m i with M also implies something stronger: that there is a vector
which contains a substring - T
To see this, first
assume that m i does not have the value 1 in any position j for 3 2. Then
3-compatibility forces m i to have the values 0 and 1 or 1 and 0 in the first and second
positions; i.e., m i is a value pattern. Now, if m i has the values 0 and 1 in positions
2, then the values in any triple of positions that includes
positions can only agree with the values in the same positions of a specific
model of M , namely, the one having the padding pattern with 0 in position
and 1 in position j. Therefore, m i is identical to this padding pattern. In this case,
however, an analogous observation shows that the whole 3-compatible model m is
identical to the model of M that has this pattern. So if m is 3-compatible with M ,
either it is in M or it consists of value patterns only.
Assume now that there exists a model
2 M that is 3-compatible with M . As
already proved, this model consists only of value patterns m i . Model m
encodes a satisfying truth assignment to the variables of /. For suppose it did conflict
with a clause c of / over variables fx i g. Consider the three value patterns
in the positions of the variables of c. Since m is 3-compatible with M
and each value pattern contains only one 1, we can conclude that there exists a model
which encodes a truth assignment T to the set of
variables such that - T
But since by construction T does not contradict a clause of /, we couldn't have
conflicted with a clause of /. Therefore, the Boolean vector is an
encoding of a satisfying assignment to the variables for formula /: string m i is an
encoding of the truth value assigned to the variable x i for each
formula / is satisfiable since every clause of / is satisfied by the truth assignment
described by vector m.
Conversely, assume that / is satisfiable; i.e., there exists a satisfying truth assignment
s for the variables fx g. Construct the model
concatenation of value patterns, where every string m i is defined as follows:
positions
z -
Obviously, model m is not included in the set M , since every model in M contains a
padding pattern. Suppose that m is not 3-compatible with M . In this case m contains
three positions that do not agree with any model in M . Since m is a concatenation
of value patterns, it must contain three substrings
assignment T for the set of variables such that the pair (W; T ) is not
encoded in any model of M . All
sets of variables are, however, examined during
the construction of M , and the only truth assignments that are not encoded are those
conflicting with a clause of /. Since T does not conflict with any clause-because it
is a restriction of s to three variables-we conclude that the pair (W; T ) is encoded
in some model of M . Hence, m is 3-compatible with M . So, if / is satisfiable, there
exists a model 3-compatible with M , specifically the model encoding a satisfying truth
assignment.
4. The dichotomy theorem. Our main result is the following generalization
of Theorem 1.
Theorem 2. The INVERSE SAT problem for S is in PTIME in each of the
following cases.
(a) All relations in S are Horn.
(b) All relations in S are anti-Horn.
(c) All relations in S are 2CNF.
(d) All relations in S are affine.
In all other cases, the INVERSE SAT problem for S is coNP-complete.
[Sc78] proves a surprisingly similar dichotomy theorem for SAT: SAT is in PTIME
for all of these four classes, and NP-complete otherwise. Our proof is based on an
interesting extension of Schaefer's main result, explained below.
Definition. Let S be a set of Boolean relations and let R be another Boolean
relation, of arity r. We say that S faithfully represents R if there are binary Boolean
functions s such that there is a conjunction of S-clauses over the variables
which is logically equivalent to the formula
s
for some That is, S-clauses can express R with the help of
uniquely defined auxiliary variables.
This is a substantial restriction of Schaefer's notion of ``represents,'' which allows
arbitrary existentially quantified conjunctions of S-clauses (our definition only allows
quantifiers which are logically equivalent to 9!x). Hence our main technical result
below extends the main result of [Sc78, Theorem 3.0]. Independently, Creignou and
Hermann [CH96] have defined the concept "quasi-equivalent," which is the same as
the concept of "faithful representation" defined in this paper.
Theorem 3. If S does not satisfy any of the four conditions of Theorem 2; then
faithfully represents all Boolean relations.
Proof. Assuming that none of the four conditions are satisfied by S, the proof
proceeds by finding more and more elaborate Boolean relations that are faithfully
represented by S. Notice that, since the notion of faithful representation was defined
as equivalence of two S-formulas, we shall restrict the proof to the construction of
appropriate S-clauses-faithful representation of the corresponding relations will then
follow immediately. In this process the allowed operations must preserve the uniqueness
of the values of the auxiliary variables and produce a formula which is also in
conjuctive form. Therefore, if C and C 0 are S-formulas, the allowed operations are:
(a) C - C 0 , i.e., conjuction of two S-formulas, (b) C[a=x], i.e., substitution of a variable
symbol by another symbol, (c) C[0=x] and C[1=x], i.e., substitution of a variable
by a constant (this is actually a selection of the tuples that agree in the specified
constant), and (d) 9!xC(x), i.e., existential quantification, where the bound variables
are uniquely defined. Some of the steps are provided by Schaefer's proof, and some
are new.
Step 1. Expressing [x j y]. This was shown in [Sc78, Lemma 3.2 and Corollary
3.2.1]. The following exposition is somewhat simpler and is based on the fact that a
set M ' f0; 1g n is the model set of a Horn formula iff it is closed under bitwise -; see
the Appendix and [KPS93].
Let R be any non-Horn relation of S (say of arity k). The closure property
mentioned above implies that there exist models t and t 0 in R such that t - t
Based on R we may define the clause R set a
all positions i where both t i and t i 0 are 0 (resp., 1). Set a x to all positions where
y to all positions where t 1. It is easy to
see that both x and y actually appear in R 0 . (If not, then one of t and t 0 coincides
with their conjunction.) Now 01 and 10 are models of R 0 , but 00 is not. Hence R 0 is
either in addition, S contains a relation which is not anti-Horn,
then a symmetric argument rules out tuple 11, resulting in a clause R 00 which is either
Notice that since this is the case we
shall henceforth feel free to use negative literals in our expressions.
Step 2. Expressing [x -y]. Schaefer shows in Lemma 3.3 that there is an S-clause
involving variables x; y; z whose set of models contains 000; 101; 011, but not 110. The
proof is as follows: it is known (see the Appendix) that an S-clause is affine if and
only if for any three models t is also a model.
Consider, therefore, an S-clause that is not affine and assume that [x j y] can be
represented. By the observation in Step 1 we may negate the variables of the clause in
the positions where t 0 is 1. Now the new S-clause, call it S 0 , is satisfied by the all-zero
truth assignment and moreover by the assignments t 1
not by 0 \Phi t 1
. Construct a new clause R(a 1 ; a is the arity of
positions i where both t 1
are 0, a
both are 1, a
0 is 1, and finally a
0 is
0. The S-clause R defined on x; y; z, has models 000, 011, 101 (corresponding to the
all-zero assignment, t 1
0 of S 0 , respectively), but not 110 (which corresponds
to t 1
We will show that R faithfully represents one of the four versions of or:
Observe that at least two of x; actually occur in
R. If exactly two variables are present in R, then R represents a version of or as
follows: if x and y are present, then R(x; are present, then
are present, then R(y; z). If all three variables
are present, depending on which of the remaining four possible models are also in the
model set of the S-clause, we have sixteen possible relations. Of these, the strongest,
with models identical to the set can be used to define X(x;
(which is true when exactly one of x; y; z is true) as follows: X(x;
and in this case the current step is unnecessary. In each of the other fifteen cases,
we show by exhaustive analysis that there is an R-clause, with one constant, which
represents a version of or. If
then R(0;
then R(x; 0;
Since we can also faithfully
express [w j x], by Step 1, we have all four versions of or.
Step 3. Expressing X(x; z). X is a formula which is satisfied if exactly one
of the three variables has the value 1. It is known (see the Appendix) that an S-
clause is 2CNF iff for any set of three satisfying assignments t 0 , t 1 , t 2 , the assignment
satisfying assignment.
We use this characterization to prove that if a relation set S contains a relation
which is not 2CNF and also contains relations which are not Horn, anti-Horn, and
affine, then X(x; y; z) can be faithfully represented.
Consider an S-clause which is not 2CNF. We may therefore find three satisfying
assignments such that the expression (t
a satisfying assignment. As in the previous step we may negate the variables in the
positions where t 0 has the value 1, resulting in a new clause S 0 , which is satisfied by the
all-zero assignment, by t 1
not by t 1
which is equal to t 1
0 . Set 0 to all positions where both t 1
are 0, x to all
positions where both t 1
are 1, y where t 1
0 is 1, and finally z where
0 is 0. Observe that all three variables actually occur in the constructed
clause R: if x is not present then t 1
0 is identical to the all-zero assignment, a
contradiction; if either y or z is not present then t 1
0 is identical to t 1
again a contradiction. The clause constructed includes models 000,
110, and 101, but not 100. Now the S-clause R(x;
exactly the models 100, 010, and 001; i.e., it is X(x;
Step 4. Expressing [x j (y-z)]. Notice that the expression X(x; s; y)-X(x; t; z)-
X(s; t; u) is equivalent to
Thus we prove that we can faithfully represent a relation in which a variable is logically
equivalent to the or of two other variables. Notice that the auxiliary variables s; t; u
are uniquely defined by the values of y and z.
Step 5. Using repeatedly [x j (y - z)] and [x j y] we can faithfully represent any
clause, and by taking conjunctions of arbitrary clauses we can faithfully represent any
Boolean relation, completing the proof of Theorem 3.
Proof of Theorem 2. Let S be a set of relations satisfying one of conditions (a)-
(d), and let r be the maximum arity of any relation in S; we can solve the inverse
satisfiability problem for S as follows.
Given a set of models M , we first identify in time O(n r jM all S-clauses that
are satisfied by all models in M ; call the conjunction of these S-clauses OE. Clearly,
if there is a conjunction of S-clauses that has M as its set of models, then by the
arguments used in Lemma 1, it is precisely OE. To tell whether the set of models of OE
is indeed M , we show how to generate the set of models of OE with polynomial delay
between consecutive outputs [JPY88]. Provided that such generation is possible, we
can decide whether checking if the generated models belong in M . If
a model not in M is generated, then we reply "no"; otherwise, if the set of models
generated is exactly M , we reply "yes." Observe that the answer will be obtained
after at most jM in overall polynomial time.
Our generation algorithm is based on a more general observation that also explains
the analogy of our dichotomy theorem to the one of Schaefer's. Call a syntactic form
of a Boolean formula hereditary if the substitution of a variable by a constant results
in a new formula of the same syntactic form. Observe that the four cases for which
we claim that the inverse satisfiability problem is polynomial are indeed hereditary
and coincide with the polynomial cases of satisfiability [Sc78].
Theorem 4. If the following two conditions hold for a class of Boolean formulas:
(a) the syntactic form of the class is hereditary, and
(b) the satisfiability problem for the class is in PTIME,
then the models of any formula in the class can be generated with polynomial delay
between consecutive outputs.
Proof. Here is an informal description of the generation algorithm: at each step
we substitute a variable by a constant, first by the value 1 and then by 0. Since
(a) holds, the substitution results in a new formula of the same syntactic form. We
then ask a polynomial-time oracle whether the produced formula is satisfiable. Since
(b) holds, such an oracle exists. If the produced formula is satisfiable, we proceed
recursively and substitute the next variable until all variables have been assigned a
value, in which case we return the model. When at a certain step we are through
with the value 1 for a variable (either by discovering a model or by rejecting the value
because the produced formula is unsatisfiable), we try the value 0, and when finished,
we backtrack to the previous step. It is easy to see that after at most 2n queries to
the oracle (where n is the number of variables) we either generate a new model or we
know that all models of the formula have been generated.
Now, to show coNP-completeness of all other cases, let S be a set of Boolean
relations not satisfying conditions (a)-(d). It is clear that the INVERSE SAT problem
for S is in coNP: let r - 3 be the largest arity of any relation in S. Given a set
of models M , we construct all S-clauses satisfied by all models in M-this takes
time. M is the set of models of a conjunction of S-clauses if and only if all
models not in M fail to satisfy at least one of these S-clauses.
To show completeness, we shall reduce UNSATISFIABILITY, the problem of
telling whether a 3CNF expression / is unsatisfiable, to the INVERSE SAT(S). We
suppose that / is a 3CNF expression on n ? 3r variables. Set M contains a model
for each 3r-tuple of variables and values for these variables that don't contradict any
clause of /. Let k be the cardinality of M , a quantity bounded by a function of r
and of the number of variables and clauses of /. Notice that since r is constant, the
number of models is not exponential. Our construction is a generalization of that of
Theorem 1: we consider some total order among the pairs (W; T ), where W is a set
of 3r variables and T a truth assignment to those variables that does not contradict
any clause of /. Every Boolean vector mW;T in M is a concatenation of two strings:
W .
String fi T
W is a concatenation of the encodings - T
occuring
in the formula /: fi T
The encoding of - T
W (x) of a variable x
is a Boolean vector of length and is defined in the proof of Theorem 1. Notice
that in this construction the unique padding pattern for (W; T ) occurs
in the string fi T
W . Call the length of a string fi T
W .
The string ffl T
W is constructed as follows: we consider all 3CNF clauses on N variables
satisfied by the set of strings fi T
W for all sets of 3r variables W and assignments
T to those variables. Call OE the conjuction of all these clauses. We express OE faithfully
by S-clauses. This will involve auxiliary variables . From the definition
of faithful representation we see that xN+' j f '
however, that each of the auxiliary variables depends on at most
three of the N variables appearing in the 3CNF clauses. This follows from the fact
that we are representing 3CNF clauses, and consequently, we can express each 3CNF
clause separately by S-clauses and then take the conjunction of the representations.
Thus, the overall dependency of an auxiliary variable xN+'
a Boolean function f '
be a string fi T
W .
The values in the s positions of the corresponding string ffl T
are the
values of the auxiliary variables: b
(Note that these
values are stated explicitly, i.e., not encoded as value patterns.) This is where the
concept of faithful representation is necessary: for each string fi T
W there is a unique
string ffl T
W . With ordinary representation the multiple ways to extend a string fi T
W via
the auxiliary variables would result in an exponential increase of our model set.
Let M ' f0; 1g N+s be the constructed set of models. We claim that M is the
set of models of a conjunction of S-clauses iff the original 3CNF expression / is
unsatisfiable.
If / is satisfiable, then M is not the set of models of any rCNF expression.
Consider the model corresponding to the satisfying truth assignment. This model
is a concatenation of two parts: the first has N positions and consists of the value
patterns encoding the values of all variables in the satisfying truth assignment, exactly
as in the proof of Theorem 1, and the second consists of the corresponding values of
the s auxiliary variables. This model is r-compatible with M : any r-tuple restricted
to the first N positions certainly matches a corresponding tuple in some model, by
the construction of M . In fact, when the tuple is restricted to the first part, any
3r-tuple can be matched. This is precisely why an r-tuple that is not restricted to
the first N positions is also r-compatible: by the dependency of each auxiliary value
to at most 3 of the first N , a compatibility of an i-tuple (i - r) in the second part
holds if a 3i-compatibility in the first part holds. Alternatively, instead of looking
at a position in the second part, we can look at the three corresponding positions
of the first part. Therefore, the whole model corresponding to the satisfying truth
assignment is r-compatible with M . It follows by Lemma 1 that M is not rCNF, and
as a result, M is not the set of models of any conjunction of S-clauses (recall that the
maximum arity in S is r).
Suppose then that / is unsatisfiable. Let M 0 be M restricted to the first N
positions. Then M 0 is exactly the set of models of OE (the conjuction of all 3CNF
clauses on N variables which don't disagree with M 0 ) by the reasoning in Theorem 1:
no model is 3-compatible with M 0 except those in M 0 . Since M 0 is the set of models
of OE, it follows that M is the set of models of the corresponding conjunction of S-expressions
that faithfully represents OE.


Appendix

. This appendix contains the proof of the closure properties of Horn,
anti-Horn 2CNF, and affine sets of models, which are used in the proof of Theorem 3.
In what follows, M ' f0; 1g n denotes a set of models.
Sets. M is Horn iff for any two models t; t the model (t - t 0 ) is also
in M .
The proof is based on the following proposition from [KPS93]. If t and t 0 are
bit-vectors we use the notation t - t 0 to denote that t
Proposition. The following are equivalent.
(a) There is a Horn formula whose model set is M .
(b) For each
either there is no t or there is a unique
(c) If t; t
Proof. That (a) implies (c) is easy. To establish (b) from (c), take t 0 to be the -
of all t 00 2 M such that t - t 00 . Finally, if we have property (b), we can construct the
following set of Horn clauses: for each
be the model guaranteed by (b);
create a Horn clause ((
1. It is
easy to see that the set of all these Horn clauses comprises the desired OE.
Anti-Horn Sets. This case is symmetric to the above. Just replace 1 with 0
and - with -.
Sets. M is 2CNF iff for any set of three models t the model
Proof. This was shown in [Sc78, Lemma 3.1B]. We give a different proof, which
is simpler and is based on Lemma 1 for 2. First notice that the model
has the following property. The value of t in each position
is equal to a value, which is the majority among the three values of the
models position (e.g., if the values of models t position i
are (1; 1; 0), respectively, the value of t in position i is 1). Call the outcome of the
operation the majority model of t
Only if: Suppose M is 2CNF. By Lemma 1 any 2-compatible model with M is
in M . It is easy to see that the majority model of any three models is 2-compatible
with these three models.
If: Suppose that the majority model of any set of three models t
also in M . We shall prove that any 2-compatible model with M is in M . We prove
this inductively, by showing that any 2-compatible model is in fact n-compatible.
Consider a model m k-compatible with M and a 1)-tuple of positions in this
model. The k distinct k-tuples of this (k + 1)-tuple agree with some model in M .
Take three of those not necessarily distinct k models. (If the models are less than
three, then .) Notice that any one of those differs in at most one position of
the 1)-tuple with m. Therefore, the (k + 1)-tuple of m agrees with the majority
model of those three models. Hence, m is 1)-compatible with M . Therefore, any
2-compatible model with M is in M and, by Lemma 1, M is a 2CNF set.
Affine Sets. M is affine iff for any three models t
is also in M .
Proof. This fact follows from linear algebra and especially the theory of diophantine
linear equations. It states the intuitive observation (and its converse) that every
convex polytope is the convex hull of its vertices. For more on that see the book of
Schrijver [Sc86].

Acknowledgments

. We are grateful to Christos Papadimitriou for helpful discussions
and suggestions. We are also indebted to the anonymous referees for their
detailed comments and suggestions that decisively helped us improve the presentation
by making it more complete and precise.



--R

Learning conjunctions of Horn clauses
Semantical and computational considerations in Horn approximations
Complexity of generalized satisfiability counting prob- lems
Model Theory
The complexity of theorem-proving procedures
Structure identification in relational data
Computers and Intractability
Logical Foundations of Artificial Intelligence
incremental recompilation of knowl- edge
On generating all maximal independent sets
Horn approximations of empirical data
Reasoning with characteristic models

Making believers out of computers


Computational Complexity
A Logic for default reasoning
The complexity of satisfiability problems
Theory of Linear and Integer Programming
Model preference default theories
Knowledge compilation using Horn approximation
--TR

--CTR
Jean-Jacques Hbrard , Bruno Zanuttini, An efficient algorithm for Horn description, Information Processing Letters, v.88 n.4, p.177-182, November
Lane A. Hemaspaandra, SIGACT news complexity theory column 34, ACM SIGACT News, v.32 n.4, December 2001
Lefteris M. Kirousis , Phokion G. Kolaitis, The complexity of minimal satisfiability problems, Information and Computation, v.187 n.1, p.20-39, November 25,
Lane A. Hemaspaandra, SIGACT news complexity theory column 43, ACM SIGACT News, v.35 n.1, March 2004
coNP-completeness;boolean satisfiability;model;computational complexity;polynomial-time algorithms