TLDR
The argument in five moves
- Conflicts are inevitable evidence. On an incomplete clause database, a systematic SAT solver will enter regions that cannot contain a model; the question is what it retains from the collision.
- Propagation has causes. Unit clauses imply assignments, and an implication graph records the earlier assignments and clauses responsible for each consequence.
- A cut becomes a clause. Tracing backwards from a conflict identifies a sufficient falsifying assignment; negating it yields a logically entailed conflict-induced clause.
- Diagnosis changes control. The learned clause can assert a necessary literal and send search to the highest relevant earlier decision level instead of retreating one level.
- Learning changes the future. Recorded clauses strengthen later propagation, prevent recurrence and turn the clause database into a history of proved mistakes: within explicit storage limits.
A clause database describes forbidden corners of a Boolean cube
GRASP works on propositional formulae in conjunctive normal form: an AND of clauses, each clause an OR of literals.
A Boolean variable takes 0 or 1. A literal is either a variable x or its complement ¬x. The literal x is true when x=1; ¬x is true when x=0. A clause is satisfied if at least one of its literals is true and falsified only when every literal is false. A CNF formula is satisfied when every clause is satisfied simultaneously.
A partial assignment leaves some variables free. Under it, a clause can already be satisfied, already be conflicting, or remain unresolved. An unresolved clause with exactly one free literal is unit. Because every other literal is false, the free literal must be made true in any extension that satisfies the formula. This forced assignment is an implication, not a heuristic guess.
Search begins from an empty or prescribed level-zero assignment. A decision procedure chooses a value for an unassigned variable. Deduction repeatedly follows unit clauses. If every clause is satisfied, a model has been found. If a clause becomes false, the current partial assignment is conflicting and some decisions must be undone.
The formula itself is a representation of a Boolean function, not the function's unique description. Equivalent CNFs can differ dramatically in deductive power. A formula containing every prime implicate would expose all consequences by propagation, but may require exponentially many clauses. Practical SAT search therefore alternates between choosing and deriving while selectively adding useful implicates.
Worked example 1 · one literal left
For (¬a ∨ b ∨ c), suppose a=1 and b=0. The first two literals are false, so c is the only route to satisfying the clause and propagation sets c=1. No branch is needed.
Causal probe 1 · release b
If b becomes unassigned, the clause has two free literals and no longer forces c. BCP depends on the present assignment, so the same clause alternates between constraint, implication and satisfied record as search changes state.
GRASP decomposes search into four engines
The architecture is not a single clever rule. It is a loop whose components exchange assignments, reasons, conflict information and a backtracking level.
Decide chooses an elective assignment when the current formula is unresolved. The paper's reported implementation uses a greedy clause-satisfaction heuristic, while the framework permits other decision policies. Decisions open new regions of the search space and create decision levels.
Deduce performs Boolean constraint propagation. It repeatedly consumes unit clauses, assigns their free literals and implicitly records antecedent clauses. Deduction stops at a fixed point or a falsified clause. A forced assignment inherits the current decision level, but its logical reason can include assignments from several earlier levels.
Diagnose is GRASP's distinguishing operation. When deduction reaches conflict, diagnosis traverses the implication structure, derives a conflict-induced clause and identifies where search should resume. Depending on the selected learning policy, the clause may be stored for future use.
Erase retracts assignments above the selected backtracking level while preserving level-zero facts and retained clauses. The new learned clause may become unit under the surviving assignment, immediately forcing a failure-driven assertion. Thus retreat is coupled to a derived next move.
This decomposition matters scientifically. Decision heuristics, propagation engines and diagnosis schemes can vary independently within the framework. A performance claim about GRASP is therefore a claim about a configured system; conflict analysis is central, but its effect depends on branching, clause management and the benchmark family.
Worked example 2 · a four-stage cycle
Decide a=1. Deduce b=1 and c=1 from unit clauses. Diagnose a conflict requiring ¬a. Erase all level-one consequences, retain the new unit clause (¬a), then deduce a=0 at level zero. The failure has changed both memory and control.
Causal probe 2 · replace Diagnose with chronological retreat
The solver remains a complete DPLL-style search if alternatives are explored, but it forgets the causal summary and may rebuild the same implication pattern under another sequence of irrelevant decisions.
Unit clauses turn decisions into causal chains
BCP is logically elementary and operationally decisive: one chosen literal can force a cascade whose recorded reasons later explain a contradiction.
Suppose a clause has literals (l₁∨…∨lₖ). Under the current assignment, if all but one are false, consistency requires the remaining free literal to be true. GRASP iterates this unit-clause rule until no unit remains. If every literal in a clause is false, that clause supplies a conflict vertex.
For an implied assignment x=v, the antecedent assignment consists of the other variable assignments that made its reason clause unit. A decision assignment has no antecedent. Edges from antecedents to the implication encode not temporal succession alone but a sufficient local explanation: given those predecessor values, the clause requires x=v.
Efficient propagation is critical because it runs after every decision and after assertions produced by conflicts. The 1999 article treats BCP as a forward reasoning engine tightly coupled to diagnosis. Later SAT solvers would refine the data structures, notably watched literals, but the semantic operation remains the repeated unit rule.
A causality graph can contain assignments from multiple decision levels. The most recent decision starts a wave, yet that wave interacts with facts inherited from earlier decisions. A conflict clause built from the graph can therefore identify which levels matter and which intervening decisions are spectators.
Worked example 3 · two implications collide
From (¬a∨b) and a=1, BCP obtains b=1. From (¬c∨d) and c=1, it obtains d=1. Clause (¬b∨¬d) is now false. The conflict depends on a and c through b and d, not on any unrelated variable assigned between them.
Causal probe 3 · delete one reason clause
Without (¬c∨d), c=1 no longer implies d=1 and the collision disappears. The implication graph is not a post-hoc story laid over a fixed outcome; changing a reason changes the reachable conflict.
Negate a sufficient cause and obtain a learned clause
Conflict analysis is a small proof construction. It derives a clause that the original formula entails, rather than inventing a prohibition because a path happened to be inconvenient.
A conflicting assignment is a conjunction of variable values sufficient to falsify a clause through the implication graph. If a∧c is sufficient for contradiction, then no satisfying assignment can contain both. By propositional equivalence, the formula entails ¬a∨¬c. This disjunction is the conflict-induced clause.
The initial conflict clause often mentions implied literals rather than decisions. Resolution replaces an implied literal with the antecedents that forced it. If d was implied by (¬c∨d), and a conflict clause contains ¬d, resolving the two clauses on d yields a clause containing ¬c instead. Repeated resolution moves the explanation backwards through the graph.
Different cuts through the implication graph yield different valid learned clauses. A cut separates the decision side from the conflict side; the assignments whose outgoing edges cross the cut form a sufficient cause. Closer cuts tend to mention more recent implications, while earlier cuts can express causes nearer the decisions. Clause size, assertion power and reuse can differ substantially.
The proof obligation is entailment. Each resolution step preserves logical consequence because both parent clauses are already implicates of the formula. The learned clause cannot remove a genuine model. It removes only assignments that would reproduce a proved contradiction.
Worked example 4 · eliminate the intermediates
Conflict (¬b∨¬d) is false under b=d=1. Resolve with b's reason (¬a∨b) to obtain (¬a∨¬d). Resolve with d's reason (¬c∨d) to obtain (¬a∨¬c). The final clause speaks directly about the two decisions that jointly caused failure.
Causal probe 4 · learn only the falsified input clause
Keeping (¬b∨¬d) adds nothing because it was already present. The explanatory gain comes from resolving through implication reasons to derive an implicate that was absent from the database.
A dominator compresses many paths into one assertion
When every route from the current decision to conflict passes through one implied assignment, that assignment is a unique implication point, or UIP.
Graphically, a UIP dominates the conflict relative to the current decision: no causal path reaches contradiction without crossing it. The decision itself is always a UIP, but later UIPs may summarise a large fan-out and reconvergence more compactly. Resolving until a chosen UIP is the only current-level literal in the learned clause produces an asserting clause.
An asserting learned clause has a crucial operational property. After backtracking to the highest decision level among its other literals, all those other literals are false, leaving the UIP literal as the only free one. BCP therefore assigns its satisfying value immediately. Diagnosis has supplied not only a prohibition but a necessary next consequence.
Modern CDCL presentations often foreground the first UIP, the one closest to conflict. GRASP's paper develops UIP-based schemes and relates them to dominators, but its historical design space should not be flattened into one later convention. Different diagnosis engines can choose different cuts, add different numbers of clauses and trade clause length against assertion and reuse.
The graph is doing two jobs. It is a proof trace for deriving an implicate and a control map for selecting the backjump. These roles align because the learned clause contains exactly the assignments that must not coexist. Its decision-level profile identifies which surviving assignment will make it unit.
Worked example 5 · assertion after a jump
Learn (¬a∨¬c) while a=1 at level 1, irrelevant x=1 at level 2, and c=1 at level 3. Jump to level 1. With a still true, the learned clause becomes unit and forces c=0. Level 2 is skipped because x appears in no cause.
Causal probe 5 · retain two current-level literals
After the same backjump, the learned clause may still have two free literals and force nothing. It remains valid memory, but the immediate failure-driven assertion is lost. The choice of cut changes control strength without changing soundness.
Retreat to the last relevant level, not the last visited level
Chronological backtracking treats time as relevance. GRASP uses the learned clause to distinguish recent decisions that caused the conflict from recent decisions that merely happened before it.
Ordinary depth-first SAT search encounters a conflict at decision level d and returns to d−1. It reverses or retries the most recent decision even if the implication graph contains no causal path from that decision to conflict. Several levels may be undone one by one before the search reaches a choice that matters.
Let a learned clause contain one literal whose variable was assigned at the current level and several literals assigned earlier. The backtracking level is the largest decision level among those earlier assignments. Levels above it can be erased together. At the target, the surviving earlier literals remain false and the learned clause makes its current-level literal unit.
In the example (¬a∨¬c), a belongs to level 1 and c to level 3; level-2 decision x is absent. The clause says every extension containing a=1 and c=1 is impossible, regardless of x. Backtracking to level 2 would preserve an irrelevant choice and then force c=0; jumping to level 1 removes that detour and still asserts c=0.
A backjump is justified by a proof, not by a guess that the intermediate region looks unpromising. The learned clause is entailed by the original formula and is false under the conflicting assignment. Any search state above the target that retains all its falsifying earlier literals cannot repair the conflict by changing omitted decisions.
Non-chronological retreat changes the geometry of traversal. The solver no longer walks a simple binary tree whose stack depth falls one edge at a time. It traverses a dynamically strengthened clause database, and a learned clause can connect remote levels. Completeness is preserved because only proved-impossible combinations are removed.
Worked example 6 · skip a spectator
Decide a=1 at level 1, x=1 at level 2 and c=1 at level 3. If the conflict graph proves (¬a∨¬c), x is irrelevant. GRASP backtracks to level 1 and propagates c=0. Chronological search would first revisit x despite having no evidence that x matters.
Causal probe 6 · insert ten irrelevant decisions
The chronological distance to the real cause grows by ten; the conflict clause and its backjump target do not change. This intervention exposes why explanation-based retreat can prune large stretches of the search stack.
A proved mistake becomes a reusable constraint
Learning is dynamic completion of the formula: the solver adds implicates precisely where search reveals that the current clause database was too weak to prevent a conflict.
Without recording, the conflict-induced clause can still support the immediate backjump and assertion. Storing it adds future deductive power. If another branch accumulates the same falsifying conditions, BCP encounters the learned clause before rebuilding the original implication subgraph. The solver recognises a family of equivalent mistakes.
The new clause does not alter the represented Boolean function. Because it is entailed by the original formula, conjoining it preserves exactly the same models. It changes the route to those models or to an unsatisfiability proof by making some consequences syntactically accessible to unit propagation.
Unlimited learning is not free. Every clause consumes memory, participates in propagation and may degrade locality. GRASP therefore treats clause addition as user-controlled, with policies based on clause size and relevance. The 1999 article discusses selective recording rather than assuming every derivable implicate deserves permanent residence.
This is another information-value problem following Paper 0080. Sabin and Freuder showed that more sound pruning can disturb a heuristic. GRASP shows how new sound clauses can eliminate repeated conflict, but the same systems caution applies: useful logical information may impose operational cost. Later CDCL solvers developed aggressive clause deletion, activity scoring and restart policies around this tension.
Learning also changes the meaning of the database. It begins as an input specification and becomes a joint product of specification plus proof history. Re-running with a different branch order can produce a different collection of learned clauses while deciding the same Boolean function.
Worked example 7 · a conflict returns under a new spectator
The first conflict occurs with a=1, x=0, c=1 and yields (¬a∨¬c). Later search reaches a=1, x=1, c unassigned. The learned clause immediately forces c=0; the irrelevant spectator has changed, but the causal pattern is blocked.
Causal probe 7 · delete the learned clause after the jump
The current branch remains repaired, yet a later branch may reconstruct the same failure. Comparing repeated implication work isolates the long-term value of recording from the immediate value of conflict analysis.
Learning prunes executions without pruning models
GRASP's speed techniques remain inside a proof discipline: returned assignments satisfy the input, learned clauses are implicates, and systematic search cannot lose the only model.
Correctness is direct at success: GRASP identifies a solution only when no clause is unsatisfied under a complete assignment. A separate checker can evaluate every original clause. Learned clauses cannot manufacture a false success because they add requirements rather than remove input clauses.
Soundness of pruning comes from resolution. Original clauses are implicates of the represented function; resolving two implicates yields another implicate. A conflict-induced clause derived along the implication graph is therefore true in every model of the original formula. Discarding assignments that falsify it discards no solution.
Completeness requires fair decisions and backtracking over remaining alternatives. Non-chronological jumps do not skip a possible model because the learned clause proves that the skipped region's relevant assignments are jointly impossible. At level zero, a conflict demonstrates unsatisfiability under all choices.
The paper also states a limiting connection between conflicts and formula completeness. If the clause database contained all prime implicates, unit propagation would expose necessary consequences early enough that search need not encounter the same kind of hidden conflict. Constructing that complete database may be exponentially expensive; dynamic learning is selective, demand-driven approximation.
Formal properties do not guarantee tractability. SAT is NP-complete, and some instances still require exponential resources. GRASP changes practical proof search by extracting structure from encountered conflicts. Its benchmark results demonstrate substantial gains on many tested instances and losses or limits on others, not a worst-case collapse.
Worked example 8 · exhaustive entailment check
For a formula over four variables, enumerate all sixteen total assignments. If every assignment satisfying the original clauses also satisfies learned clause L, then L is an implicate. This truth-table oracle is expensive at scale but ideal for auditing a small teaching laboratory.
Causal probe 8 · flip one sign in the learned clause
A model of the original formula may now falsify the altered clause. The exhaustive checker catches the unsound “learning”, showing why syntactic resemblance to a conflict explanation is insufficient without a valid derivation.
A founding architecture is not the whole modern CDCL solver
GRASP is rightly recognised as a root of conflict-driven clause learning, but later conventions and engineering advances should not be silently attributed to the 1999 system.
The article reports experiments on UCSC and DIMACS benchmarks and on instances drawn from electronic design automation, including automatic test-pattern generation. GRASP is compared with contemporary procedures and wins strongly on many, though not every, class. The authors explicitly retain negative cases and discuss parameter choices such as learned-clause limits.
The benchmark evidence is historical. Processor speed, memory hierarchy, encodings and baseline solvers have changed. Exact CPU times primarily establish the comparison among implementations and machines reported then. The enduring evidence lies in the mechanism's repeated adoption: implication-based conflict analysis, learned clauses, asserting consequences and non-chronological backtracking became central to modern SAT solving.
Modern CDCL usually adds engineering not exhausted by GRASP: watched-literal propagation, activity-based branching such as VSIDS, restarts, clause activity and deletion, phase selection, preprocessing and inprocessing. Some concepts were anticipated or compatible with the framework; that does not make every later standard feature a GRASP result.
The DOI in the supplied canon contains a catalogue error. The verified IEEE journal identifier is 10.1109/12.769433, not 10.1109/92.769433. The article appears in IEEE Transactions on Computers, volume 48, issue 5, pages 506–521, May 1999. An earlier 1996 University of Michigan technical report and ICCAD paper document the developing framework.
The fairest summary is architectural and bounded: GRASP integrated conflict diagnosis tightly with BCP, showed how the implication graph yields clauses and jumps, formalised correctness and completeness, and demonstrated strong practical results on its suite. It did not make SAT easy in the worst case or establish one timeless configuration.
Worked example 9 · separate idea from implementation
A solver using first-UIP learning, watched literals, VSIDS, rapid restarts and clause deletion is a modern CDCL system. Calling all five ingredients “the GRASP algorithm” erases later contributions. Calling its conflict-learning loop a descendant of GRASP preserves the lineage.
Causal probe 9 · disable only learning
Keep BCP, the same decision heuristic and chronological backtracking. Any performance difference now belongs to accumulated conflict memory and the jumps it enables, rather than to a different encoding or branching policy.
A mistake can become a rule without becoming an experience
GRASP is a clean model of functional learning: an agent-like process diagnoses why an action failed, changes memory and selects a non-local correction.
Reactive backtracking treats conflict as a binary signal: this branch failed, so try another. GRASP extracts a reusable counterfactual: these assignments cannot coexist in any solution. That abstraction transfers across incidental histories, which is a recognisable form of learning in an operational sense.
The implication graph provides credit assignment for failure. Rather than blaming the last action by default, the solver traces forced consequences to the decisions that jointly entailed contradiction. Non-chronological backtracking then aligns control with diagnosed responsibility. This is more structured than reward alone: the system produces a proof certificate for its revision.
Its memory is epistemically disciplined. A learned clause is not a statistical hunch and cannot be false in any model of the input. The solver grows an explicit theory of excluded combinations. Yet selective retention remains resource-bounded; an entailed fact can be operationally unhelpful if it is too large, too rare or too costly to propagate.
Nothing in this architecture establishes phenomenal consciousness. A conflict is a falsified clause, not frustration. Diagnosis is graph traversal and resolution, not introspective awareness. Memory is a clause database, not recollection with qualitative character. The language of causes and mistakes is exact enough at the computational level and unsupported at the experiential level.
The paper therefore helps separate three notions often conflated in AI discussion. Adaptation changes future behaviour. Explanation identifies a derivational cause. Consciousness concerns subjective presence. GRASP robustly exhibits the first two in formal, inspectable machinery; it supplies no evidence for the third.
Worked example 10 · proof-carrying correction
A planning agent rejects an action sequence because it violates a resource clause, derives a constraint over the two commitments responsible and skips three unrelated choices. The correction is intelligible because a resolution trace supports it; no claim about felt regret is needed.
Causal probe 10 · keep the jump but discard the proof
A heuristic jump might sometimes land at the same level, but its safety is no longer certified. GRASP's distinctive agency is not merely moving backwards quickly; it is coupling movement to an entailed explanation.
Evidence boundary
“Learns from conflict” means that resolution adds an entailed clause affecting later propagation. It does not imply autobiographical memory, selfhood, emotion or any subjective encounter with failure.
Resolve one conflict and audit the learned clause
Choose a scenario to watch decisions trigger BCP, trace implication reasons, derive an asserting clause and jump over irrelevant levels.
The first scenario uses decisions a=1 at level 1, x=1 at level 2 and c=1 at level 3. Clauses (¬a∨b) and (¬c∨d) imply b=d=1; (¬b∨¬d) conflicts. Resolving on d and b yields (¬a∨¬c), whose only level-3 literal is ¬c. Backjumping to level 1 skips x and makes the clause unit, so c=0 is asserted.
The second scenario lets a single decision fan into b and c, then d, then incompatible e assignments; diagnosis resolves the chain to unit clause ¬a and jumps to level zero. The third adds a longer two-decision implication chain to show that clause length follows the causal cut, not the number of graph vertices.
Three independent audits run for every scenario. A complete truth table verifies that each learned clause is entailed by its original CNF. A level-aware check verifies that the clause is unit after the stated backjump. A replay check verifies that the recorded cause falsifies the learned clause. These are exact small-model tests, not a performance reproduction of GRASP's historical benchmarks.
Worked example 11 · read the colours and the labels
Blue outlined nodes are decisions, gold nodes are implications and the red node is conflict. Edge labels name reason clauses. The redundant textual trail, learned clause and target make the proof readable without colour.
Causal probe 11 · select the root-unit case
Every conflict path ultimately depends on a alone. The learned clause shrinks from two literals to one, the backjump target becomes zero and BCP permanently fixes a=false for the remainder of search.
To rebuild GRASP, preserve reasons as carefully as values
A solver that propagates the right assignments but discards why they were implied cannot perform the same diagnosis.
Represent CNF clauses and a three-valued assignment: true, false or unassigned. Maintain a decision level for every assigned variable. When BCP assigns a literal, store the clause that made it unit; decisions carry no reason. If a clause becomes false, retain it as the initial conflict clause.
Conflict analysis repeatedly chooses a current-level literal in the working clause and resolves it with that variable's reason. Stop according to a documented cut policy: commonly when one current-level literal remains. Deduplicate literals, reject tautological resolvents and preserve a derivation trace for testing.
Compute the backjump level from the learned clause: among literals other than the sole current-level one, take the highest assignment level, or zero if none exists. Erase assignments above that level, add the learned clause under the retention policy and let BCP assert its remaining literal.
Test semantics independently of the solver's own messages. For small formulae, exhaustive truth tables check learned-clause entailment and solver answers. Replay reason clauses to validate every implication. Check that the learned clause is false before the jump and unit afterwards. A wrong sign or stale reason can silently make an apparently fast solver unsound.
Then measure performance with separate counters for decisions, propagations, conflicts, learned literals, backjumps, retained clauses and elapsed time. Compare on identical instances and retain losses. The insight is an architecture of explanation-driven search, not a licence to call any cache of failures “learning”.
Worked example 12 · one sign error
If b=1 was implied by (¬a∨b), its reason resolves a conflict literal ¬b to ¬a. Replacing ¬a with a reverses the excluded decision and may delete valid models. An exhaustive four-variable oracle catches the defect immediately.
Causal probe 12 · store assignments without reasons
BCP still reaches the conflict, but diagnosis cannot distinguish a decision cause from a forced intermediate. It can retreat chronologically or learn the entire decision trail, losing the graph's compression and precise jump.
What the evidence does and does not establish
| Claim | Evidence | Scope guard |
|---|---|---|
| Conflict analysis yields sound learned clauses. | Antecedent traversal and resolution derive implicates from original and previously entailed clauses. | Depends on correct reason bookkeeping and resolution; arbitrary conflict summaries are not sound. |
| Learned clauses enable non-chronological backtracking. | The clause's decision-level profile identifies irrelevant intervening levels and an asserting target. | The jump follows this derivation, not a guarantee that every jump is large. |
| Recording can prevent recurring conflicts. | The stored implicate becomes unit or conflicting before the old causal assignment is reconstructed. | Retention has propagation and memory costs; policies matter. |
| GRASP was effective on broad historical benchmarks. | UCSC, DIMACS and EDA comparisons reported in the article and technical report. | Historical implementations and hardware; not universal or directly modern timing evidence. |
| The architecture learns functionally. | Past conflict creates entailed memory that changes future inference and control. | No evidence of phenomenal consciousness or felt failure. |
Fidelity, teaching and implementation review
Review one: scholarship. The reconstruction preserves CNF semantics, partial-assignment outcomes, decision levels, unit propagation, antecedent assignments, the implication graph, Decide/Deduce/Diagnose/Erase, conflict-induced clauses, resolution, failure-driven assertions, conflict-directed backtracking, UIPs, clause recording, controlled learning, correctness, completeness, the prime-implicate limiting case and the reported breadth and limits of benchmark evidence. The supplied DOI error is corrected against IEEE, DBLP and institutional metadata.
Review two: teaching and execution. Ten paper-specific SVGs each have unique titles, descriptions, captions and source scopes; motion stops for reduced-motion preference. Twelve examples and twelve causal probes target the mechanism's load-bearing links. The laboratory offers three conflict structures rather than one decorative animation and checks logical entailment, post-jump assertion and cause exclusion independently.
Evidence and AI-telltale review. The account does not retroject watched literals, VSIDS, rapid restarts or modern clause deletion into GRASP. It distinguishes the 1996 technical report from the 1999 journal article, implementation timings from architectural inheritance, learned implicates from statistical generalisation and proof-directed backtracking from a psychological response to error.
Accessibility and responsive review. Colour is redundant with node labels and output panels; controls have visible labels; changing proof output uses a live region; graph descriptions are available to assistive technology; tables scroll at narrow widths; grids collapse at 900 and 600 pixels. The executable tests use a truth-table oracle rather than trusting the analyser's own claim.
Twelve cards for reconstruction
Failed search becomes future inference
Canon 0080 showed that inference and search cannot be priced independently: propagation changes the heuristic trajectory, sometimes for worse, while deeper maintenance can expose failure early enough to win. Canon 0081 turns that interaction into a learning loop. BCP produces a conflict; diagnosis converts the failed trajectory into a new clause; the new clause changes both propagation and the next retreat.
The contrast with Canon 0079 is equally sharp. Min-conflicts repairs a complete inconsistent assignment by reducing a local score. GRASP preserves a partial consistent assignment until propagation proves contradiction, then derives a symbolic explanation that applies beyond the current state. One learns a direction from violation counts; the other learns an implicate from proof.
Canon 0082, Moskewicz et al.'s Chaff (2001), will rebuild this conflict-driven architecture around engineering choices that make Boolean constraint propagation dramatically cheaper, including watched literals and the VSIDS branching heuristic. GRASP establishes what a learned conflict can mean; the next paper asks how to make that loop run at industrial scale.
The proof of failure is more valuable than the fact of failure
Chronological backtracking uses one bit of information: conflict occurred below the latest decision. GRASP recovers structure hidden in that bit by preserving the antecedent of every forced assignment. The resulting graph says which commitments mattered and how their consequences converged.
Resolution compresses a history into a transferable boundary. The learned clause may mention far fewer decisions than the branch contained, yet it applies to every future branch that repeats those causes. This is a precise form of abstraction: discard incidental sequence while retaining a logically sufficient exclusion.
The backjump then closes the explanation–action loop. The system does not merely store a post-mortem; it uses the clause's level structure to choose where to resume and what literal must follow. Memory, inference and control share one proof object.
But more memory is not automatically better. An exponential complete formula would make hidden conflicts disappear while overwhelming storage. Selective learning occupies the middle ground between total forgetting and total deduction. The best clause is judged by proof validity first and operational influence second.
GRASP therefore offers a durable model of bounded rational agency: make a choice, derive consequences, diagnose contradiction, retain a justified abstraction and revise at the relevant cause. Every stage is inspectable. That transparency explains considerable competence without closing the separate question of consciousness.
What this companion adds
This companion reconstructs GRASP from Boolean semantics through its four-engine search loop, implication graph, conflict-induced clauses, resolution cuts, UIPs, failure-driven assertions, non-chronological backtracking, clause recording and proof obligations. It keeps historical GRASP distinct from the larger modern CDCL engineering stack.
The primary article is João P. Marques-Silva and Karem A. Sakallah, IEEE Transactions on Computers 48(5), 506–521 (1999). The verified DOI is 10.1109/12.769433; the canon's “10.1109/92.769433” is a metadata error. The source pack includes the University of Michigan technical report CSE-TR-292-96, which exposes the architecture, algorithms, proofs and experiments in extended form.
Ten animated accessible SVGs, twelve worked examples, twelve causal probes, twelve memory cards, a claim ledger and a three-scenario conflict laboratory turn the paper's core proof process into an auditable object. Exact truth tables test every learned clause for entailment and assertion.
Primary and contextual sources
- João P. Marques-Silva and Karem A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability”, IEEE Transactions on Computers 48(5), 506–521 (1999). Verified IEEE DOI.
- João P. Marques-Silva and Karem A. Sakallah, “GRASP—A New Search Algorithm for Satisfiability”, University of Michigan CSE-TR-292-96 (1996). Technical report.
- Martin Davis, George Logemann and Donald Loveland, “A machine program for theorem-proving”, Communications of the ACM 5(7), 394–397 (1962).
- Robert J. Bayardo Jr and Robert C. Schrag, “Using CSP look-back techniques to solve real-world SAT instances”, AAAI-97, 203–208 (1997).
- Matthew W. Moskewicz et al., “Chaff: Engineering an Efficient SAT Solver”, DAC 2001, 530–535 (2001).
- Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh (eds), Handbook of Satisfiability, IOS Press; used for later CDCL terminology and historical context.
- SAT Museum, “First solver in the Museum: GRASP”, source-code archive and historical note. Archive record.