Splitting Preserves Satisfiability, Not Equivalence

A naive way to think about the splitting algorithm is to demand equivalent replacement at every step:

$$I\models B_1\leftrightarrow B_2⟹I\models A[B_1]\leftrightarrow A[B_2].$$

This rule is sound, but it is too strong as a requirement for a recursive branch. A branch is not supposed to remain another spelling of the original formula. It is the original formula under an assumption about one atom.

A branch is a restriction

Take

$$A=p\wedge (q\vee r).$$

Splitting on $p$ produces

$$A_p^{\top }=q\vee r,A_p^{\perp }=\perp .$$

Neither branch is globally equivalent to $A$:

$$A\not\equiv q\vee r,A\not\equiv \perp .$$

For example, when $p=\perp$, the original formula is false regardless of $q$ and $r$, while $q\vee r$ may be true. But each replacement is correct in its own case:

$$\models p\to (A\leftrightarrow A_p^{\top }),\models \neg p\to (A\leftrightarrow A_p^{\perp }).$$

The discarded information is carried by the branch condition. Together, the guarded branches are exactly equivalent to the original formula:

$$A\equiv (p\wedge A_p^{\top })\vee (\neg p\wedge A_p^{\perp }).$$

The recursive algorithm can drop the guards because it only asks whether one branch has a model. A model of $A_p^{\top }$ extends with $p=\top$; a model of $A_p^{\perp }$ extends with $p=\perp$. Thus the split preserves satisfiability without preserving equivalence in either branch.

A bad splitting tree

The choice of splitting atom also affects the amount of work. If we split on $q$ first, the algorithm asks about $p$ before it has exposed that $p$ is the decisive gate for the whole formula:

This tree is correct, but it has five leaves. The $p$-test is repeated in both $q$-branches.

A better splitting tree

If we split on $p$ first, the false branch closes immediately and the remaining search is performed only when the conjunction’s gate is open:

This tree has four leaves. The point is not that equivalent replacement is unsound. It is that a satisfiability procedure may safely move to a smaller, non-equivalent branch formula, provided that the branch records the assignment that made the replacement valid. A good splitting tree uses this freedom to expose contradictions early instead of preserving equivalence at every intermediate node.

Can we do better?

In the above, we learned that equivalent replacement is too strict, and implications conditioned on the branch might be better. One possible question we can ask is whether we can replace the strict equivalence ($⟺$) with a weak implication ($⟹$), i.e.,

$$I\models B_1⟹B_2,\text{then}I\models A[B_1]⟹A[B_2],$$

or rather when the above holds.

Before we continue, define a total order $\le$ on $\{0,1\}$ with $0\le 0\le 1\le 1$, which allows converting logical statements into inequalities:

$$\begin{array}{rl}I\models B_1⟹B_2& \mathrm{iff}I(B_1)\le I(B_2)\\ I\models \neg B_1& \mathrm{iff}1-I(B_1)=1\\ & \mathrm{iff}I(B_1)=0\end{array}$$

Negation reverses implication

Consider the negated context $A[B]:=\neg B$. If

$$I\models B_1⟹B_2,\text{equivalently}I(B_1)\le I(B_2),$$

then the order-reversing map $x\mapsto 1-x$ gives

$$I(\neg B_2)=1-I(B_2)\le 1-I(B_1)=I(\neg B_1).$$

Hence

$$I\models A[B_2]\to A[B_1].$$

The implication does not pass through negation unchanged; its direction reverses. Negation is therefore antimonotonic.

Conjunction preserves implication

Consider the conjunctive context $A[B]:=B\wedge C$. Under the order on $\{0,1\}$, conjunction is the minimum:

$$I(A[B])=I(B\wedge C)=\min \{I(B),I(C)\}.$$

If

$$I\models B_1⟹B_2,\text{equivalently}I(B_1)\le I(B_2),$$

then monotonicity of the minimum in each argument gives

$$\min \{I(B_1),I(C)\}\le \min \{I(B_2),I(C)\}.$$

Hence

$$I\models A[B_1]⟹A[B_2].$$

The implication passes through conjunction in the same direction. Conjunction is therefore monotonic in each argument.

Disjunction preserves implication

Consider the disjunctive context $A[B]:=B\vee C$. Under the order on $\{0,1\}$, disjunction is the maximum:

$$I(A[B])=I(B\vee C)=\max \{I(B),I(C)\}.$$

If

$$I\models B_1⟹B_2,\text{equivalently}I(B_1)\le I(B_2),$$

then monotonicity of the maximum in each argument gives

$$\max \{I(B_1),I(C)\}\le \max \{I(B_2),I(C)\}.$$

Hence

$$I\models A[B_1]⟹A[B_2].$$

The implication passes through disjunction in the same direction. Disjunction is therefore monotonic in each argument.

Implication reverses in its antecedent

Implication has truth value

$$I(B\to C)=\max \{1-I(B),I(C)\}.$$

Suppose $I(B_1)\le I(B_2)$. In the antecedent context $A_{\mathrm{ant}}[B]:=B\to C$, negation reverses the order before the maximum is taken:

$$I(A_{\mathrm{ant}}[B_2])\le I(A_{\mathrm{ant}}[B_1]).$$

Hence

$$I\models A_{\mathrm{ant}}[B_2]⟹A_{\mathrm{ant}}[B_1].$$

In the consequent context $A_{\mathrm{con}}[B]:=C\to B$, the maximum preserves the order:

$$I(A_{\mathrm{con}}[B_1])\le I(A_{\mathrm{con}}[B_2]).$$

Hence

