Splitting Preserves Satisfiability, Not Equivalence

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

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

Splitting on produces

Neither branch is globally equivalent to :

For example, when , the original formula is false regardless of and , while may be true. But each replacement is correct in its own case:

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

The recursive algorithm can drop the guards because it only asks whether one branch has a model. A model of extends with ; a model of extends with . 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 first, the algorithm asks about before it has exposed that is the decisive gate for the whole formula:

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

A better splitting tree

If we split on 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.,

or rather when the above holds.

Before we continue, define a total order on with , which allows converting logical statements into inequalities:

Negation reverses implication

Consider the negated context . If

then the order-reversing map gives

Hence

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

Conjunction preserves implication

Consider the conjunctive context . Under the order on , conjunction is the minimum:

If

then monotonicity of the minimum in each argument gives

Hence

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

Disjunction preserves implication

Consider the disjunctive context . Under the order on , disjunction is the maximum:

If

then monotonicity of the maximum in each argument gives

Hence

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

Suppose . In the antecedent context , negation reverses the order before the maximum is taken:

Hence

In the consequent context , the maximum preserves the order:

Hence

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

Equivalence has no fixed implication direction

Consider the context . Its truth value is

Fixing reveals two different behaviours:

Thus, if , then

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 :

• : monotonic w.r.t. to
• : antimonotonic w.r.t. to
• : unknown
  where is a position.

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

More formally:

Definition

Polarity (Propositional Logic)

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

We write for the polarity of the occurrence at position in :

An occurrence is called positive, negative, or neutral according as its polarity is , , or .

Link to original

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

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

We can now define two lemmas:

Definition

Positive Monotonic Replacement (Propositional Logic)

Let be a pure atom in formula with positive polarity with . Define

We can then infer that

i.e., with being true is also a model of .

Link to original

Definition

Negative Monotonic Replacement (Propositional Logic)

Let be a pure atom in formula with negative polarity with . Define

We can then infer that

i.e., with being false is also a model of .

Link to original

Why is this more efficient?

Without polarity information, splitting on must retain both restrictions:

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

Purity identifies one branch that is sufficient. If is positive and pure, every model of can be changed into a model with by the positive-purity lemma. Conversely, every model of extends to a model of by assigning . Therefore

The negative case is symmetric:

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

to one of

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.