
## 4. Querying A Compiled Theory

In evaluating the suitability of a target compilation language to a particular application, the succinctness of the language must be balanced against the set of queries and transformations that it supports in polytime. We consider in this section a number of queries, each of which returns valuable information about a propositional theory, and then identify target compilation languages which provide polytime algorithms for answering such queries. We restrict our attention in this paper to the existence **of polytime algorithms for answering queries, but we do not present the algorithms**
themselves. The interested reader is referred to (Darwiche, 2001a, 2001b, 1999; Bryant, 1986) for some of these algorithms and to the proofs of theorems in Appendix A for others.

The queries we consider are tests for consistency, validity, implicates (clausal entailment), implicants, equivalence, and sentential entailment. We also consider counting and enumerating theory models; see Table 4. One can also consider computing the probability of a propositional sentence, assuming that all variables are probabilistically independent. For the subsets we **consider, however,**
this can be done in polytime whenever models can be counted in polytime.

From here on, L **denotes a subset of language** NNF.

Definition 4.1 (CO, VA) L satisfies CO (VA**) iff there exists a polytime algorithm that maps** every formula Σ from L to 1 if Σ is consistent (valid), and to 0 **otherwise.**
One of the main applications of compiling a theory is to enhance the efficiency of answering clausal entailment queries:
Definition 4.2 (CE) L satisfies CE **iff there exists a polytime algorithm that maps every formula**
Σ from L and every clause γ **from** NNF to 1 if Σ |= γ holds, and to 0 **otherwise.**
A key application of clausal entailment is in testing equivalence. Specifically, suppose we have a design expressed as a set of clauses ∆d =Vi αi **and a specification expressed also as a set of clauses**
∆s =Vj βj **, and we want to test whether the design and specification are equivalent. By compiling**
each of ∆d and ∆sto targets Γd and Γs**that support a polytime clausal entailment test, we can test**
the equivalence of ∆d and ∆sin polytime. That is, ∆d and ∆s are equivalent iff Γd|= βj **for all** j and Γs|= αi **for all** i.

A number of the target compilation languages we shall consider support a direct polytime equivalent test:
Definition 4.3 (EQ, SE) L satisfies EQ (SE**) iff there exists a polytime algorithm that maps every**
pair of formulas Σ, Φ from L to 1 if Σ ≡ Φ (Σ |= Φ) holds, and to 0 **otherwise.**
Note that sentential entailment (SE**) is stronger than clausal entailment and equivalence. Therefore,**
if a language L satisfies SE, it also satisfies CE and EQ.

For completeness, we consider the following dual to CE:
Definition 4.4 (IM) L satisfies IM **iff there exists a polytime algorithm that maps every formula**
Σ from L and every term γ **from** NNF to 1 if γ |= Σ holds, and to 0 **otherwise.**
Finally, we consider counting and enumerating models:
Definition 4.5 (CT) L satisfies CT **iff there exists a polytime algorithm that maps every formula**
Σ from L to a nonnegative integer that represents the number of models of Σ **(in binary notation).**
Definition 4.6 (ME) L satisfies ME iff there exists a polynomial p(.,.) **and an algorithm that** outputs all models of an arbitrary formula Σ from L in time p(n,m), where n is the size of Σ and m **is the number of its models (over variables occurring in** Σ).