1.2 Logical Equivalence, Normal Forms, and SAT: Letting Machines Search for Solutions

Suppose a product has four features: database, cache, audit logging, and offline mode. Among them, there are dozens of compatibility constraints. Manually testing every combination quickly becomes unmanageable. By translating these constraints into Boolean formulas, we can ask a precise question: Does there exist a configuration that satisfies all the rules simultaneously?

This is the fundamental form of the SAT (Boolean Satisfiability Problem).

Toolkit for Equivalence Transformations

Common logical equivalences include:

Double negation      ¬¬p ≡ p
De Morgan's laws     ¬(p ∧ q) ≡ ¬p ∨ ¬q
                      ¬(p ∨ q) ≡ ¬p ∧ ¬q
Implication elimination    p → q ≡ ¬p ∨ q
Biconditional        p ↔ q ≡ (p → q) ∧ (q → p)
Distributive laws    p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)
                      p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
Absorption laws      p ∨ (p ∧ q) ≡ p
                      p ∧ (p ∨ q) ≡ p

Each transformation should replace a known equivalent subformula. Simply looking at symbols and saying "they're similar" easily leads to mistakes with De Morgan's laws: when negation passes through parentheses, each atomic proposition must be negated, and the ∧ and ∨ connectives must be swapped.

NNF, CNF, and DNF

Negation Normal Form (NNF) requires the use of only ∧, ∨, and direct negations applied to atomic propositions ¬.

¬(p → (q ∧ r))
≡ ¬(¬p ∨ (q ∧ r))
≡ p ∧ (¬q ∨ ¬r)

Conjunctive Normal Form (CNF) is a conjunction of clauses, each of which is a disjunction of literals:

(p ∨ ¬q ∨ r) ∧ (¬p ∨ s) ∧ (q ∨ s)

In this context, p or ¬p are called literals, and the expressions within parentheses are known as clauses.

Disjunctive Normal Form (DNF) is a disjunction of terms, each of which is a conjunction of literals:

(p ∧ q) ∨ (¬p ∧ r)

CNF is well-suited for input to many SAT solvers; DNF can intuitively list several scenarios under which a formula evaluates to true. However, these forms are structural representations and do not guarantee that the expressions are necessarily short.

Direct Distribution Can Grow Exponentially

Converting:

(a1 ∧ b1) ∨ (a2 ∧ b2) ∨ ...

mechanically to CNF can result in an exponential increase in the number of clauses. In practice, SAT encodings often use Tseitin transformation: introduce auxiliary variables for subformulas and add constraints that express their relationships.

For example, for:

x ↔ (p ∧ q)

we add the following CNF constraints:

(¬x ∨ p) ∧ (¬x ∨ q) ∧ (x ∨ ¬p ∨ ¬q)

Use x to represent this subformula in higher-level combinations. For fixed-arity connectives, each syntax node adds only a constant number of clauses, so encoding size grows linearly with the original formula. Also assert that the root variable representing the whole formula is true; definitions alone do not require the original formula to hold.

If the original formula is p ∧ q, add the unit clause (x) to the three clauses above. Without it, p=F, q=F, x=F satisfies the definitions even though the original formula is false. For each assignment to the original variables, a correct encoding has a satisfying auxiliary extension exactly when the original formula holds.

Tseitin transformations typically emphasize that the resulting formula is equivalent in satisfiability to the original: the original formula has a solution if and only if the extended formula with auxiliary variables does. After introducing auxiliary variables, it is not valid to claim that the two formulas are fully equivalent in terms of variable assignments without explicit justification.

Encode Product Configuration as Clauses

Definition:

d: Enable database
c: Enable cache
a: Enable auditing
o: Enable offline mode

Rules:

1. Cache requires a database;
2. Enabling the database must include auditing;
3. Offline mode cannot use the database;
4. At least one of cache or offline mode must be enabled.

Translation:

c → d          ≡ ¬c ∨ d
d → a          ≡ ¬d ∨ a
o → ¬d         ≡ ¬o ∨ ¬d
c ∨ o

The combined form is already in CNF:

