Propositional Inference and Logical Agents

This builds on Logical Agents and 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.¹ 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): $\neg L_{1,1}\vee \neg Breeze\vee B_{1,1}$ becomes $(L_{1,1}\wedge 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.

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.

To see forward chaining run, trace it on the definite clauses $P\Rightarrow Q$, $L\wedge M\Rightarrow P$, $B\wedge L\Rightarrow M$, $A\wedge B\Rightarrow L$, with facts $A$ and $B$, querying $Q$. Initialize each clause's count to the number of premises: the $A\wedge B\Rightarrow L$ and $B\wedge L\Rightarrow M$ clauses start at 2, the $L\wedge M\Rightarrow P$ clause at 2, $P\Rightarrow Q$ at 1. The agenda begins as $[A,B]$.

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?.²

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.

To see the pruning at work, run DPLL on a small unsatisfiable set. Let the clauses be $\{A\vee B,\neg A\vee C,\neg B\vee C,\neg 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:

• $\neg C$ is a unit clause, forcing $C=false$.
• With $C$ false, $\neg A\vee C$ becomes the unit $\neg A$, forcing $A=false$; likewise $\neg B\vee C$ forces $B=false$.
• Now $A\vee B$ is $false\vee false$ — a falsified clause — so the branch fails, and since no choice was ever made, the whole set is unsatisfiable.

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

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.

Agents based on propositional logic

The lesson opened with a knowledge-based agent that Tells its percepts and Asks 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.³

The device is the fluent: a proposition whose truth varies with time, written with a time superscript. $L_{1,1}^t$ means "the agent is in $[1,1]$ at time $t$"; ${HaveArrow}^t$ means it still holds its arrow at time $t$; ${Forward}^t$ means it executes $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]$,

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]$.

Assert ${Forward}^0$ and the agent can prove $L_{2,1}^1$ — so far so good. But Ask the $KB$ whether ${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.⁴

One repair is a frame axiom for every fluent an action leaves alone — ${Forward}^t\Rightarrow ({HaveArrow}^t\iff {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:

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:

Location is more involved, because several actions and orientations can put the agent in a square. $L_{1,1}^{t+1}$ holds if the agent was already at $[1,1]$ and did not move off it (either the action was not $Forward$, or it walked into a wall and bumped), or it moved forward into $[1,1]$ from an adjacent square facing the right way:

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_{1,2}^6$ (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 ${OK}_{x,y}^t\iff \neg P_{x,y}\wedge \neg (W_{x,y}\wedge {WumpusAlive}^t)$, it proves ${OK}_{2,2}^6$ — 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 Asks 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).⁵

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 $\neg 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.

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 $\neg X^t$ for each symbol and keep whichever holds. This is a conservative approximation — it may forget a disjunction like $P_{3,1}\vee 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.⁶

The sentence conjoins three parts, all over symbols indexed up to a horizon $t$: the initial state ${Init}^0$; the successor-state axioms${Transition}^1,\dots ,{Transition}^t$ for every action at every step up to $t$; and the goal asserted at time $t$, for the wumpus ${HaveGold}^t\wedge {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.

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_{1,1}^0$ and the goal $L_{2,1}^1$ and it finds not only the honest plan $[{Forward}^0]$ but also the absurd $[{Shoot}^0]$ — by quietly assigning $L_{2,1}^0$ 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. $\neg L_{x,y}^0$ 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 ${Shoot}^t\Rightarrow {HaveArrow}^t$ rules that out.
• Action-exclusion axioms. Without them a model can set ${Forward}^0$ and ${Shoot}^0$ both true. For each interfering pair $A_i^t,A_j^t$ add $\neg A_i^t\vee \neg A_j^t$; 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.

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.