Purpose. These notes are my own write-up of the lecture material from TU/e’s MSc course 2IMF25 — Automated Reasoning. I adapted the technical content into a blog-friendly format while preserving the formal detail, examples, and connections to my broader research work. All images were recreated based on my understanding of the use cases.
1. What the course covers (at a glance)
The TU/e listing for 2IMF25 highlights resolution-based SAT, SMT, unification and first-order resolution, Binary Decision Diagrams (BDDs), and their application to CTL-based symbolic model checking, with learning outcomes that include building ROBDDs and applying tools to planning, verification, and deadlock detection.
2. Propositional logic, CNF, and resolution
2.1 Syntax and CNF via Tseitin
Let formulas be built from variables $x_i$, connectives $\neg,\land,\lor,\rightarrow$, and parentheses. A clause is a disjunction of literals; CNF is a conjunction of clauses. Direct CNF expansion can blow up; Tseitin transformation introduces fresh variables to ensure linear growth.
Example (Tseitin). Convert $\varphi \equiv (x \land y) \lor (\neg x \land z)$ to CNF.
Introduce $a \leftrightarrow (x \land y)$ and $b \leftrightarrow (\neg x \land z)$, and $t \leftrightarrow (a \lor b)$. Encode each equivalence with implications:
- $a \rightarrow x$, $a \rightarrow y$, $(x \land y) \rightarrow a$ becomes $(\neg a \lor x)\land(\neg a \lor y)\land(\neg x \lor \neg y \lor a)$.
- $b \rightarrow \neg x$, $b \rightarrow z$, $(\neg x \land z) \rightarrow b$ becomes $(\neg b \lor \neg x)\land(\neg b \lor z)\land(x \lor \neg z \lor b)$.
- $t \leftrightarrow (a \lor b)$ becomes $(\neg t \lor a \lor b)\land(\neg a \lor t)\land(\neg b \lor t)$.
Then assert $t$ as the top-level variable. The result is equisatisfiable with $\varphi$.
2.2 Resolution rule and refutation
A clause set $S$ is unsat iff the empty clause $\Box$ is derivable by resolution: from $(C \lor p)$ and $(D \lor \neg p)$ infer $(C \lor D)$.
Example (refutation). $S={(x),( \neg x \lor y),(\neg y)}$. Resolve $(x)$ with $(\neg x \lor y)$ to get $(y)$; resolve $(y)$ with $(\neg y)$ to get $\Box$.
Resolution is the foundational proof rule for SAT and first-order logic (with lifting).
3. SAT solving: from DP to CDCL
3.1 DP, DPLL, and modern practice
- DP (1960) eliminates variables by resolution (exponential in worst case but seminal).
- DPLL (1962) adds backtracking search with unit propagation and pure-literal elimination.
- CDCL (1990s) augments DPLL with conflict analysis and non-chronological backtracking.
Key historical references: Davis–Putnam (1960), Davis–Logemann–Loveland (1962), and CDCL frameworks such as GRASP (Marques-Silva & Sakallah, 1999).
3.2 Worked CDCL-style trace (toy)
Let $F$ be ${(x \lor y),( \neg x \lor z),(\neg y \lor z),(\neg z)}$.
1) Decide $x=\text{true}$. Unit-prop: from $(\neg x \lor z)$ derive $z$; conflict with $(\neg z)$.
2) Analyze conflict: learn $(\neg x)$; backjump.
3) Assign $x=\text{false}$. Unit-prop: $(x \lor y)$ gives $y$, and $(\neg y \lor z)$ gives $z$; conflict with $(\neg z)$.
4) Learn $(\neg y)$; propagate to conflict with $(x \lor y)$. UNSAT.
This tiny run illustrates clause learning and non-chronological backtracking.
4. Binary Decision Diagrams (BDDs)
A Reduced Ordered BDD (ROBDD) is a canonical DAG representation of a Boolean function under a fixed variable order. Reduction merges isomorphic subgraphs and removes redundant tests. The canonical nature enables equivalence checking in $O(1)$ by pointer comparison; complexity depends critically on variable ordering.
Example (order sensitivity). For $f=(x \land y)\lor(\neg x \land z)$, order $x \prec y \prec z$ yields a small ROBDD; the order $y \prec z \prec x$ can expand considerably.
5. Symbolic model checking with BDDs (CTL)
Let a Kripke structure be $(S,R,L)$ with transition relation $R \subseteq S\times S$. For CTL, fixed-point calculations over sets of states are computed with BDDs. Example operators:
- $EX\ \phi$: pre-image ${s \mid \exists s’.\ R(s,s’) \land s’ \in [[ \phi ]]}$.
- $EG\ \phi$: greatest fixed point of $\lambda X.\ [[ \phi ]] \cap \text{Pre}(X)$.
- $AF\ \phi$: least fixed point of $\lambda X.\ [[ \phi ]] \cup \text{Pre}(X)$.
Example property. $AG(req \rightarrow AF\ grant)$ asserts every request is eventually granted. BDD-based fixpoint iteration computes the satisfying set symbolically, enabling verification of systems with up to $10^{20}$ states in classic results.
6. First-order logic, unification, and resolution
6.1 Unification
A most general unifier (mgu) for terms $s,t$ is a substitution $\theta$ such that $s\theta=t\theta$, and any other unifier $\sigma$ factors as $\sigma=\rho\circ\theta$. Martelli–Montanari give an efficient algorithm for computing an mgu.
Example. Unify $f(x,a)$ and $f(g(y),y)$.
- Decompose to equations ${x=g(y), a=y}$.
- Occurs-check passes.
- Solve $y=a$, then $x=g(a)$. So $\theta={x\mapsto g(a), y\mapsto a}$.
6.2 First-order resolution (lifting)
Propositional resolution lifts to clauses with variables by applying unifiers to complementary literals before resolving, yielding a refutation-complete calculus for first-order logic (with Skolemization).
7. SMT: Satisfiability Modulo Theories
SMT decides satisfiability of first-order formulas modulo background theories (e.g., linear arithmetic, uninterpreted functions, arrays, bit-vectors). Two pillars:
1) Nelson–Oppen combination for stably-infinite, signature-disjoint theories (equality sharing).
2) DPLL(T) architecture: a SAT engine drives a theory solver via propagation and conflict explanation.
Classic surveys and tutorials: Barrett–Tinelli (2018, Handbook of Model Checking) and De Moura–Bjørner (CACM 2011). Theoretical frameworks include DPLL(T) (Ganzinger, Nieuwenhuis, Oliveras, Tinelli).
7.1 Tiny DPLL(T) example (EUF + LRA)
Formula: $(x=y) \land (y=z) \land (x\neq z)$ in EUF is inconsistent. A DPLL(T) loop assigns propositional proxies, theory solver detects congruence closure $x=y=z$ contradicting $x\neq z$, returns a theory conflict clause that drives learning and backjumping.
With LRA: $(x<y)\land(y<x)$ is immediately inconsistent via simplex. Combined reasoning uses Nelson–Oppen (if signature-disjoint and stably-infinite) or integrated designs.
7.2 Tools
Z3 (Microsoft Research) and Yices (SRI) are standard SMT solvers used in assignments and research.
8. Term rewriting, confluence, and termination
Term Rewriting Systems (TRS) define directed equations $l \rightarrow r$. Properties of interest:
- Confluence: if $s \rightarrow^{\ast} s_1$ and $s \rightarrow^{\ast} s_2$, there exists $t$ with $s_1 \rightarrow^{\ast} t$ and $s_2 \rightarrow^{\ast} t$.
- Termination: no infinite rewrite chains. Proved via well-founded orders (e.g., recursive path order) or interpretations.
Knuth–Bendix completion orients equations to aim for a confluent, terminating rewrite system, using critical-pair analysis. Standard references: Knuth–Bendix (1970) and the textbook by Baader & Nipkow.
9. Applications: program safety and register allocation
9.1 Safety with nondeterministic branching
Consider a toy imperative fragment with nondeterministic choice if ? then S1 else S2. Encode path constraints to SAT/SMT:
- Path 1: $pc_1$ with constraints $C_1$ and assertion $A$.
- Path 2: $pc_2$ with constraints $C_2$ and assertion $A$.
Check $C_1 \land \neg A$ and $C_2 \land \neg A$ for satisfiability; any model is a counterexample. Assignments in the 2IMF25 practicals require letting the tool (not manual algebra) do this search.
9.2 Register allocation via graph coloring
Build an interference graph from live ranges; $k$ registers correspond to $k$-colorability. Classic Chaitin-style allocators use simplify/spill/coalesce; Briggs et al. introduced optimistic coloring and rematerialization to reduce spills.
Toy example. Interference graph is a 3-clique on ${a,b,c}$ plus a leaf $d$ that interferes only with $a$. For $k=3$, color $a,b,c$ with 3 colors; $d$ reuses the color of either $b$ or $c$. For $k=2$, the 3-clique forces a spill.
Canonical references: Chaitin (1981/82) and Briggs–Cooper–Torczon (1994).
10. Worked end-to-end example: from SAT to BDDs to CTL
We will check a liveness property in a tiny controller:
1) Propositional model. Encode next-state function for state bits $(s_1,s_0)$ and input $req$.
- If $req$ then move to GRANT in 2 steps; otherwise stay.
- Tseitin-transform and feed to SAT to sanity-check invariants (no dead states).
2) BDDs. Build ROBDDs for transition relation $R(s,s’)$ under order $s_1 \prec s_0 \prec req \prec s_1’ \prec s_0’$. Compute $EX\ \phi$ via pre-image: $\exists s’.\ R(s,s’) \land \phi(s’)$.
3) CTL. Evaluate $AG(req \rightarrow AF\ grant)$ as nested fixed points using BDD pre-images. If the set of initial states $\subseteq [[ AG(req \rightarrow AF\ grant) ]]$, the property holds.
This pipeline mirrors the course’s emphasis on connecting algorithms (resolution, ROBDDs) to verification tasks.
11. Study tips and cross-links
- Practice converting arbitrary formulas to CNF with Tseitin; prove equisatisfiability, not equivalence.
- Hand-run a small DPLL/CDCL trace; record learned clauses.
- Build ROBDDs for the same function under different orders to feel the blow-up vs. compactness.
- Write a tiny SMT-LIB file for linear arithmetic and arrays; run with Z3 and Yices; examine unsat cores.
References
- TU/e 2IMF25 Course Listing: scope, outcomes, topics (resolution, SMT, unification, BDDs, CTL).
- Robinson, J. A. “A Machine-Oriented Logic Based on the Resolution Principle,” JACM 12(1):23–41, 1965.
- Davis, M., Putnam, H. “A Computing Procedure for Quantification Theory,” JACM 7(3):201–215, 1960; Davis, M., Logemann, G., Loveland, D. “A Machine Program for Theorem-Proving,” CACM 5(7):394–397, 1962.
- Marques-Silva, J., Sakallah, K. “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE TC 48(5):506–521, 1999.
- Bryant, R. “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE TC 35(8):677–691, 1986; “Symbolic Boolean Manipulation with OBDDs,” ACM Comput. Surv. 1992.
- Clarke, E. M., Emerson, E. A. “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” 1981; Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., Hwang, L. J. “Symbolic Model Checking: $10^{20}$ States and Beyond,” 1990; Clarke, Grumberg, Peled, Model Checking, MIT Press, 1999.
- Barrett, C., Tinelli, C. “Satisfiability Modulo Theories,” in Handbook of Model Checking, 2018. Nelson, G., Oppen, D. “Simplification by Cooperating Decision Procedures,” TOPLAS, 1979. Ganzinger, H., Nieuwenhuis, R., Oliveras, A., Tinelli, C. “DPLL(T): Fast Decision Procedures,” CAV 2004.
- Z3 SMT Solver: de Moura, L., Bjørner, N. “Z3: An Efficient SMT Solver,” TACAS 2008. Yices SMT Solver: Dutertre, B., de Moura, L. “The Yices SMT Solver,” 2006; and “A Fast Linear-Arithmetic Solver for DPLL(T),” CAV 2006.
- Martelli, A., Montanari, U. “An Efficient Unification Algorithm,” TOPLAS 4(2):258–282, 1982.
- Knuth, D., Bendix, P. “Simple Word Problems in Universal Algebras,” 1970. Baader, F., Nipkow, T. Term Rewriting and All That, CUP, 1998.
- Chaitin, G. “Register Allocation and Spilling via Graph Coloring,” SIGPLAN 1982; Briggs, P., Cooper, K., Torczon, L. “Improvements to Graph Coloring Register Allocation,” TOPLAS 16(3):428–455, 1994.