b

DiscoverSearch
About
Are You Satisfied by This Partial Assignment?
2020·arXiv
Abstract
Abstract

Many procedures for SAT and SAT-related problems –in particular for those requiring the complete enumeration of satisfying truth assignments– rely their efficiency on the detection of partial assignments satisfying an input formula. In this paper we analyze the notion of partial-assignment satisfiability –in particular when dealing with non-CNF and existentially-quantified formulas– raising a flag about the ambiguities and subtleties of this concept, and investigating their practical consequences. This may drive the development of more effective assignment-enumeration algorithms.

Many procedures for SAT and SAT-related problems (e.g. Analytic Tableaux [21], DPLL [9], OBDDs [5]) rely their efficiency on the detection of partial truth assignments  µsatisfying an input propositional formula  ϕ, which allows to state that (i)  ϕis satisfiable and (ii) all total assignments extending  µsatisfy  ϕ. In particular, when it comes to SAT-based problems requiring the complete enumeration of satisfying assignments (e.g. #SAT [11], Lazy SMT [2], AllSAT and AllSMT [14], satisfiability of modal and description logics [20], Weighted Model Integration [16]), the ability of enumerating satisfying partial assignments which are as small as possible is essential, because each of them avoids the enumeration of the whole subtree of total assignments extending it, whose size is exponential in the number of unassigned propositions.

In this paper we analyze the notion of partial-assignment satisfiability –in particular when dealing with non-CNF and existentially-quantified formulas– raising a flag about the ambiguities and subtleties of this concept, and investigating their practical consequences. We notice, analyze and discuss the following facts.1

First, despite its widespread (implicit) usage in algorithms, there seems to be no general and universally-agreed notion of partial-assignment satisfaction. Most authors do not define partial-assignment satisfaction explicitly, or define it only when dealing with (tautology-free) CNF formulas (e.g. [13]). We stress the fact that this is not simply an issue of the meaning of the word “satisfy”: regardless which “verb” one might use for it (e.g. “satisfy”, “entail”, “imply”, “evaluate to true”,...), we would like a universally-agreed criterion to establishing that, if a partial truth-assignment “verb”s a formula  ϕ, then (i)  ϕis satisfiable and (ii) all total truth assignments extending it satisfy  ϕ.

Second, for (tautology-free) CNF formulas the sentence “a partial truth assignment µsatisfies a formula  ϕ” may be indifferently be interpreted either as “µevaluates to true  ϕ” (i.e. “applying  µto  ϕmakes  ϕtrue”) or as “µentails  ϕ” (i.e. “all total assignments extending  µsatisfy  ϕ”) because in this case the two concepts are equivalent. Consequently, satisfiability and enumeration algorithms for CNF formulas typically use evaluation to true as criterion to conclude that the current partial assignment satisfies the input formula, because it is much cheaper and easier to implement than entailment.

Third, and most importantly, for non-CNF formulas evaluation to true is strictly stronger than entailment, and they have complementary properties. Consequently, whereas using evaluation to true as partial-assignment satisfiability criterion is much cheaper and easier to implement, adopting entailment allows for detecting satisfiability earlier and thus for producing smaller partial truth assignments. We also show that, whereas equivalent formulas are always entailed by the same partial assignments, this is not the case for evaluation to true, that is, equivalent formulas are not always evaluated to true by the same partial assignments. This would be an embarrassing fact if we adopted evaluation to true as the definition of partial-assignment satisfiability for non-CNF formulas. We remark that standard Tseitin-style CNF-ization does not solve these issues, because it may loose information regarding partial-assignment evaluation to true or entailment.

Fourth, the same issues apply also for existentially-quantified formulas, even CNF ones. This is very important, because in many application domains, fundamental operations —like preimage computation in symbolic model checking (see e.g. [6]) or predicate abstraction in SW verification (see e.g. [12,3])— require dealing with existentially-quantified formulas and with the enumeration of partial assignments “satisfying” them.

Fifth, different algorithms handling non-CNF formulas implicitly implement different notions of partial-assignment satisfaction. E.g., Analytic Tableaux [21] and (nonCNF) DPLL [9] implicitly enumerate partial assignment evaluating to true the input formulas, whereas OBDDs [5] implicitly enumerate partial assignment entailing them. Also, e.g., techniques like pure-literal filtering [19,2] in lazy SMT implicitly aim at reducing a total assignment to a partial one evaluating to true the input formula.

Overall, the theoretical considerations above suggest to adopt entailment as general definition of partial-assignment satisfiability, although evaluation to true is a cheaper though less-effective criterion which can (most) often be adopted in actual implementations. However, since partial assignments entailing  ϕare in general subsets of those evaluating to true  ϕ, using entailment rather than evaluation to true as satisfiability criterion allows for producing smaller partial assignments, and hence possibly drastically reducing their number, in particular in the presence of existentially-quantified formulas. This may drive the development of more effective assignment-enumeration algorithms.

Motivation. The analysis presented in this paper was triggered by the effort of conceiving more efficient procedures for predicate abstraction in SMT for improving Weighted Model Integration [16,17], which forced me to elaborate on the distinction between evaluation to true and entailment. Before then, I personally used to see partial-assignment satisfiability as entailment (see [10]) without paying attention to this distinction.

Content. The rest of the paper is organized as follows.  §2 provides the necessary notation, terminology and concepts used in the paper.  §3 introduces evaluation to true and entailment for generic propositional formulas and discusses their relative properties and use.  §4 lifts the discussion to existentially-quantified formulas.  §5 provides some conclusions and future-work suggestions.

image

Fig. 1. Three-value-semantics of  µ(ϕ)in terms of {T, F, ?} (“true”, “false”, “unknown”).

Fig. 2. Propagation of truth values through the Boolean connectives.

image

In this section we introduce the notation and terminology adopted in this paper. Moreover, in order to avoid any ambiguity (although at the risk of being a little pedantic), we recall the standard syntax and semantics of propositional logics, plus some basic facts. Notation. In what follows T, F, ? denote the truth values “true”, “false” and “unknown” respectively;  ⊤, ⊥denote the logic constants “true” and “false” respectively; A, B denote propositional atoms;  ϕ, φ, ψdenote propositional formulas;  µ, η, γdenote truth value assignments. The symbols  A def= {A1, ..., AN}and  B def= {B1, ..., BK}denote disjoint sets of propositional atoms. More precisely,  ϕ, φand  ψdenote generic propositional formulas built on A, B and  A∪Brespectively;  ηand  µdenote total and a partial assignments on A respectively;  δdenote total assignments on B. (All above symbols may possibly have subscripts).

Syntax. A propositional formula is defined inductively as follows: the constants  ⊤and  ⊥(denoting the truth values true and false) are formulas; a propositional atom A1, A2, A3, ...is a formula; if  ϕ1and  ϕ2are formulas, then  ¬ϕ1and  ϕ1 ∧ ϕ2are formulas. We use the standard Boolean abbreviations: “ϕ1 ∨ ϕ2” for “¬(¬ϕ1 ∧ ¬ϕ2)”, “ϕ1 → ϕ2” for “¬(ϕ1 ∧ ¬ϕ2)”, “ϕ1 ↔ ϕ2” for “¬(ϕ1 ∧ ¬ϕ2) ∧ ¬(ϕ2 ∧ ¬ϕ1)”. A literal is either an atom (a positive literal) or its negation (a negative literal). (If l is a negative literal  ¬Ai, then by “¬l” we conventionally mean  Airather than  ¬¬Ai.) A clause is a disjunction of literals �j lj. A cube is a conjunction of literals  �j lj. ϕis in Conjunctive Normal Form (CNF) iff it is a conjunction of clauses: �Li=1�Kiji=1 lji.

Semantics. Given  A def= {A1, ..., AN}, a map  η : A �−→ {T, F}Nis a total truth assignment for A. We assume  η(⊤)def= Tand  η(⊥)def= F. We represent  ηas a set of literals  ηdef= {Ai | η(Ai) = T}∪{¬Ai | η(Ai) = F}. We sometimes represent  ηalso as a cube �η(Ai)=T Ai ∧ �η(Ai)=F ¬Aiwhich we denote as “�η” so that to distinguish the set and the cube representations.

A map  µ : A′ �−→ {T, F}N ′s.t.  A′ ⊆ Aand  N ′ def= ||A′||is a partial truth assignment for A. As with total assignments, we can represent  µas a set of literals or as a cube, denoted with “�µ”. Using a three-value logic we extend  µto A as  µ :A �−→ {T, F, ?}Nby assigning to ? (unknown) the unassigned atoms in  A \ A′. Then we extend the semantics of  µto any formula  ϕon A as described in Figure 1. We say that  µevaluates to true [resp. false]  ϕif  µ(ϕ) = T[resp.  µ(ϕ) = F].

By “apply a partial assignment  µto  ϕ” we mean “substitute all instances of each assigned  Aiin  ϕwith the truth value in  {⊤, ⊥}assigned by  µand then apply recursively the standard propagation of truth values through the Boolean connectives described in Figure 2. We denote by “ϕ|µ” (“residual of  ϕunder  µ) the formula resulting from applying  µto  ϕ. The following fact follows straightforwardly.

Property 1.  ϕ|µis  ⊤iff  µ(ϕ) = Tand  ϕ|µis  ⊥iff  µ(ϕ) = F.

Notice that total assignments are a subcase of partial ones, so that all above definitions and facts apply also to total assignments  η.

Given a total truth assignment  ηon A and some formulas  ϕ, ϕ1, ϕ2on A, the sentence “ηsatisfies  ϕ”, written “η |= ϕ”, is defined recursively on the structure of ϕas follows:  η |= ⊤, η ̸|= ⊥, η |= Aiif and only if  η(Ai) = T, η |= ¬ϕ1if and only if  η ̸|= ϕ1, η |= ϕ1 ∧ ϕ2if and only if  η |= ϕ1and  η |= ϕ2. (The definition of η |= ϕ1 ▷◁ ϕ2for the other connectives follows straightforwardly from their definition in terms of  ¬, ∧.) ϕis satisfiable iff  η |= ϕfor some total truth assignment  ηon  A. ϕis valid (written “|= ϕ”) iff  η |= ϕfor every total truth assignment  ηon  A. ϕ1entails  ϕ2(written ϕ1 |= ϕ2) iff, for every total assignment  ηon A, if  η |= ϕ1then  η |= ϕ2. ϕ1and  ϕ2are equivalent iff  ϕ1 |= ϕ2and  ϕ2 |= ϕ1. Consequently:  ϕis unsatisfiable iff ¬ϕis valid;  ϕ1 |= ϕ2iff  ϕ1 → ϕ2is valid; a clause �i liis valid (aka is a tautology) iff both  Aiand  ¬Aioccur in it for some  Ai; a CNF formula  ϕis valid iff either it is  ⊤or all its clauses are tautologies. We say that a CNF formula is tautology-free iff none of its clauses is a tautology.

The following facts follow straightforwardly and are of interest for our discussion.

Property 2. Let  ηbe a total truth assignment on A and  ϕ, ϕ1, ϕ2be formulas on A.

image

Notice that Property 2(i) justifies the usage of “|=” for both satisfiability and entailment.

CNF-ization. Every generic formula  ϕon A can be encoded into a CNF formula  ψon A ∪ Bfor some B by applying (variants of) Tseitin CNF-ization [22], consisting e.g. in applying recursively bottom-up the rewriting rule:

image

until the resulting formula  ψis in CNF, where  lj1, lj2are literals,  ▷◁ ∈ {∧, ∨, →, ←, ↔}and CNF() is the validity-preserving CNF conversion based on DeMorgan rules (e.g., CNF(B ↔ (l1 ∧ l2))def= (¬B ∨ l1) ∧ (¬B ∨ l2) ∧ (B ∨ ¬l1 ∨ ¬l2)). ψis s.t.  η |= ϕiff exists a total assignment  δon B s.t.  η ∪ δ |= ψ, and the size of  ψis linear wrt. that of  ϕ. Existentially-quantified formulas. A total truth assignment  ηsatisfies  ∃B.ψ, written “η |= ∃B.ψ”, iff exists a total truth assignment  δon B s.t.  η ∪δ |= ψ. We call the Shannon expansion  SE[∃B.ψ] of the existentially-quantified formula  ∃B.ψthe propositional formula on A defined as

image

Notice that some  ψ|δimay be inconsistent or  ⊥. The following property derives directly from the above definitions.

Property 3. Let  ψbe a formula on  A ∪ Band  ηbe a total truth assignment on A. Then η |= ∃B.ψiff  η |= SE[∃B.ψ].

We wish to provide a satisfactory definition of partial-assignment satisfiability for a generic propositional formula —i.e., non necessarily (tautology-free) CNF. One first possibility is to see partial-assignment satisfiability as evaluation to true.

Definition 1. We say that a partial truth assignment  µevaluates to true  ϕiff  µ(ϕ) = T(or, equivalently by Property 1, iff  µ|ϕ = ⊤). We denote this fact with “µ |≈ ϕ”.

One second possibility is to see partial-assignment satisfiability as entailment.

Definition 2. We say that a partial truth assignment  µentails  ϕif and only if, for every total truth assignments  ηs.t.µ ⊆ η, ηsatisfies  ϕ. We denote this fact with “µ |= ϕ”.

Notice that both evaluation to true and entailment are semantic definitions. Due to Property 1, evaluation to true has also an easy-to-check syntactic characterization as “µ|ϕ = ⊤”.

In substance, Definition 1 extends to partial assignments Property 2(iii), whereas Definition 2 extends to partial assignments Property 2(i). Ideally, a suitable definition of partial-assignment satisfiability should verify all statements in Property 2, in particular (ii) and (iv). In practice, unfortunately, at least for generic (non-CNF) formulas, we see this is not the case.

When the formula  ϕis in CNF and does not contain valid clauses –which however are easy to eliminate by preprocessing– then Definitions 1 and 2 are equivalent:  µ |≈ ϕiff  µ |= ϕ. In fact, if  µ |≈ ϕthen, for every  ηs.t.  η ⊇ µ, η |≈ ϕand thus  η |= ϕ, hence µ |= ϕ; also, if  µ |= ϕthen  ϕ|µis a valid CNF formula which does not contain valid clauses, so that  ϕ|µmust be  ⊤, hence  µ |≈ ϕ.

Unfortunately, when dealing with generic (non-CNF) formulas, we notice that Definitions 1 and 2 are not equivalent, the former being strictly stronger than the latter. In fact, as above, if  µ |≈ ϕthen  µ |= ϕ, whereas the converse is not true: e.g., if ϕdef= (A1 ∧ A2) ∨ (A1 ∧ ¬A2)and  µdef= {A1}, then  µ |= ϕbut  µ ̸|≈ ϕ. This leads to the following statement.

Proposition 1. If a partial truth assignment  µevaluates to true  ϕ, then it also entails ϕ, but the converse does not hold.

Example 1. Let  µ def= {A1, .., AM}s.t. M < N and  ϕ def= �i(Ai ∧ cubei)s.t. each cubeiis a cube and �i cubeiis valid and does not contain occurrences of the atoms A1, .., AM. Then  µ |= ϕbut  ϕ|µis the valid formula �i cubei, so that  µ ̸|≈ ϕ. ⋄

We try to build a counterpart of Property 2 for Definitions 1 and 2 respectively, but in both cases we fail to achieve all points (i)-(iv) in Property 2, resulting into complementary situations.

From Definition 1 we easily derive the following. (Here “✓” [resp. “×”] denotesfacts from Property 2 which are [resp. are not] preserved.)

Property 4. Let  µbe a partial truth assignment on A and  ϕ, ϕ1, ϕ2be formulas on A.

image

From Definition 2 we easily derive the following.

Property 5. Let  µbe a partial truth assignment on A and  ϕ, ϕ1, ϕ2be formulas on A.

image

(iii)  × µ |= ϕiff  ϕ|µis a valid formula, not necessarily  ⊤(also, in general  µ(ϕ) ̸= T). (iv)  ×Checking if  µ |= ϕis co-NP-complete. 2

On the one hand, the advantage of adopting evaluation to true for checking partial-assignment satisfiability is that it matches the intuition and practical need that the process of checking it should be fast (Property 4(iv)). On the other hand, the main drawback is that that equivalent although syntactically different formulas may be satisfied by different sets of partial assignments (Property 4(ii)), which looks theoretically awkward.

On the one hand, the advantage of adopting entailment for checking partial-assignment satisfiability is that it matches the intuition and theoretical requirement that equivalent formulas should be satisfied by the same assignments, even partial ones (Property 5(ii)). On the other hand, the price to pay is that the resulting problem is co-NP-complete (Property 5(iv)), because it is equivalent to checking the validity of the residual  ϕ|µ.

Due to Proposition 1, every partial assignments entailing the input formula is a subset of some other(s) evaluating to true it. Therefore, for an assignment-enumeration algorithm, being able to enumerate partial assignments entailing the input formula rather than simply evaluating to true it may (even drastically) reduce the number of the satisfying assignment enumerated.

image

Fig. 3. Left: OBDD for  ϕdef= ((A1 ∧A2)∨(A1 ∧¬A2))∧((¬A3 ∧A4)∨(¬A3 ∧¬A4)). Center and right: Assignment enumeration for  ϕvia Analytic Tableaux and (non-CNF) DPLL.

For instance we notice that, when applied to satisfiable formulas, OBDDs [5] produce branches representing partial assignments which entail the input formula (Defini-tion 2), because if  µ |= ϕthen  ϕ|µis valid (Property 5(iii)), so that its corresponding sub-OBDD is reduced into the  ⊤node. Instead SAT/AllSAT algorithms like Analytic Tableaux 3 [21] or “classic” DPLL 4 [9] produce branches representing partial assignments which evaluate to true the input formula (Definition 1) because, unlike with OBDDs, as soon as it is produced (a branch corresponding to) an assignment  µs.t.  µ |= ϕbut  µ ̸|≈ ϕ, they do not realize it and proceed the search until they extend it to some µ′ ⊃ µs.t.  µ′ |≈ ϕ, extending the search tree of up to  2||µ′||−||µ||branches.

image

One may argue that in SAT/AllSAT the distinction between  |≈and |= is not much relevant in practice, because we can CNF-ize upfront the input formulas —typically by variants of Tseitin CNF-ization— removing tautological clauses, and this distinction does not hold for (tautology-free) CNF formulas. However, we notice that with Tseitin CNF-ization we may loose information regarding entailment or evaluation to true. In fact, if  ψon  A ∪ Bis the result of Tseitin CNF-izing  ϕ, then:

image

image

Example 3. Consider  ϕdef= A1 ∨ (A2 ∧ A3)and its Tseitin CNF-ized version:

image

On the one hand,  µdef= {A1}is such that  µ |≈ ϕ. On the other hand, there is no total truth assignment  δon  {B1}s.t.  µ ∪ δ |≈ ψ. In fact, neither  {A1, B1} |≈ ψnor  {A1, ¬B1} |≈ ψ.

Consider  ϕdef= (A1 ∧ A2) ∨ (A1 ∧ ¬A2)and its Tseitin CNF-ized version:

ψdef= (B1 ∨ B2) ∧

image

In many application domains, fundamental operations —like preimage computation in symbolic model checking (see e.g. [6]) or predicate abstraction in SW verification (see e.g. [12,3])— require dealing with existentially-quantified formulas and with the enumeration of partial assignments satisfying them. Thus, we lift the discussion of  §3 to existentially-quantified formulas, and we wish to provide a satisfactory definition of partial-assignment satisfiability for an existentially-quantified propositional formula.

One first possibility is to see partial-assignment satisfiability as evaluation to true, leveraging Definition 1 and Property 3 to the existentially-quantified case. By (2) and Definition 1,  µ |≈ SE[∃B.ψ]iff  (SE[∃B.ψ])|µis  ⊤, that is, iff there exists some  δis.t. ψ|δi|µis  ⊤, that is, iff there exists some  δis.t.  µ ∪ δievaluates to true  ψ. This leads to the following definition and relative property.

Definition 3. We say that a partial truth assignment  µon A evaluates to true  ∃B.ψif and only if, there exists a total truth assignment  δon B s.t.  µ ∪ δ |≈ ψ.

Property 6. Let  ψbe a formula on  A ∪ Band  µbe a partial assignment on A. Then µ |≈ ∃B.ψiff  µ |≈ SE[∃B.ψ].

One second possibility is to see partial-assignment satisfiability as entailment, leveraging Definition 2 and Property 3 to the existentially-quantified case. We notice that µ |= SE[∃B.ψ]iff, for every total assignment  ηs.t.  η ⊇ µ, η |= SE[∃B.ψ], that is, by Property 3 for every total assignments  ηs.t.  η ⊇ µexists a total assignment  δon B s.t. η ∪ δ |= ψ. This leads to the following definition and relative property.

Definition 4. We say that a partial truth assignment  µon A entails  ∃B.ψ, written µ |= ∃B.ψ, if and only if , for every total truth assignment  ηon A extending  µ, there exists a total truth assignment  δon B s.t.  η ∪ δsatisfies  ψ.

Property 7. Let  ψbe a formula on  A ∪ Band  µbe a partial assignment on A. Then µ |= ∃B.ψiff  µ |= SE[∃B.ψ].

Notice the nesting order of forall/exists in Definition 4: “for every  ηexists  δs.t. ...”. In fact, distinct  η’s may satisfy distinct disjuncts  ψ|δiin  SE[∃B.ψ], requiring thus distinct δi’s.

Due to Proposition 1 and Property 3 we have that  µ |≈ ∃B.ψ(Definition 3) is strictly stronger than  µ |= ∃B.ψ(Definition 4). Remarkably, and unlike with the un-quantified case, this is the case even if  ψis a tautology-free CNF formula! (Intuitively, this can be seen as a consequence of the fact that  SE[∃B.ψ] is not in CNF even if  ψis in CNF.)

Example 4. Consider  µdef= {A1}and the tautology-free CNF formula on  A ∪ B:

image

Then we have that  SE[∃B.ψ] = (A1 ∧ A2∧ ¬A2) ∨ (A1 ∧ A2) ∨ (A1∧ ¬A2)∨ ⊥ so

that  µ |= SE[∃B.ψ]but  µ ̸|≈ SE[∃B.ψ]. Thus, we have that  µ |= ∃B.ψbut  µ ̸|≈ ∃B.ψ.

image

4.1 A Relevant Example Application: Predicate Abstraction.

Given a propositional formula  φon B and a set  Φdef= {φi}iof formulas on B denoting relevant “predicates” and a set A of fresh proposition s.t. each  Ailabels  φi, then the Predicate Abstraction of  φwrt.  Φis defined as follows [12]:

image

PredAbs(φ, Φ)is typically computed as disjunction of mutually-inconsistent partial assignments (cubes)  µjon A s.t.  µj |= PredAbs(φ, Φ)and �j µjis equivalent to PredAbs(φ, Φ)[14,7]. 6

We notice that in the computation of such cubes the distinction between  |≈and |= may be very relevant: whereas it would be desirable to look for partial assignments µjentailing  PredAbs(φ, Φ)to keep them small and hence reduce their number, most algorithms can reveal only when  µjevaluates to true it, and are thus incapable of producing partial assignments  µjs.t.  µj |= PredAbs(φ, Φ)and  µj ̸|≈ PredAbs(φ, Φ). This happens every time that, for some  Akand some  µkon (subsets of)  A \ {Ak}, both  (φ ∧ �i̸=k(Ai ↔ φi))|µk ∧ φkand  (φ ∧ �i̸=k(Ai ↔ φi))|µk ∧ ¬φkare satisfi- able but they are satisfied by distinct sets of assignmets  δon B (Definition 4), so that µk |= PredAbs(φ, Φ)but  µk ̸|≈ PredAbs(φ, Φ).

Example 5. Consider the CNF formula  φdef= (¬B1 ∨ B2) ∧ (B1 ∨ ¬B2)and the ”predicate” CNF formulas  Φ1def= B1 ∧ B2and  Φ2def= ¬B1 ∧ B2. Then

image

Both  {A1, ¬A2}and  {¬A1, ¬A2}evaluate to true  PredAbs(φ, Φ), whereas  {A1}entails it without evaluating to true it. Thus, if the algorithm is able to detect if  µj |=PredAbs(φ, Φ)and  µj ̸|≈ PredAbs(φ, Φ), then it can return (6), otherwise it can only return (5). ⋄

Therefore, having algorithms able to stop extending  µjas soon as  µj |= PredAbs(φ, Φ), even when  µj ̸|≈ PredAbs(φ, Φ), would produce much more compact formulas.

We have shown that, when dealing with non-CNF formulas or with existentially-quantified formulas, we may have two distinct notions of partial-assignment satisfiability, entailment and evaluation to true, with different properties, and that adopting one or the other may influence the effectiveness of assignment-enumeration procedures.

In the next future we wish to investigate the adoption of partial-assignment reduction techniques exploiting entailment rather than evaluation to true, in particular in AllSMT and predicate abstraction. A possible candidate can be Dualization [15]. Also, we wish to investigate the tradeoff between the cost of detecting entailment wrt. the effectiveness in reducing the number of enumerated assignments, in particular when the latter may have computationally-hard consequences (e.g. WMI [16,17]).

The analysis described in this paper strongly benefitted from interesting discussions, either personal or via email, with Armin Biere, Alessandro Cimatti, Allen van Gelder, David Mitchell, Sibylle M¨ohle, Laurent Simon, Armando Tacchella, and Stefano Tonetta, whom are all warmly thanked.

1. A. Armando and E. Giunchiglia. Embedding Complex Decision Procedures inside an Inter- active Theorem Prover. Annals of Mathematics and Artificial Intelligence, 8(3–4):475–502, 1993.

2. C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability Modulo Theories, chapter 26, pages 825–885. In Biere et al. [4], February 2009.

3. D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Software model checking via large-block encoding. In FMCAD, pages 25–32. IEEE, 2009.

4. A. Biere, M. J. H. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability. IOS Press, February 2009.

5. R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug. 1986.

6. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking:  1020 States and Beyond. Information and Computation, 98(2):142–170, June 1992.

7. R. Cavada, A. Cimatti, A. Franz´en, K. Kalyanasundaram, M. Roveri, and R. K. Shyamasun- dar. Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. In FMCAD, pages 69–76. IEEE Computer Society, 2007.

8. M. D’Agostino. Are Tableaux an Improvement on Truth-Tables? Journal of Logic, Language and Information, 1:235–252, 1992.

9. M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7), 1962.

