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

The first assignment at the Math Observatory comes from the Configuration Hub: a set of interdependent switch constraints, so many that manual enumeration can no longer guarantee completeness.

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 ∨ operands 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 Assignment May Exponentially Blow Up

Assigning:

(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)

And use x to represent atomic subformulas in higher-level combinations. This results in a size that grows nearly linearly.

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

A SAT solver finds at least one valid configuration, proving only that some configuration satisfies the constraints, it does not verify that the rules align with the actual product intent. Encoding errors can still yield highly efficient but incorrect answers.

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 an NP-complete problem, and in the worst case it may still be difficult, yet mature solvers successfully solve many large, structured industrial instances. The complexity class indicates an upper bound on the difficulty of general problems, not that every instance will be slow.

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, this depends on the specific solver and its guarantees.

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