$$I\models A_{\mathrm{con}}[B_1]⟹A_{\mathrm{con}}[B_2].$$

Implication is therefore antimonotonic in its antecedent and monotonic in its consequent.

Equivalence has no fixed implication direction

Consider the context $A[B]:=B\leftrightarrow C$. Its truth value is

$$I(A[B])=1-|I(B)-I(C)|.$$

Fixing $C$ reveals two different behaviours:

$$I(A[B])=\{\begin{array}{ll}I(B),& I(C)=1,\\ 1-I(B),& I(C)=0.\end{array}$$

Thus, if $I(B_1)\le I(B_2)$, then

$$\begin{array}{rl}I(C)=1& ⟹I(A[B_1])\le I(A[B_2]),\\ I(C)=0& ⟹I(A[B_2])\le I(A[B_1]).\end{array}$$

Whether implication is preserved or reversed depends on the other argument. Equivalence is therefore neither monotonic nor antimonotonic in either argument.

We observed three different implication preservation behaviours:

1. monotonic: the direction of the implication is preserved
2. antimonotonic the direction of the implication is flipped
3. unknown: the implication isn’t preserved at all

Monotonicity, however, is only a one-level parent-child relation. It would be more beneficial to create a measure to determine the monotonicity behaviour of one variable w.r.t. the root formula, i.e., the formula itself, rather than its immediate parent.

To create such a measure, we introduce the notion of polarity $\mathrm{pol}(F,\pi )\in \{-1,0,1\}$:

• $+1$: monotonic w.r.t. to $F$
• $-1$: antimonotonic w.r.t. to $F$
• $0$: unknown
  where $\pi$ is a position.

Polarity is defined recursively: to determine the polarity of one atom $p$, traverse the path from root to position $\pi$:

More formally:

Definition

Polarity (Propositional Logic)

Let $A$ be a propositional formula. The polarity of an occurrence of a subformula in $A$ is defined recursively from the root of $A$.

We write $\mathrm{pol}(A,\pi )$ for the polarity of the occurrence at position $\pi$ in $A$:

$$\mathrm{pol}(A,\pi )=\{\begin{array}{ll}1& \text{if }\pi =\epsilon ,\\ \mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=B_1\wedge \cdots \wedge B_n\text{ and }\pi ={\pi }^{\prime }.i,\\ \mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=B_1\vee \cdots \vee B_n\text{ and }\pi ={\pi }^{\prime }.i,\\ -\mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=\neg B_1\text{ and }\pi ={\pi }^{\prime }.1,\\ -\mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=B_1\to B_2\text{ and }\pi ={\pi }^{\prime }.1,\\ \mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=B_1\to B_2\text{ and }\pi ={\pi }^{\prime }.2,\\ 0& \text{if }A{|}_{{\pi }^{\prime }}=B_1\leftrightarrow B_2\text{ and }\pi ={\pi }^{\prime }.i.\end{array}$$

An occurrence is called positive, negative, or neutral according as its polarity is $1$, $-1$, or $0$.

Link to original

We call an atom $p$ pure w.r.t. a formula $F$ if one of the two cases is true:

1. every occurrence of $p$ in $F$ has positive ($+1$) polarity, or
2. every occurrence of $p$ in $F$ has negative ($-1$) polarity.
   Purity now allows us to say whether every replacement of $p$ preserves (anti)monotonicity.

We can now define two lemmas:

Definition

Positive Monotonic Replacement (Propositional Logic)

Let $p$ be a pure atom in formula $F$ with positive polarity with $I\models F$. Define

$$I^{\prime }:=I\cup \{p\mapsto 1\}.$$

We can then infer that

$$I^{\prime }\models F,$$

i.e., $I$ with $p$ being true is also a model of $F$.

Link to original

Definition

Negative Monotonic Replacement (Propositional Logic)

Let $p$ be a pure atom in formula $F$ with negative polarity with $I\models F$. Define

$$I^{\prime }:=I\cup \{p\mapsto 0\}.$$

We can then infer that

$$I^{\prime }\models F,$$

i.e., $I$ with $p$ being false is also a model of $F$.

Link to original

Why is this more efficient?

Without polarity information, splitting on $p$ must retain both restrictions:

$$\mathrm{SAT}(F)⟺\mathrm{SAT}(F_p^{\top })\vee \mathrm{SAT}(F_p^{\perp }).$$

Either branch may contain the only model, so a recursive solver may have to search both.

Purity identifies one branch that is sufficient. If $p$ is positive and pure, every model of $F$ can be changed into a model with $p=1$ by the positive-purity lemma. Conversely, every model of $F_p^{\top }$ extends to a model of $F$ by assigning $p=1$. Therefore

$$\mathrm{SAT}(F)⟺\mathrm{SAT}(F_p^{\top }).$$

The negative case is symmetric:

$$\mathrm{SAT}(F)⟺\mathrm{SAT}(F_p^{\perp }).$$

The solver can therefore choose the polarity-compatible value immediately, remove $p$ from the formula, and discard the sibling branch. Schematically, the recursive work changes from

$$T(F)=T(F_p^{\top })+T(F_p^{\perp })+O(|F|)$$

to one of

$$T(F)=\{\begin{array}{ll}T(F_p^{\top })+O(|F|),& p\text{ is positive and pure},\\ T(F_p^{\perp })+O(|F|),& p\text{ is negative and pure}.\end{array}$$

Computing polarities requires only a traversal of the formula, whereas avoiding a branch can remove an entire recursive subtree. This is the structural form of pure-literal elimination: the gain comes not merely from simplifying one formula, but from proving that one half of the search is unnecessary.