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.

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

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

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 and denote disjoint sets of propositional atoms. More precisely, and denote generic propositional formulas built on A, B and respectively; 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 is a formula; if and are formulas, then and are formulas. We use the standard Boolean abbreviations: “” for “”, “” for “”, “” for “”. A literal is either an atom (a positive literal) or its negation (a negative literal). (If l is a negative literal , then by “” we conventionally mean rather than .) A clause is a disjunction of literals . A cube is a conjunction of literals is in Conjunctive Normal Form (CNF) iff it is a conjunction of clauses: .

Semantics. Given , a map is a total truth assignment for A. We assume and . We represent as a set of literals . We sometimes represent also as a cube which we denote as “” so that to distinguish the set and the cube representations.

A map s.t. and 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 by assigning to ? (unknown) the unassigned atoms in . 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 [resp. ].

By “apply a partial assignment to ” we mean “substitute all instances of each assigned in 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 and is iff .

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 on A, the sentence “satisfies ”, written “”, is defined recursively on the structure of as follows: if and only if if and only if if and only if and . (The definition of for the other connectives follows straightforwardly from their definition in terms of is satisfiable iff for some total truth assignment on is valid (written “”) iff for every total truth assignment on entails (written “”) iff, for every total assignment on A, if then and are equivalent iff and . Consequently: is unsatisfiable iff is valid; iff is valid; a clause is valid (aka is a tautology) iff both and occur in it for some ; 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 be formulas on A.

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 for some B by applying (variants of) Tseitin CNF-ization [22], consisting e.g. in applying recursively bottom-up the rewriting rule:

until the resulting formula is in CNF, where are literals, and CNF() is the validity-preserving CNF conversion based on DeMorgan rules (e.g., 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 , written “”, iff exists a total truth assignment on B s.t. . We call the Shannon expansion ] of the existentially-quantified formula the propositional formula on A defined as

Notice that some may be inconsistent or . The following property derives directly from the above definitions.

Property 3. Let be a formula on and be a total truth assignment on A. Then iff .

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 (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 and , 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 s.t. M < N and s.t. each is a cube and is valid and does not contain occurrences of the atoms . Then but is the valid formula , 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 be formulas on A.

From Definition 2 we easily derive the following.

Property 5. Let be a partial truth assignment on A and be formulas on A.

(iii) iff is a valid formula, not necessarily (also, in general ). (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.

Fig. 3. Left: OBDD for . 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 branches.

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 is the result of Tseitin CNF-izing , then:

Example 3. Consider and its Tseitin CNF-ized version:

On the one hand, is such that . On the other hand, there is no total truth assignment on s.t. . In fact, neither nor .

Consider and its Tseitin CNF-ized version:

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, iff is , that is, iff there exists some s.t. is , that is, iff there exists some s.t. evaluates 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 if and only if, there exists a total truth assignment on B s.t. .

Property 6. Let be a formula on and be a partial assignment on A. Then iff .

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 iff, for every total assignment s.t. , 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 , written , 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 and be a partial assignment on A. Then iff .

Notice the nesting order of forall/exists in Definition 4: “for every exists s.t. ...”. In fact, distinct ’s may satisfy distinct disjuncts in ], requiring thus distinct ’s.

Due to Proposition 1 and Property 3 we have that (Definition 3) is strictly stronger than (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 ] is not in CNF even if is in CNF.)

Example 4. Consider and the tautology-free CNF formula on :

Then we have that ∧ ¬∧ ¬∨ ⊥ so

that but . Thus, we have that but .

4.1 A Relevant Example Application: Predicate Abstraction.

Given a propositional formula on B and a set of formulas on B denoting relevant “predicates” and a set A of fresh proposition s.t. each labels , then the Predicate Abstraction of wrt. is defined as follows [12]:

is typically computed as disjunction of mutually-inconsistent partial assignments (cubes) on A s.t. and is equivalent to [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 entailing to keep them small and hence reduce their number, most algorithms can reveal only when evaluates to true it, and are thus incapable of producing partial assignments s.t. and . This happens every time that, for some and some on (subsets of) , both and are satisfi- able but they are satisfied by distinct sets of assignmets on B (Definition 4), so that but .

Example 5. Consider the CNF formula and the ”predicate” CNF formulas and . Then

Both and evaluate to true , whereas entails it without evaluating to true it. Thus, if the algorithm is able to detect if and , then it can return (6), otherwise it can only return (5).

Therefore, having algorithms able to stop extending as soon as , even when , 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: 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.