--- title: Propositional Inference and Logical Agents module: Logic and Planning moduleNumber: 3 lessonNumber: 2 order: 302 summary: > Model checking and resolution decide entailment, but both can blow up. This part turns propositional logic into a practical engine and a working agent. Horn clauses give linear-time forward and backward chaining — the basis of logic programming. DPLL and WalkSAT make satisfiability testing fast in the common case. Then we make the agent situated: time-indexed fluents, the frame problem and its solution by successor-state axioms, a hybrid agent that deduces a safe map and plans a route through it, and SATPlan, which finds a plan by asking a SAT solver for a satisfying model. topics: [Logic] sources: - book: AIMA ref: "§7.5 Propositional Theorem Proving (Horn clauses and chaining)" - book: AIMA ref: "§7.6 Effective Propositional Model Checking; §7.7 Agents Based on Propositional Logic" --- This builds on [Logical Agents and Propositional Logic](/artificial-intelligence/logic-and-planning/propositional-logic), which set up the knowledge base, the entailment relation $KB \models \alpha$, and two complete but potentially exponential ways to decide it — truth-table enumeration and resolution. Here we make inference fast where we can, and give the agent a way to reason across time. ## Horn clauses and chaining Completeness is often unneeded. Many real knowledge bases restrict the _form_ of their sentences, which allows a faster, still-sound inference method.[^aima-horn] A **definite clause** is a disjunction of literals with _exactly one_ positive literal; a **Horn clause** relaxes this to _at most one_ positive literal. Every definite clause is a Horn clause. The restriction matters for three reasons. First, a definite clause reads naturally as an implication whose premise is a conjunction of positive literals (the **body**) and whose conclusion is a single positive literal (the **head**): $\lnot L_{1,1} \lor \lnot Breeze \lor B_{1,1}$ becomes $(L_{1,1} \land Breeze) \Rightarrow B_{1,1}$. A clause with a single positive literal, like $L_{1,1}$, is a **fact**. Second, inference with Horn clauses runs through the **forward-chaining** and **backward-chaining** algorithms, whose steps are natural enough for a human to follow — the basis of logic programming. Third, deciding entailment with Horn clauses takes time _linear_ in the size of the knowledge base. **Forward chaining** is data-driven. It starts from the known facts and fires any implication whose entire body is known, adding the head to the known set, until the query appears or nothing more can fire. `PL-FC-Entails?` runs this in linear time by keeping, for each clause, a `count` of premises not yet satisfied; each time a symbol is confirmed, it decrements the counts of the clauses that mention it, and fires a clause the moment its count hits zero. ```algorithm caption: $\textsc{PL-FC-Entails?}$ — forward chaining over definite clauses input: $KB$, definite clauses; $q$, a query symbol $count \gets$ a table of the premise-count of each clause $inferred \gets$ a table, $false$ for every symbol $agenda \gets$ a queue of the symbols known true in $KB$ while $agenda$ is not empty do $p \gets \textsc{Pop}(agenda)$ if $p = q$ then return $true$ if $inferred[p] = false$ then $inferred[p] \gets true$ for each clause $c$ in $KB$ with $p$ in its premise do decrement $count[c]$ if $count[c] = 0$ then add the conclusion of $c$ to $agenda$ return $false$ ``` Forward chaining is sound (every step is a Modus Ponens) and complete for definite clauses: at the fixed point where nothing more fires, the `inferred` table is a model of $KB$, so every entailed atom has already been derived. The dual algorithm, **backward chaining**, is goal-driven: to prove $q$, find the implications whose head is $q$ and try to prove their bodies, recursing until it bottoms out at known facts. It touches only propositions relevant to the query, so it is often far cheaper than linear. Both algorithms have a clean reading as search over an **AND–OR graph**. Multiple links joined by an arc form a conjunction — _all_ of them must be proved — while links without an arc form a disjunction — _any_ one suffices. Forward chaining sets the known leaves and propagates upward, waiting at each conjunction until all its inputs are known; backward chaining walks the same graph downward from the goal. $$ % caption: The AND-OR graph for the clauses $P \Rightarrow Q$, $L \land M % \Rightarrow P$, $B \land L \Rightarrow M$, $A \land B \Rightarrow L$, plus facts % $A$ and $B$. A small arc crossing two incoming links marks a conjunction: both % must be proved. Forward chaining sets the known leaves $A, B$ and propagates % upward to prove $Q$. \begin{tikzpicture}[>=stealth, font=\footnotesize, n/.style={circle, draw, minimum size=7mm, inner sep=0pt}] \definecolor{acc}{HTML}{2348F2} \node[n, draw=acc, text=acc] (Q) at (0,4.4) {Q}; \node[n] (P) at (0,3.2) {P}; \node[n] (L) at (-1.5,1.9) {L}; \node[n] (M) at (1.5,1.9) {M}; \node[n] (A) at (-1.5,0) {A}; \node[n] (B) at (1.5,0) {B}; % P => Q (single link, no conjunction) \draw[->] (P) -- (Q); % L and M => P (conjunction arc across the two links entering P) \draw[->] (L) -- (P); \draw[->] (M) -- (P); \draw[acc, thick] ($(P)+(-0.55,-0.45)$) arc[start angle=210, end angle=330, radius=0.64]; % B and L => M (conjunction into M) \draw[->] (B) -- (M); \draw[->] (L) -- (M); \draw[acc, thick] ($(M)+(-0.58,-0.42)$) arc[start angle=205, end angle=320, radius=0.64]; % A and B => L (conjunction into L) \draw[->] (A) -- (L); \draw[->] (B) to[out=140, in=-20] (L); \draw[acc, thick] ($(L)+(-0.42,-0.55)$) arc[start angle=230, end angle=310, radius=0.62]; % label the known facts \node[font=\scriptsize, acc, anchor=north] at (0,-0.45) {known facts}; \end{tikzpicture} $$ To see forward chaining run, trace it on the definite clauses $P \Rightarrow Q$, $L \land M \Rightarrow P$, $B \land L \Rightarrow M$, $A \land B \Rightarrow L$, with facts $A$ and $B$, querying $Q$. Initialize each clause's `count` to the number of premises: the $A \land B \Rightarrow L$ and $B \land L \Rightarrow M$ clauses start at 2, the $L \land M \Rightarrow P$ clause at 2, $P \Rightarrow Q$ at 1. The agenda begins as $[A, B]$. $$ % caption: A forward-chaining count trace for the AND-OR clauses. Each row shows a % symbol popped from the agenda and the clause counts it decrements; a clause fires % (adds its head) when its count reaches zero. The query $Q$ is derived on the last % firing. \begin{tikzpicture}[>=stealth, font=\footnotesize, hd/.style={font=\scriptsize\bfseries, text=black}, cel/.style={font=\scriptsize, anchor=west}] \definecolor{acc}{HTML}{2348F2} % header \node[hd, anchor=west] at (0,3.2) {pop}; \node[hd, anchor=west] at (1.4,3.2) {counts after decrement}; \node[hd, anchor=west] at (6.6,3.2) {f\/ires}; \draw[black] (-0.1,3.0) -- (8.6,3.0); \node[cel] at (0,2.5) {A}; \node[cel] at (1.4,2.5) {L: 2 to 1}; \node[cel, acc] at (6.6,2.5) {none}; \node[cel] at (0,1.9) {B}; \node[cel] at (1.4,1.9) {L: 1 to 0, M: 2 to 1}; \node[cel, acc] at (6.6,1.9) {L}; \node[cel] at (0,1.3) {L}; \node[cel] at (1.4,1.3) {M: 1 to 0, P: 2 to 1}; \node[cel, acc] at (6.6,1.3) {M}; \node[cel] at (0,0.7) {M}; \node[cel] at (1.4,0.7) {P: 1 to 0}; \node[cel, acc] at (6.6,0.7) {P}; \node[cel] at (0,0.1) {P}; \node[cel] at (1.4,0.1) {Q: 1 to 0}; \node[cel, acc] at (6.6,0.1) {Q}; \draw[black] (-0.1,-0.2) -- (8.6,-0.2); \node[cel, acc] at (0,-0.7) {Q popped: query proved}; \end{tikzpicture} $$ Each fact confirmed decrements the counts of the clauses that mention it; a clause fires the instant its count hits zero, and its head joins the agenda. The whole run touches each clause a constant number of times, which is what makes it linear. ## Effective model checking Resolution and chaining prove entailment. But since entailment reduces to _unsatisfiability_, and unsatisfiability is a SAT question, the fastest general propositional reasoners are SAT solvers: algorithms that decide whether a set of clauses has a satisfying model. Two families dominate, and both improve on the brute enumeration of `TT-Entails?`.[^aima-sat] ### DPLL The **Davis–Putnam–Logemann–Loveland** algorithm — DPLL — takes a CNF sentence and does a recursive, depth-first search over models, exactly like `TT-Entails?`, but with three improvements that prune vast subtrees. - **Early termination.** A clause is already true if any one of its literals is true, and the whole sentence already false if any clause is false — either can be detected before the model is complete, letting the search abandon a subtree early. - **Pure symbols.** A symbol that appears with the same sign in every remaining clause is _pure_; assigning it to satisfy those clauses can never hurt, so DPLL fixes pure symbols without branching. - **Unit clauses.** A clause with a single unassigned literal (the rest already false) forces that literal's value. Assigning it can turn another clause into a unit clause, and so on — a cascade called **unit propagation**, which reduces to forward chaining when the clauses are definite. ```algorithm caption: $\textsc{DPLL}$ — decide satisfiability of a CNF sentence input: $clauses$, a set of clauses; $symbols$, its unassigned symbols; $model$ if every clause in $clauses$ is true in $model$ then return $true$ if some clause in $clauses$ is false in $model$ then return $false$ $P, value \gets \textsc{Find-Pure-Symbol}(symbols, clauses, model)$ if $P$ is non-null then return $\textsc{DPLL}(clauses, symbols - P, model \cup \{P = value\})$ $P, value \gets \textsc{Find-Unit-Clause}(clauses, model)$ if $P$ is non-null then return $\textsc{DPLL}(clauses, symbols - P, model \cup \{P = value\})$ $P \gets \textsc{First}(symbols)$; $rest \gets \textsc{Rest}(symbols)$ return $\textsc{DPLL}(clauses, rest, model \cup \{P = true\})$ or $\textsc{DPLL}(clauses, rest, model \cup \{P = false\})$ ``` To see the pruning at work, run DPLL on a small unsatisfiable set. Let the clauses be $\{A \lor B,\; \lnot A \lor C,\; \lnot B \lor C,\; \lnot C\}$ over symbols $A, B, C$. Brute enumeration would test up to $2^3 = 8$ models; DPLL closes the case with no branching at all: - $\lnot C$ is a **unit clause**, forcing $C = \mathit{false}$. - With $C$ false, $\lnot A \lor C$ becomes the unit $\lnot A$, forcing $A = \mathit{false}$; likewise $\lnot B \lor C$ forces $B = \mathit{false}$. - Now $A \lor B$ is $\mathit{false} \lor \mathit{false}$ — a **falsified clause** — so the branch fails, and since no choice was ever made, the whole set is unsatisfiable. $$ % caption: Unit propagation on $\{A \lor B,\ \lnot A \lor C,\ \lnot B \lor C,\ % \lnot C\}$. The unit $\lnot C$ forces $C$ false, which turns two clauses into new % units forcing $A$ and $B$ false, which falsifies $A \lor B$. DPLL reports % unsatisfiable without branching. Each arrow is a forced assignment. \begin{tikzpicture}[>=stealth, font=\footnotesize, as/.style={draw, minimum width=17mm, minimum height=7mm, font=\scriptsize, align=center}, bad/.style={draw=red, text=red, thick, minimum width=17mm, minimum height=7mm, font=\scriptsize, align=center}] \definecolor{acc}{HTML}{2348F2} \definecolor{red}{HTML}{C0392B} \node[as, draw=acc, text=acc] (c) at (0,2.4) {C = false}; \node[as] (a) at (-2.4,0.8) {A = false}; \node[as] (b) at (2.4,0.8) {B = false}; \node[bad] (x) at (0,-0.9) {A or B now false}; \draw[->, acc, thick] (c) -- (a) node[midway, above, sloped, font=\scriptsize, text=black] {unit not A}; \draw[->, acc, thick] (c) -- (b) node[midway, above, sloped, font=\scriptsize, text=black] {unit not B}; \draw[->, thick] (a) -- (x); \draw[->, thick] (b) -- (x); \node[font=\scriptsize, text=black, anchor=west] at (1.4,2.4) {from unit not C}; \node[font=\scriptsize, text=red, anchor=north] at (0,-1.55) {UNSAT, no branching}; \end{tikzpicture} $$ Real solvers layer more tricks on this skeleton — component analysis, degree-based variable ordering, conflict-clause learning with intelligent backtracking, random restarts, and fast dynamic indexing of clauses. With them, modern DPLL descendants decide sentences with tens of millions of variables, and have made hardware and protocol verification routine where hand-guided proofs once ruled. ### WalkSAT and local search The second family abandons systematic search for **local search** over complete assignments. Start with a random model and repeatedly flip the truth value of one symbol, guided by an evaluation function that counts unsatisfied clauses. **WalkSAT** is the canonical example: on each step it picks an unsatisfied clause, then either flips the symbol in it that minimizes total unsatisfied clauses (a greedy "min-conflicts" move) or, with probability $p$, flips a random symbol in it (a "random walk" move to escape local minima). ```algorithm caption: $\textsc{WalkSAT}$ — local search for a satisfying model input: $clauses$; $p$, walk probability; $max\text{-}flips$, the flip budget $model \gets$ a random assignment of $true$/$false$ to the symbols for $i = 1$ to $max\text{-}flips$ do if $model$ satisfies $clauses$ then return $model$ $clause \gets$ a randomly chosen clause that is false in $model$ with probability $p$ do flip a randomly chosen symbol from $clause$ else flip the symbol in $clause$ that maximizes satisfied clauses return failure ``` The trade is fundamental. When WalkSAT returns a model, the sentence is definitely satisfiable; but when it returns failure, the cause is ambiguous — the sentence may be unsatisfiable, or the flip budget may simply have run out. Local search cannot _reliably_ prove unsatisfiability, which is what deciding entailment demands. So an agent can use WalkSAT to say "I couldn't find a world where this square is unsafe," a strong empirical hint, but never a proof. DPLL, being complete, gives the proof when one is needed. The hardest random SAT instances cluster near a **clause-to-symbol ratio** around $4.3$: far below it, problems are underconstrained and models are dense and easy to stumble onto; far above, they are overconstrained and quickly seen to have no model; right at the threshold, an instance is as likely satisfiable as not, and both DPLL and WalkSAT slow sharply. $$ % caption: The satisfiability phase transition for random 3-SAT. The fraction of % satisfiable instances (left curve) drops sharply from near 1 to near 0 as the % clause-to-symbol ratio $m/n$ crosses about $4.3$; median solver runtime (right % curve) peaks right at that crossover, where a random instance is as likely % satisfiable as not. \begin{tikzpicture}[>=stealth, font=\footnotesize] \definecolor{acc}{HTML}{2348F2} \definecolor{red}{HTML}{C0392B} % axes \draw[->, black] (0,0) -- (7.2,0) node[anchor=north west, font=\scriptsize, black] {ratio m/n}; \draw[->, black] (0,0) -- (0,3.2); \foreach \x/\lab in {0/0, 2.15/2, 4.3/4.3, 6.45/6} {\draw[black] (\x,-0.06) -- (\x,0.06); \node[font=\scriptsize, anchor=north, black] at (\x,-0.06) {\lab};} % threshold marker \draw[black, dashed] (4.3,0) -- (4.3,3.0); % P(satisfiable): high, sharp drop near 4.3, low \draw[acc, thick] (0.2,2.7) -- (3.0,2.6) .. controls (4.0,2.4) and (4.6,0.4) .. (5.6,0.25) -- (7.0,0.22); \node[acc, anchor=west, font=\scriptsize] at (0.3,2.9) {P(sat)}; % runtime: peaks at 4.3 \draw[red, thick] (0.2,0.3) .. controls (3.0,0.6) and (3.9,2.7) .. (4.3,2.85) .. controls (4.7,2.7) and (5.6,0.7) .. (7.0,0.35); \node[red, anchor=west, font=\scriptsize] at (5.0,2.2) {median runtime}; \node[font=\scriptsize, black, anchor=south] at (4.3,3.0) {threshold}; \end{tikzpicture} $$ ## Agents based on propositional logic The lesson opened with a knowledge-based agent that `Tell`s its percepts and `Ask`s for an action, and everything since has built the inference machinery that answers the `Ask`. What it has not yet built is a $KB$ rich enough for a _situated_ agent that acts over time. The wumpus sentences $R_1$ through $R_5$ describe a single snapshot. A real agent moves, and after it moves the sentence "the agent is in $[1,1]$" is no longer true. To reason across time we need proposition symbols that carry a time index, and axioms that say how the world changes.[^aima-agents] The device is the **fluent**: a proposition whose truth varies with time, written with a time superscript. $L^t_{1,1}$ means "the agent is in $[1,1]$ at time $t$"; $\mathit{HaveArrow}^t$ means it still holds its arrow at time $t$; $\mathit{Forward}^t$ means it executes $\mathit{Forward}$ at time $t$. Symbols for permanent facts — $P_{x,y}$ for a pit, $W_{x,y}$ for the wumpus — carry no superscript and are **atemporal**. The percept-to-property links now read at a particular time: for any $t$ and square $[x,y]$, $$ L^t_{x,y} \Rightarrow (\mathit{Breeze}^t \Leftrightarrow B_{x,y}), \qquad L^t_{x,y} \Rightarrow (\mathit{Stench}^t \Leftrightarrow S_{x,y}). $$ ### The frame problem The hard part is stating how fluents change. The obvious move is an **effect axiom**: if the agent is at $[1,1]$ facing east at time $0$ and goes forward, then at time $1$ it is at $[2,1]$ and no longer at $[1,1]$. $$ L^0_{1,1} \land \mathit{FacingEast}^0 \land \mathit{Forward}^0 \Rightarrow (L^1_{2,1} \land \lnot L^1_{1,1}). $$ Assert $\mathit{Forward}^0$ and the agent can prove $L^1_{2,1}$ — so far so good. But `Ask` the $KB$ whether $\mathit{HaveArrow}^1$ holds and it cannot prove it _either way_. The effect axiom said what the action changed; it said nothing about what stayed the same, so the arrow's status simply drops out of the deducible facts. This is the **frame problem**: an action leaves almost everything untouched, and stating all of it is the difficulty.[^aima-frame] One repair is a **frame axiom** for every fluent an action leaves alone — $\mathit{Forward}^t \Rightarrow (\mathit{HaveArrow}^t \Leftrightarrow \mathit{HaveArrow}^{t+1})$, and one like it for the wumpus's life, the gold's location, and so on. With $m$ actions and $n$ fluents this is $O(mn)$ axioms, most of them asserting that nothing happened — the **representational** frame problem. Real worlds have many fluents but each action changes only a small number $k$ of them (the world has **locality**), so the fix should cost $O(mk)$, not $O(mn)$. ### Successor-state axioms The fix is to stop writing axioms about actions and write one axiom per _fluent_ instead. A fluent $F$ is true at $t+1$ in exactly two cases: the action at $t$ made it true, or it was already true at $t$ and the action did not make it false. That schema is the **successor-state axiom**: $$ F^{t+1} \Leftrightarrow \mathit{ActionCausesF}^t \lor (F^t \land \lnot \mathit{ActionCausesNotF}^t). $$ > **Definition (Successor-state axiom).** For each fluent $F$, a biconditional > defining $F^{t+1}$ from the fluents at time $t$ and the actions at time $t$: $F$ > holds next iff an action just made it hold, or it held already and no action > undid it. One axiom per fluent captures both the change and the persistence, > dissolving the representational frame problem at $O(mk)$ size. The arrow is the simplest case. Nothing reloads it, so the "made true" branch is empty and the axiom is just persistence minus the one action that spends it: $$ \mathit{HaveArrow}^{t+1} \Leftrightarrow (\mathit{HaveArrow}^t \land \lnot \mathit{Shoot}^t). $$ Location is more involved, because several actions and orientations can put the agent in a square. $L^{t+1}_{1,1}$ holds if the agent was already at $[1,1]$ and did not move off it (either the action was not $\mathit{Forward}$, or it walked into a wall and bumped), or it moved forward into $[1,1]$ from an adjacent square facing the right way: $$ \begin{aligned} L^{t+1}_{1,1} \Leftrightarrow\; &(L^t_{1,1} \land (\lnot \mathit{Forward}^t \lor \mathit{Bump}^{t+1})) \\ &\lor\, (L^t_{1,2} \land (\mathit{South}^t \land \mathit{Forward}^t)) \\ &\lor\, (L^t_{2,1} \land (\mathit{West}^t \land \mathit{Forward}^t)). \end{aligned} $$ $$ % caption: A successor-state axiom as a two-branch timeline for one fluent F. F is % true at t+1 exactly when an action at t made it true (the CAUSE branch) or F held % at t and no action undid it (the PERSIST branch). One such axiom per fluent % replaces the $O(mn)$ frame axioms and dissolves the representational frame % problem. \begin{tikzpicture}[>=stealth, font=\footnotesize, st/.style={draw, minimum width=22mm, minimum height=8mm, align=center, font=\scriptsize}, br/.style={draw, minimum width=30mm, minimum height=9mm, align=center, font=\scriptsize}] \definecolor{acc}{HTML}{2348F2} % time t and t+1 markers \node[st, draw=black] (ft) at (0,0) {F at time t}; \node[st, draw=acc, text=acc, thick] (ft1) at (8.6,0) {F at time t+1}; % two branches \node[br] (cause) at (4.3,1.35) {action makes F true}; \node[br] (persist) at (4.3,-1.35) {F held and no action undid it}; \draw[->, acc, thick] (ft.north) to[out=60, in=180] (cause.west); \draw[->, acc, thick] (cause.east) to[out=0, in=120] (ft1.north); \draw[->, acc, thick] (ft.south) to[out=-60, in=180] (persist.west); \draw[->, acc, thick] (persist.east) to[out=0, in=-120] (ft1.south); \node[font=\scriptsize, text=black] at (4.3,0.35) {either branch suf\/f\/ices (OR)}; \end{tikzpicture} $$ Given a complete set of successor-state axioms plus the percept-property links, the agent can `Ask` any answerable question about the current state. Running the six percepts and actions from the opening story through the $KB$, the agent proves $L^6_{1,2}$ (it knows where it is), $W_{1,3}$ and $P_{3,1}$ (it has pinned the wumpus and a pit), and, with a safety axiom $\mathit{OK}^t_{x,y} \Leftrightarrow \lnot P_{x,y} \land \lnot(W_{x,y} \land \mathit{WumpusAlive}^t)$, it proves $\mathit{OK}^6_{2,2}$ — square $[2,2]$ is safe to enter. A sound and complete solver like DPLL answers each such query in milliseconds for small caves. ### A hybrid agent Deduction tells the agent what is _true_; it does not by itself tell the agent what to _do_. The **hybrid agent** couples the propositional $KB$ with the problem-solving search of the earlier modules: it `Ask`s the $KB$ which squares are safe, then plans a route through them with $A^\ast$. Its $KB$ starts with the atemporal "wumpus physics" and, each step, gains the new percept sentence and the $t$-indexed axioms (the successor-state axioms among them).[^aima-hybrid] ```algorithm caption: $\textsc{Hybrid-Wumpus-Agent}$ — deduce the safe map, plan a route through it input: $percept$, a list [stench, breeze, glitter, bump, scream] persistent: $KB$, initially the atemporal wumpus physics; $t \gets 0$; $plan$, empty $\textsc{Tell}(KB, \textsc{Make-Percept-Sentence}(percept, t))$ $\textsc{Tell}$ the $KB$ the temporal physics sentences for time $t$ $safe \gets \{[x,y] : \textsc{Ask}(KB, \mathit{OK}^t_{x,y}) = true\}$ if $\textsc{Ask}(KB, \mathit{Glitter}^t) = true$ then $plan \gets [\mathit{Grab}] + \textsc{Plan-Route}(current, \{[1,1]\}, safe) + [\mathit{Climb}]$ if $plan$ is empty then $unvisited \gets \{[x,y] : \textsc{Ask}(KB, L^{t'}_{x,y}) = false \text{ for all } t' \le t\}$ $plan \gets \textsc{Plan-Route}(current, unvisited \cap safe, safe)$ if $plan$ is empty and $\textsc{Ask}(KB, \mathit{HaveArrow}^t) = true$ then $possible \gets \{[x,y] : \textsc{Ask}(KB, \lnot W_{x,y}) = false\}$ $plan \gets \textsc{Plan-Shot}(current, possible, safe)$ if $plan$ is empty then $plan \gets \textsc{Plan-Route}(current, \{[1,1]\}, safe) + [\mathit{Climb}]$ $action \gets \textsc{Pop}(plan)$ $\textsc{Tell}(KB, \textsc{Make-Action-Sentence}(action, t))$ $t \gets t + 1$ return $action$ ``` The goals sit in a strict priority order: grab visible gold and head home; else route to the nearest unvisited safe square; else, if armed, plan a shot at a possible wumpus square (one where $\lnot W_{x,y}$ is _not_ provable); else take a calculated risk on a not-provably-unsafe square; else climb out. Each branch pairs a logical query — is this square safe, unvisited, possibly-wumpus — with an $A^\ast$ route through allowed squares. $$ % caption: The hybrid wumpus agent's cycle. The percept and the time-indexed axioms % are told to the KB; the agent asks which squares are safe, unvisited, or possibly % hold the wumpus; a route planner turns those answers into a plan; the popped % action is told back to the KB and executed. Logic decides what is true; search % decides what to do. \begin{tikzpicture}[>=stealth, font=\footnotesize, box/.style={draw, minimum width=24mm, minimum height=10mm, align=center, font=\scriptsize}, kb/.style={draw, thick, minimum width=26mm, minimum height=14mm, align=center}] \definecolor{acc}{HTML}{2348F2} \node[box] (perc) at (0,2.0) {percept}; \node[kb, draw=acc, text=acc] (kb) at (0,0) {knowledge\\base}; \node[box] (ask) at (4.6,0) {ask: safe,\\unvisited?}; \node[box] (plan) at (9.0,0) {plan route\\(A-star)}; \node[box] (act) at (9.0,2.0) {action}; \draw[->, acc, thick] (perc) -- (kb) node[midway, right, font=\scriptsize, black] {\texttt{Tell}}; \draw[->, acc, thick] (kb) -- (ask) node[midway, above, font=\scriptsize, black] {\texttt{Ask}}; \draw[->, thick] (ask) -- (plan); \draw[->, thick] (plan) -- (act); \draw[->, acc, thick] (act.north) to[out=90, in=90] node[above, font=\scriptsize, black] {\texttt{Tell} action} (perc.north); \end{tikzpicture} $$ One weakness stays hidden in the loop: the calls to `Ask` grow more expensive as $t$ climbs, because each inference reaches further back through more time-indexed symbols. An agent whose per-step cost grows with its lifetime is untenable. The fix is **logical state estimation** — cache a **belief state**, a single sentence over the current time step's symbols that stands in for the whole percept history, and update it in place each step. The exact belief state can need a formula of size exponential in the number of symbols, so a common approximation keeps it as a **1-CNF** conjunction of literals: prove $X^t$ and $\lnot X^t$ for each symbol and keep whichever holds. This is a **conservative approximation** — it may forget a disjunction like $P_{3,1} \lor P_{2,2}$ that names no single provable literal, so its set of possible worlds is an outer envelope around the true one, never a subset. ### SATPlan: planning as satisfiability The hybrid agent deduces safety with `Ask` but plans routes with $A^\ast$. It can plan by logic alone. Recall the refutation identity: entailment reduces to satisfiability. Planning has a dual reduction — a **plan exists iff a certain sentence is satisfiable**, and the satisfying model _is_ the plan. **SATPlan** builds that sentence and hands it to a SAT solver.[^aima-satplan] The sentence conjoins three parts, all over symbols indexed up to a horizon $t$: the **initial state** $\mathit{Init}^0$; the **successor-state axioms** $\mathit{Transition}^1, \dots, \mathit{Transition}^t$ for every action at every step up to $t$; and the **goal** asserted at time $t$, for the wumpus $\mathit{HaveGold}^t \land \mathit{ClimbedOut}^t$. A satisfying model assigns truth values to the action symbols across time; reading off the ones set true yields a sequence of actions that reaches the goal. Because the agent does not know the plan length in advance, SATPlan tries horizons $t = 0, 1, 2, \dots$ up to $T_{\max}$ and returns the first that succeeds, which is the shortest plan. ```algorithm caption: $\textsc{SATPlan}$ — find a plan by translating to SAT and solving input: $init$, $transition$, $goal$ — a problem description; $T_{\max}$, a horizon bound for $t = 0$ to $T_{\max}$ do $cnf \gets \textsc{Translate-To-SAT}(init, transition, goal, t)$ $model \gets \textsc{SAT-Solver}(cnf)$ if $model$ is not null then return $\textsc{Extract-Solution}(model)$ return failure ``` $$ % caption: SATPlan unrolls the problem to a fixed horizon t: the initial state, the % successor-state axioms for every step, and the goal asserted at time t are % conjoined into one CNF sentence. A SAT solver either returns a model, whose % true action symbols are read off as the plan, or reports unsatisfiable, and the % horizon is bumped. The first satisfiable horizon gives the shortest plan. \begin{tikzpicture}[>=stealth, font=\footnotesize, box/.style={draw, minimum width=24mm, minimum height=9mm, align=center, font=\scriptsize}, wide/.style={draw, minimum width=34mm, minimum height=9mm, align=center, font=\scriptsize}] \definecolor{acc}{HTML}{2348F2} \definecolor{red}{HTML}{C0392B} \node[box] (init) at (0,1.9) {init state (t=0)}; \node[box] (trans) at (0,0.6) {transition axioms}; \node[box] (goal) at (0,-0.7) {goal holds at t}; \node[wide, draw=acc, text=acc, thick] (cnf) at (4.6,0.6) {one CNF sentence}; \node[box] (sat) at (8.8,0.6) {SAT solver}; \node[box, draw=acc, text=acc] (plan) at (8.8,1.9) {true actions = plan}; \node[box, draw=red, text=red] (bump) at (8.8,-0.7) {UNSAT: bump t}; \foreach \a in {init, trans, goal} \draw[->, thick] (\a) -- (cnf); \draw[->, acc, thick] (cnf) -- (sat); \draw[->, acc, thick] (sat) -- (plan) node[midway, left, font=\scriptsize, black] {model}; \draw[->, red, thick] (sat) -- (bump); \end{tikzpicture} $$ The subtlety is that a $KB$ good enough for `Ask` is not good enough for SATPlan, and what separates them is the gap between entailment and satisfiability. `Ask` proves the goal only from what is _forced_; SATPlan is free to set any unforced symbol to whatever makes the goal true. Give it $L^0_{1,1}$ and the goal $L^1_{2,1}$ and it finds not only the honest plan $[\mathit{Forward}^0]$ but also the absurd $[\mathit{Shoot}^0]$ — by quietly assigning $L^0_{2,1}$ true, placing the agent in two squares at once, since nothing forbade it. Three families of extra axioms close these leaks: - **Location/state constraints.** Assert the agent is in exactly one square (and has one orientation) each step, e.g. $\lnot L^0_{x,y}$ for every $[x,y] \ne [1,1]$; the successor-state axioms then carry the constraint forward. - **Precondition axioms.** The successor-state axioms predict that an ill-preconditioned action does nothing, but do not forbid _selecting_ it — SATPlan will "shoot" with no arrow. Adding $\mathit{Shoot}^t \Rightarrow \mathit{HaveArrow}^t$ rules that out. - **Action-exclusion axioms.** Without them a model can set $\mathit{Forward}^0$ and $\mathit{Shoot}^0$ both true. For each interfering pair $A^t_i, A^t_j$ add $\lnot A^t_i \lor \lnot A^t_j$; imposing exclusion only on pairs that truly conflict leaves room for legitimate simultaneous actions, and since SATPlan finds the shortest legal plan it uses that room. With the initial state, successor-state axioms, precondition axioms, and action-exclusion axioms, every model of the sentence is a valid plan — no spurious solutions survive. A DPLL-style solver handles the 11-step wumpus plan without difficulty. That SATPlan surfaces missing constraints as bogus plans makes it a sharp _debugging_ tool for a knowledge base: each absurd solution names an axiom the $KB$ forgot to state. This closes the knowledge-based-agent loop the lesson opened — the same `Tell`/`Ask` interface now perceives across time, tracks a belief state, and selects actions, all by propositional inference. ## CDCL and the modern SAT revolution AIMA's DPLL is the 1962 skeleton. The solvers that made SAT an industrial tool descend from a single idea layered on top of it: **conflict-driven clause learning** (CDCL). When search hits a falsified clause, DPLL merely backtracks one level; a CDCL solver instead _analyzes_ the conflict, computes the assignment that caused it, and adds a new **learned clause** that forbids that assignment from ever recurring, then jumps back non-chronologically to the earliest decision that matters. The learned clauses accumulate into a memory of dead ends. Marques-Silva and Sakallah's GRASP (1996, IEEE Trans. Computers) introduced conflict analysis and non-chronological backtracking; Chaff (Moskewicz, Madigan, Zhao, Zhang, and Malik, DAC 2001) added the **two-watched-literals** scheme, which makes unit propagation cheap by watching only two literals per clause instead of scanning all of them, and the **VSIDS** decision heuristic, which biases branching toward variables that appear in recent conflicts. MiniSat (Eén and Sörensson, SAT 2003) distilled the whole design into a few thousand lines that became the template for a generation of solvers. $$ % caption: The DPLL-to-CDCL lineage. Each layer keeps the one below and adds a % pruning mechanism: unit propagation and branching from DPLL, then conflict % analysis with learned clauses and backjumping, then the engineering (watched % literals, VSIDS, restarts) that makes it fast at scale. \begin{tikzpicture}[>=stealth, font=\footnotesize, lay/.style={draw, minimum width=62mm, minimum height=8mm, align=center, font=\scriptsize}] \definecolor{acc}{HTML}{2348F2} \node[lay] (l1) at (0,0) {DPLL: unit propagation + branching (1962)}; \node[lay, draw=acc, text=acc, thick] (l2) at (0,-1.15) {+ con\/f\/lict analysis, learned clauses, backjumping}; \node[lay] (l3) at (0,-2.3) {+ two-watched-literals, VSIDS, restarts}; \node[lay] (l4) at (0,-3.45) {millions of variables, veri\/f\/ication at scale}; \foreach \a/\b in {l1/l2, l2/l3, l3/l4} \draw[->, acc, thick] (\a) -- (\b); \node[anchor=west, text=black, font=\scriptsize] at (3.4,-1.15) {GRASP 1996}; \node[anchor=west, text=black, font=\scriptsize] at (3.4,-2.3) {Cha\/f\/f 2001}; \end{tikzpicture} $$ Two threads extend the reach of SAT further. The annual **SAT Competition**, running since 2002, drives benchmark-measured progress and has repeatedly shown CDCL solvers dispatching structured industrial instances that random 3-SAT theory would call impossibly large. And **SMT** — satisfiability modulo theories — bolts a CDCL core to decision procedures for richer theories (linear arithmetic, bit-vectors, arrays, uninterpreted functions), so a solver can reason about "$x + y \le 4$ and $x > 2$" rather than opaque Boolean symbols. Barrett and Tinelli's survey (in the _Handbook of Model Checking_, 2018) and solvers like Z3 (de Moura and Bjørner, TACAS 2008) made SMT the engine behind program verifiers, symbolic-execution bug finders, and type checkers. The lesson's DPLL is where all of this starts: the propagate-branch loop is still the core, wrapped in decades of learning and engineering. [^aima-horn]: **AIMA**, §7.5.3 Horn and Definite Clauses; §7.5.4 Forward and Backward Chaining: definite versus Horn clauses, body and head, `PL-FC-Entails?` in linear time, the fixed-point completeness argument, backward chaining as goal-directed reasoning, and the AND–OR graph. [^aima-sat]: **AIMA**, §7.6 Effective Propositional Model Checking: DPLL with early termination, pure-symbol and unit-clause heuristics, unit propagation, the extra tricks in modern solvers, WalkSAT local search, and the satisfiability threshold near ratio $4.3$. [^aima-agents]: **AIMA**, §7.7 Agents Based on Propositional Logic; §7.7.1 The Current State of the World: time-indexed fluents, atemporal symbols, and the percept-property links $L^t_{x,y} \Rightarrow (\mathit{Breeze}^t \Leftrightarrow B_{x,y})$ that connect what is sensed at a time to permanent properties of squares. [^aima-frame]: **AIMA**, §7.7.1: effect axioms and the frame problem — an effect axiom fails to state what an action leaves unchanged, so a fluent's status can become unprovable; frame axioms fix it at $O(mn)$ (the representational frame problem), while locality means only $O(mk)$ should be needed. [^aima-hybrid]: **AIMA**, §7.7.2 A Hybrid Agent; §7.7.3 Logical State Estimation: `Hybrid-Wumpus-Agent` (Figure 7.20) pairing `Ask`ed safety queries with $A^\ast$ route planning under a priority of goals; belief states as sentences, the exponential blow-up of exact state estimation, and the 1-CNF conservative approximation (Figure 7.21). [^aima-satplan]: **AIMA**, §7.7.4 Making Plans by Propositional Inference: `SATPlan` (Figure 7.22), the init/transition/goal sentence unrolled to horizon $T_{\max}$, the entailment-versus-satisfiability gap that admits spurious plans, and the location, precondition, and action-exclusion axioms that make every model a valid plan.