10. F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propo- sitional decision procedures - the case study of modal K(m). Information and Computation, 162(1/2), October/November 2000.

11. C. P. Gomes, A. Sabharwal, and B. Selman. Model Counting, chapter 20, pages 633–654. In Biere et al. [4], February 2009.

12. S. Graf and H. Sa¨ıdi. Construction of abstract state graphs with pvs. In CAV, pages 72–83. Springer, 1997.

13. H. Kleine B¨uning and O. Kullmann. Minimal Unsatisfiability and Autarkies, chapter 11, pages 339–401. In Biere et al. [4], February 2009.

14. S. K. Lahiri, R. Nieuwenhuis, and A. Oliveras. SMT techniques for fast predicate abstraction. In Proc. CAV, LNCS 4144. Springer, 2006.

15. S. M¨ohle and A. Biere. Dualizing projected model counting. In L. H. Tsoukalas, ´E. Gr´egoire, and M. Alamaniotis, editors, ICTAI’18, pages 702–709. IEEE, 2018.

16. P. Morettin, A. Passerini, and R. Sebastiani. Efficient weighted model integration via smt- based predicate abstraction. In IJCAI-17, pages 720–728, 2017.

17. P. Morettin, A. Passerini, and R. Sebastiani. Advanced SMT techniques for weighted model integration. Artificial Intelligence, 275:1–27, October 2019.

18. R. Sebastiani. From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain. In Frontiers of Combining Systems, 6th International Symposium, FroCoS, volume 4720 of LNCS, pages 28–46. Springer, 2007.

19. R. Sebastiani. Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, JSAT, 3(3-4):141–224, 2007.

20. R. Sebastiani and A. Tacchella. SAT Techniques for Modal and Description Logics, chapter 25, pages 781–824. In Biere et al. [4], February 2009.

21. R. M. Smullyan. First-Order Logic. Springer-Verlag, NY, 1968.

22. G. Tseitin. On the complexity of derivation in propositional calculus. In studies in constructive mathematics and mathematical logics, pages 115–125, 1970.


Designed for Accessibility and to further Open Science