(¬c ∨ d) ∧ (¬d ∨ a) ∧ (¬o ∨ ¬d) ∧ (c ∨ o)

A satisfying assignment is:

o=T, d=F, c=F, a=F

Another valid assignment is:

c=T, d=T, a=T, o=F

Finding a model proves that some configuration satisfies the encoded constraints. It does not verify that the rules match the product’s actual intent. Encoding errors can still yield highly efficient but incorrect answers.

Enumerate this four-variable example using the Python 3 standard library, with tuple order (d, c, a, o):

from itertools import product

def valid(d, c, a, o):
    return ((not c or d) and (not d or a)
            and (not o or not d) and (c or o))

models = [bits for bits in product([False, True], repeat=4) if valid(*bits)]
print(len(models))
print(models)
# 3
# [(False, False, False, True), (False, False, True, True),
#  (True, True, True, False)]

There are three models. The first two differ only in auditing while offline, which no rule forbids. If that is unintended, add the missing requirement; the solver has followed the rules it received. This is finite enumeration, not an implementation of DPLL or CDCL.

From Exhaustive Search to DPLL/CDCL

A truth table with n variables has 2^n rows. Direct enumeration is suitable for teaching and small formulas but cannot scale to large constraint sets.

The core idea behind modern SAT solvers can be understood in layers:

1. Select an unassigned variable to make a decision;
2. Use unit propagation to derive forced assignments;
3. If a conflict arises, backtrack and try an alternative choice;
4. CDCL solvers learn new clauses from conflicts and jump back to the relevant decision level;
5. Restart strategies and heuristics continue to guide the search.

For example, clause (p) has only one unassigned literal, so p must be true; subsequently, (¬p ∨ q) forces q to be true. This propagation rapidly shrinks the search space without enumerating all possible assignments.

SAT is NP-complete: a candidate assignment can be checked in polynomial time, and every problem in NP reduces to SAT in polynomial time. This does not prove that every algorithm requires exponential time. A polynomial-time SAT algorithm would imply P=NP. Worst-case difficulty is compatible with efficient solving of many structured industrial instances.

UNSAT Also Needs Explanation

When a formula is unsatisfiable, engineers most care about which specific rules are in conflict. Solvers or higher-level tools can return an unsat core, a set of constraints that together are sufficient to cause unsatisfiability.

Rule A: c → d
Rule B: c
Rule C: ¬d

These three cannot all be true at the same time. By giving stable, meaningful names to these constraints, the unsat core can be mapped back to the original requirements documentation:

cache_requires_database
cache_is_mandatory
database_is_forbidden

This is far more actionable than simply reporting "the formula is unsatisfiable." Note that an unsat core does not necessarily represent the smallest possible conflicting set, that depends on the solver and its guarantees.

An inclusion-minimal core becomes satisfiable when any member is removed; a minimum-cardinality core has the fewest members. The former need not be the latter. Timeout or unknown is not UNSAT. Check a SAT model against the original constraints; independent UNSAT verification requires suitable proof output and checking support. See the authors’ Programming Z3 for model, core, and proof interfaces.

The Boundary Between SAT, SMT, and Constraint Solving

SAT variables take Boolean values. When rules involve integers, arrays, bit vectors, strings, or linear real numbers, an SMT solver can be used to extend beyond Boolean logic and incorporate the relevant theories.

replicas >= 3
replicas <= available_nodes
region != backup_region

Avoid manually encoding all numerical values into large Boolean bit vectors using SAT unless you fully understand the encoding complexity and the resulting semantics. When selecting tools, first evaluate the domain-specific constraints.

Completion Check

Write at least six rules for a three-node deployment: one master node, at least one replica, fault domain restriction, maintenance mode restriction. Then:

1. Convert them into CNF (Conjunctive Normal Form);
2. Find two valid assignments that satisfy the rules;
3. Add one rule that makes the system unsatisfiable;
4. Identify a conflict core;
5. Explain which constraints involving quantities are better suited to SMT (Satisfiability Modulo Theories) rather than pure SAT.

References

• SAT Competition
• SMT-LIB Standard