PaperlayerView exact revision on arXiv

Source-linked AI summary

PENCIL: Long Thoughts with Short Memory

Chenxiao Yang, Nathan Srebro, David McAllester, Zhiyuan Li

arXiv:2503.14337v2cs.LGcs.CL

TL;DR

CoT’s append-only context retains intermediate computations that are no longer needed, limiting its use for longer reasoning. PENCIL interleaves autoregressive generation with reduction of completed thoughts. The paper reports shorter context and more efficient reasoning, including a 97% success rate on the 5×5 Einstein puzzle, and proves a space-efficient Turing-machine simulation.

  • Problem

    CoT retains intermediate computations in context even when they are no longer needed for future reasoning.

    Source: §1 · p. 1

  • Method

    PENCIL alternates next-token generation with a learned-pattern reduction rule that removes completed intermediate thoughts from context.

    Source: §1 · p. 2, §2.1 · p. 4

  • Results

    PENCIL reduces maximal CoT length from exponential to polynomial on exponential-time tasks, and achieves 97% success on the 5×5 Einstein puzzle with a 25M-parameter transformer and 2048-token context.

    Source: §1 · pp. 2–3

  • Takeaways & Limitations

    A fixed finite-size decoder-only transformer using PENCIL can simulate a Turing machine in T steps and S space with O(T) generated tokens and O(S) maximal sequence length.

    Source: §1 · p. 3

    Experiments use online learning until convergence with unconstrained data access, and include special tokens in CoT that may benefit its training.

    Source: §4 · p. 9

Abstract

from arXiv · show

While state-of-the-art LLMs have demonstrated great promise of using long Chains-of-Thought (CoT) to boost reasoning, scaling it up to more challenging problems at test-time is fundamentally limited by suboptimal memory usage -- intermediate computations accumulate indefinitely in context even when no longer needed for future thoughts. We introduce PENCIL, which incorporates a novel reduction mechanism into the autoregressive generation process that recursively cleans up intermediate thoughts based on patterns learned from training. By iteratively generating and erasing thoughts, PENCIL can think deeper to solve harder problems using shorter context and less compute. Empirically, we observe PENCIL is significantly more effective and efficient than CoT. For example, we demonstrate PENCIL with a small 25M-parameter transformer and 2048 context length solves Einstein's puzzle -- a task that challenges much larger models like GPT-4. Theoretically, we prove PENCIL can perform universal efficient computation by simulating any Turing machines with optimal time and space complexity, and thus can solve arbitrary computable tasks that are otherwise intractable for vanilla CoT.

1 Introduction

CoT retains intermediate computations in context even after they are no longer needed, motivating PENCIL’s reduction-based cleanup. The paper reports more efficient long reasoning and gives both empirical and theoretical results for PENCIL.

Motivation

  • CoT appends each intermediate reasoning step to context, so computations remain there even when no longer useful and complex problems can drive context growth indefinitely.The paper notes this can demand impractical memory and impair information retrieval.Source: §1 · p. 1

Approach

  • PENCIL combines next-token generation with a reduction rule that removes completed intermediate thoughts and merges the answer back into context, recursively enabling nested reasoning.The reduction rule is applied after generation when the sequence matches its pattern.Source: §1 · p. 2

Results

  • PENCIL reduces maximal CoT length from exponential to polynomial on tasks requiring exponential computation time, allowing larger problems under fixed architecture and context.The reported tasks are SAT, QBF, and Einstein’s puzzle.Source: §1 · p. 2
  • 97% success on the 5×5 Einstein puzzle is achieved with a 25M-parameter transformer and 2048-token context.The passage describes this as a task that challenges much larger models like GPT-4.Source: §1 · p. 3

Theoretical result

  • A fixed finite-size decoder-only transformer running PENCIL simulates a Turing machine in T steps and S space with O(T) generated tokens and O(S) maximal sequence length.The paper contrasts this with standard CoT, whose context grows proportionally to O(T).Source: §1 · p. 3

2 PENCIL: Iterative Generation and Reduction

PENCIL pairs autoregressive generation with a pattern-based reduction rule that removes completed intermediate thoughts. Its alternating generation and reduction keeps context shorter than scaffolded CoT and reduces the context used for each generated token.

2 PENCIL: Iterative Generation and Reduction

  • PENCIL addresses CoT’s write-once context by selectively eliminating reasoning traces so models can generate longer thoughts with less memory.CoT permanently retains intermediate computations regardless of their later relevance.Source: §2 · p. 3

2.1 The Reduction Rule and PENCIL

  • The reduction rule removes the intermediate thoughts and special-token triplet from a matching C [CALL] T [SEP] A [RETURN] sequence, merging the answer into context.The rule leaves sequences that do not match the pattern unchanged; allowing [CALL] in context supports nested reasoning.Source: §2.1 · pp. 3–4

2.2 Alternated Generation and Reduction Process

  • At each iteration, PENCIL generates a prompt-response pair ending in [RETURN], then reduces it into the prompt for the next iteration.Generation and reduction alternate, with ineffective reductions simply leaving the sequence unchanged.Source: §2.2 · pp. 4–5
  • PENCIL’s maximal sequence length can be much smaller than scaffolded CoT’s, and its shorter context per token can significantly save compute.For complex tasks, the passage says CoT context can grow exponentially while PENCIL context remains polynomial.Source: §2.2 · p. 5

3 Thinking with PENCIL

This section applies PENCIL’s reduction rule to recursive SAT and QBF solving and to Einstein’s puzzle, including tail recursion for summarization. Across these examples, reduction shortens maximal sequence length while discarded reasoning traces leave final answers preserved.

3.1 SAT and QBF

  • SAT and QBF traces follow recursive variable assignments and branch trials, with [CALL], [SEP], and [RETURN] forming a hierarchical binary tree.Without reduction, the context retains the complete recursive trace, including partial assignments and intermediate formulas; PENCIL discards a branch’s intermediate reasoning when it returns.Source: §3.1 · p. 5
  • At n = 10, maximal sequence length falls from 13,804 to 2,507 for SAT and from 151,661 to 649 for QBF.The reduction rule discards a branch’s intermediate reasoning after it returns, lowering the maximal length from worst-case exponential space to O(n).Source: §3.1 · pp. 5–6, Figure 4 · p. 7

3.2 Special Use Case and Einstein’s Puzzle

  • For the 5×5 Einstein puzzle, maximal sequence length falls from 151,192 to 3,335; without tail recursion, it is 7,705.Figure 4 presents the maximal-sequence comparison.Source: §3.2 · p. 7, Figure 4 · p. 7
  • Einstein’s puzzle asks the model to deduce house attributes from clues; each iteration propagates constraints, merges results through tail recursion, and explores branches while discarding intermediate reasoning.Tail recursion can simplify a complex question into a more tractable one or summarize a lengthy reasoning trace.Source: §3.2 · p. 7

4 Experiments

The experiments compare PENCIL with CoT on SAT, QBF, and Einstein’s puzzle, reporting results across problem sizes, inference budgets, and model capacities. They also examine training convergence and describe the data-processing and evaluation setup.

4 Experiments

  • Training data is scaffolded CoT split into shorter sequences at reduction steps; loss is computed only on tokens generated after the preceding reduction, and batches can reuse KV caches.Experiments use online learning with unconstrained data access and include special tokens in CoT for a fair comparison; evaluation uses 100 held-out instances.Source: §4 · pp. 7–9

4.1 Results on SAT and QBF

  • At inference budgets around 10s for SAT and 40s for QBF, PENCIL handles problems up to n=10, while CoT struggles to scale as budgets increase.The authors attribute this to PENCIL keeping reasoning length polynomial rather than exponential with problem size.Source: Figure 5 · p. 8, §4.1 · p. 9
  • With unlimited context and fixed training FLOPs, PENCIL achieves better QBF performance and converges faster than CoT for n=3–6, with the gap growing for larger problems.CoT results are limited to n=3–6 because larger problems’ space consumption can cause out-of-memory errors.Source: Figure 6 · p. 8, §4.1 · p. 9

4.2 Results on Einstein’s Puzzle

  • 97% accuracy on 5×5 Einstein’s puzzle is achieved by PENCIL with 25.19M parameters and 2048 context length, while CoT reaches 25%.The comparison is with the same architecture and training; PENCIL’s average inference time per sample is 42.98s.Source: Table 2 · p. 9, §4.2 · p. 10
  • For 3×3 Einstein’s puzzle, PENCIL maintains high accuracy at model sizes of at least 3.15M parameters even with limited context, whereas CoT needs larger models and longer context.Both methods perform poorly when model size is too small, indicating a minimum-capacity threshold.Source: Figure 7 · p. 9, §4.2 · p. 10

4.1 Results on SAT and QBF

  • At n=10, CoT accuracy drops to 50% on SAT and 61% on QBF, while PENCIL maintains near-perfect accuracy and exceeds 90% trace rate on most problem sizes.Both methods achieve at least 95% accuracy on smaller problems: n ≤6 for SAT and 5 for QBF.Source: Table 1 · p. 8, §4.1 · p. 9

5 Universal Efficient Computation Power of PENCIL

The section proves that a fixed finite-size transformer running PENCIL can simulate any Turing machine with O(T) generated tokens and O(S) maximal context, using an abstract-machine and FASP proof.

5 Universal Efficient Computation Power of PENCIL

  • A fixed finite-size transformer lets PENCIL simulate any Turing machine in O(T) generated tokens and O(S) maximal context, unlike CoT's O(T) context.Source: §5 · p. 10
  • With polynomial maximal context, PENCIL solves PSPACE, while standard CoT with any poly-time next-token generator solves only P.Source: §5 · p. 11
  • Under P ⊊ PSPACE, PSPACE-complete problems such as QBF cannot be solved by polynomial-length CoT, but PENCIL can solve them with polynomial maximal context.Source: §5 · p. 11

5.1 Autoregressive Machine and Complexity

  • The Autoregressive Machine formalizes computation as token generation, while a state function erases trace details yet preserves information needed for future steps.Source: §5 · p. 11, §5.1 · p. 12

5.2 Space and Time-Efficient Simulation using PENCIL

  • Summarizing after every token bounds context by O(S) but raises time complexity to O(S · T).Source: §5.2 · p. 12
  • PENCIL waits until the trace exceeds twice the state length before summarizing, keeping context O(S) without reducing after every token.Source: §5.2 · pp. 12–13

5.3 FASP for Proving Transformer Expressiveness

  • FASP is a sequence-to-embedding programming language that characterizes finite-transformer functions, reducing the expressiveness proof to a program for the efficient simulation.Source: §5.3 · p. 13

6 Related Work

Prior work improves reasoning structure through trees, graphs, task decomposition, and prompting, while context-optimization approaches still use append-only generation. PENCIL instead learns structured reasoning end to end and addresses CoT's context-growth constraint.

Structured Reasoning

  • CoT can improve performance on complex problems, but its intermediate steps cause unbounded context growth [Wei et al., 2022, Nye et al., 2021, Kojima et al., 2022].Tree and graph reasoning, task decomposition, and prompting frameworks explore alternatives, but require carefully crafted prompts and multiple interaction rounds.Source: §6 · p. 14

Test-Time Scaling

  • Sparse and local attention, KV-cache reduction, and context pruning target long-context bottlenecks, yet retain append-only next-token prediction.The passage characterizes these approaches as inefficient in their use of context space.Source: §6 · p. 14

Computational Power / Limitation of CoT

  • Transformers with CoT may simulate Turing machines, but bounded context constrains their ability to handle problems requiring extensive intermediate computation.The paper presents PENCIL as addressing this constraint through more efficient context use.Source: §6 · p. 14

7 Conclusion

The conclusion identifies CoT's indefinite accumulation of intermediate computations and presents PENCIL's reduction rule as a way to discard finalized reasoning. Its computational-benefits section describes the costs of generation and reduction steps.

7 Conclusion

  • PENCIL removes finalized, unneeded reasoning steps, turning long traces into compact representations for training and challenging tasks under the same memory constraints.The conclusion reports extensive experiments demonstrating effectiveness on challenging tasks with less compute and smaller memory.Source: §7 · p. 14

A Computational Benefits of PENCIL

  • PENCIL's attention-computation accounting separates model-generation steps from reduction steps that recompute the answer's KV cache after merging it into a changed prefix.The generation term is associated with the number of generated tokens; the reduction term reflects the answer length.Source: A Computational Benefits of PENCIL · p. 21

B Additional Experimental Results

The additional material describes a QBF training-convergence comparison and formalizes Turing-machine configurations and their translation equivalence. It states that equivalent configurations preserve future computation behavior.

B Additional Experimental Results

  • Figure 9 compares QBF training convergence for n from 3 to 6, marking each method's first iteration at optimal performance.The horizontal axis is the number of iterations.Source: Figure 9 · p. 21

C.1 Definition of Turing Machine

  • A Turing-machine configuration records its control state, tape contents, and head position, providing a snapshot that determines future computation.The configuration is given as (q, σ′, p).Source: §C.1 · p. 22
  • Translationally equivalent configurations have tape contents and head positions shifted by the same offset, and preserve future computation behavior.The stated lemma says their transition rules agree and updates remain translationally equivalent.Source: §C.1 · p. 23

C.2 Construction of Autoregressive Machine

The construction represents Turing-machine steps as autoregressive tokens and configurations as token sequences. The paper states that this machine faithfully simulates the Turing machine's accept-or-reject output.

C.2 Construction of Autoregressive Machine

  • The autoregressive machine emits one token for each Turing-machine step, encoding the new state, written symbol, and head movement.Its next-token generator applies the Turing machine's transition rule to the configuration reconstructed from prior update tokens.Source: §C.2 · p. 24
  • The embedding maps a Turing-machine configuration to tokens encoding its state, tape symbols, and head position, with the representation invariant to translation.The construction writes non-blank symbols and adds movements as needed to place the head correctly.Source: §C.2 · pp. 24–25
  • The constructed autoregressive machine faithfully simulates the Turing machine, producing the same accept-or-reject output for every input.The proof relates embedded configurations to the original configurations up to translation and establishes the simulation by induction.Source: §C.2 · pp. 25–26

C.3 Construction of State Function sTM

The state function sTM compresses a generated history into a representation of the currently used tape cells and head position. The construction preserves next-token behavior, future traces, and idempotence, while matching the simulated Turing machine’s time and space complexity.

C.3 Construction of State Function sTM

  • sTM maps a token history to an embedding of the resulting configuration, retaining only the currently used tape cells and head position.This is the minimal representation used to condense the full generated history.Source: §C.3 · p. 26
  • The state function preserves next-token predictions, future traces, and its own output when applied again.These are the three properties the construction is shown to satisfy.Source: §C.3 · p. 27
  • sTM preserves the Turing machine’s step count as token generations and bounds its maximum state length by tape usage, preserving time and space complexity.The constructed machine and sTM therefore simulate the Turing machine optimally in both measures.Source: §C.3 · p. 27

D Notations and Transformer Architecture

This section defines the notation and transformer components used in the analysis, then characterizes transformer-computable sequence-to-embedding functions. It also specifies the hard-attention setting and the operator framework used to describe those functions.

D Notations and Transformer Architecture

  • A decoder-only transformer is defined as a next-token generator built from token and positional embeddings, transformer layers, and a decoding layer.The decoding layer projects the final embedding to vocabulary scores and selects the unique argmax token.Source: D Notations and Transformer Architecture · p. 27, §9 · p. 30

D.1 Standard Notations

  • As β approaches zero, softmax becomes hardmax, which distributes weight uniformly across indices attaining the maximum.The analysis uses this instance-wise zero-temperature limit as Average-Hard Attention.Source: §D.1 · p. 28

D.2 Transformer Layers

  • Self-attention forms queries, keys, and values from embeddings, while causal masking restricts the final position to attending only to positions j ≤ n.Multi-head attention concatenates separate head outputs; the paper uses heads with model-dimensional width.Source: §4 · p. 29, §5 · p. 29

D.3 Function Classes Implementable by Transformers

  • The transformer function class contains sequence-to-embedding functions computable by fixed-size transformers, independent of input length.The paper assumes full-precision computation and states that its AHA and layernorm-free intermediate values require O(log(n)) precision at position n.Source: §D.3 · p. 31

D.4 Closed Operators

  • Closed operators take transformer-computable sequence functions as inputs and return functions in the same class; the framework includes attention and concatenation.The section also defines local operators and direct sums as tools for describing these function classes.Source: §D.4 · pp. 31–32

E Full-Access Sequence Processing

FASP specifies programs that build sequence-to-embedding functions using primitive operators, and its expressiveness matches that of fixed-size transformers with the stated positional features and activations. The section also extends the programming framework and introduces more restricted output types.

E Full-Access Sequence Processing

  • FASP supports vector-valued sequences and standard hard attention, and is expressively equivalent to transformers with average-hard attention and causal masking.Theorem E.2 states that FASP and the transformer-implementable function class are equal for any positional feature function and activation class.Source: E Full-Access Sequence Processing · pp. 32–33
  • FASP programs build functions by concatenating existing functions or applying local operators, average-hard attention, linear projections, and nonlinear activations.The program maintains a set of definable functions and adds each newly constructed function to that set.Source: E Full-Access Sequence Processing · pp. 32–33

E.1 Custom Operators in FASP

  • Custom closed operators extend the programming syntax through compositions of primitive or previously defined custom operators while remaining transformer-computable.The paper gives addition as an example and establishes closure results for concatenation, local operators, and average-hard attention.Source: §E.1 · pp. 34–35

E.2 Fine-Grained Types of Seq-to-Embedding Functions

  • The framework distinguishes binary, integer, and one-hot sequence-to-embedding functions by restricting their output ranges.One-hot embeddings are useful before argmax when producing a final token.Source: §E.2 · pp. 35–36

F Notable Special Cases of FASP

The section compares FASP variants with different positional features and activations, showing strict expressiveness increases and an equivalence among three activation choices. It also describes operations available in selected variants, including sequence-length-dependent computation.

F Notable Special Cases of FASP

  • Each inclusion in the hierarchy of FASP variants represents a strict increase in expressiveness.The variants differ in positional features and activation sets.Source: F Notable Special Cases of FASP · p. 37
  • FASP[0; [·]+, ×], FASP[0; [·]+, square], and FASP[0; ReGLU] have equivalent expressiveness.ReGLU is introduced as a gated activation that multiplies one input by the rectified second input.Source: F Notable Special Cases of FASP · p. 37

F.1 Expressiveness of FASP[0; [·]+]

  • With ReLU alone, FASP includes local MLP operators and supports integer comparisons, arithmetic, Boolean operations, and running averages and maxima.The stated comparison and arithmetic operators operate on their respective integer or real-valued inputs.Source: §F.1 · pp. 38–39
  • The paper notes that FASP[0; [·]+] cannot construct Kronecker products over infinite integer or real domains without multiplication, square, or gated ReLU.Its construction over finite one-hot inputs relies on Boolean coordinates.Source: §F.1 · p. 39

F.2 Expressiveness of FASP[0; [·]+, ×]

  • Adding multiplication to ReLU FASP provides a conditional operator that selects between values based on a Boolean condition.This variant is FASP[0; [·]+, ×].Source: §F.2 · p. 40

F.3 Expressiveness of FASP[is_first; [·]+, ×] and F.4 Expressiveness of FASP[seq_len; [·]+, ×]

  • The is_first positional feature enables counting-related operators, while seq_len supports a running partial sum constructed by scaling the average operator.The paper characterizes is_first as the minimal positional embedding that allows counting and notes that computing partial sums entails computing sequence length.Source: §F.3 · p. 41, §F.4 · p. 42

G Proof of Theorem 5.1: Main Result

PENCIL’s fixed finite-size transformer simulates any Turing machine while preserving its output, using O(T(x)) generated tokens and at most O(S(x)) context. Its generator alternates machine simulation with a separator-marked summarization phase that compresses the state for recursive continuation.

G Proof of Theorem 5.1: Main Result

  • PENCIL reproduces a Turing machine’s accept-or-reject output using O(T(x)) generated tokens and at most O(S(x)) maximal context length.The theorem states the construction for a fixed finite-size transformer.Source: G Proof of Theorem 5.1: Main Result · p. 43
  • The generator simulates the machine, emits [SEP] to start summarization, then produces a compressed state followed by [RETURN].The new sequence contains an uncompressed computation block, separator, updated compressed state, and return token.Source: G Proof of Theorem 5.1: Main Result · p. 43
  • The transformer construction implements machine-step generation, selects [SEP] when the sequence reaches the summarization threshold, and simulates summarization.The proof describes the construction using a FASP program and a simplified reduction rule, stating that it extends to the original rule.Source: G Proof of Theorem 5.1: Main Result · p. 43

H Omitted Proofs from Section 5 for Genreal Autoregressive Machines

  • The omitted general-autoregressive-machine proof uses a state function whose repeated application is idempotent, s2(z) = s(z).The accompanying passage says the second part follows from the first, but the displayed relation is incomplete.Source: H Omitted Proofs from Section 5 for… · p. 46

H.1 Proof of Proposition 5.6

The proof bounds PENCIL’s peak sequence length by the simulated machine’s space and its total generated tokens by the machine’s time. It also establishes the limiting behavior of softmax as its temperature approaches zero.

H.1 Proof of Proposition 5.6

  • Each iteration ends when the compressed state is at most half the length of its newly generated segment, limiting how often reductions occur.Iterations span from one selected time step to the next; the proof uses this threshold to avoid excessive time overhead from reducing after every token.Source: §H.1 · pp. 46–47
  • PENCIL simulates the machine with optimal space S(M, s, x) and optimal time T(M, x).The proof bounds the maximum sequence length by O(S(M, s, x)) and total generated tokens by O(T(M, x)).Source: §H.1 · pp. 46–47

I.1 Omitted Proofs in Appendix D

  • As β approaches zero, softmax assigns probability mass only to indices attaining the maximum input value.The proof states that this mass is distributed uniformly among the maximizing indices.Source: §I.1 · p. 48

I.2 Omitted Proofs in Appendix E

Appendix E proves that the specified FASP programs and transformers can express one another. The accompanying examples show a CoT trace and a PENCIL trace ending with the answer False.

I.2 Omitted Proofs in Appendix E

  • The proof establishes both directions of expressibility between FASP programs and transformers in the stated framework.It builds transformer implementations for FASP operations and uses induction over transformer layers to express transformers as FASP programs.Source: §I.2 · pp. 48–49

J.1 Chain-of-Thought

  • The CoT example’s displayed reasoning trace ends with the answer False.The trace includes successive assignments and calls before its final answer.Source: §J.1 · p. 53

J.2 PENCIL

  • The displayed PENCIL example ends with the answer False.The supplied example contains the prompt and final answer, but not a full intermediate trace.Source: §J.2 · p. 53

J.3 Internal Thinking Process of PENCIL

The section presents examples of PENCIL’s internal traces on a Boolean formula and the house puzzle, where the Brit owns the Fish. It also shows a Chain-of-Thought trace evaluating assignments and returning True for the formula, and traces from both methods solving the puzzle.

J.3 Internal Thinking Process of PENCIL

  • PENCIL’s internal trace tries 1 = True, reduces the formula through nested calls, then finds ¬4 and returns True after another branch succeeds.The trace first reaches a contradiction under one branch, then tries 3 = False and obtains ¬4, letting 4 = False satisfy the reduced formula.Source: §J.3 · p. 54

Model Generation (Final Response)

K.1 Chain-of-Thought

  • The Chain-of-Thought trace evaluates assignments against the quantified Boolean formula and returns True.It tests variable values through nested calls, with clause checks identifying a failed assignment before a satisfying one is found.Source: §K.1 · p. 55

K.2 PENCIL

  • PENCIL’s final response for the quantified Boolean formula is True.Source: §K.2 · p. 55

K.3 Internal Thinking Process of PENCIL

  • PENCIL’s internal trace recursively tests quantified-variable assignments and evaluates clauses, returning True for satisfying branches and ultimately for the formula.The trace includes a failed assignment and then checks alternatives, including assignments where all clauses are True.Source: §K.3 · pp. 56–59
  • The internal PENCIL trace evaluates a Boolean formula under assignments to variables 1–4, records every displayed check as True, and returns True.The trace shows assignments 1=False, 2=True, 3=True, and 4=True.Source: §K.3 · p. 60

L.1 Chain-of-Thought

  • Chain-of-Thought solves the house puzzle by branching on House #1’s color, rejecting Blue and propagating Red to the solution where the Brit owns the Fish.The Red branch yields Red/Swede/Dogs, Blue/German/Birds, and Green/Brit/Fish across Houses #1–#3.Source: §L.1 · pp. 63–64

L.2 PENCIL

  • PENCIL’s house-puzzle trace gives the Brit the Fish, with the Red-house/Dogs, Green-right-of-Birds, and Brit-right-of-German constraints satisfied.The displayed solution assigns Red/Swede/Dogs to House #1, Blue/German/Birds to House #2, and Green/Brit/Fish to House #3.Source: §L.2 · p. 64

L.3 Internal Thinking Process of PENCIL

The traces illustrate PENCIL’s puzzle-solving process, using constraint propagation and branching on unresolved possibilities to reach a complete solution and identify the fish’s owner.

L.3 Internal Thinking Process of PENCIL

  • Applying Constraints #1–#4 successively narrows candidates, fixing House #3 as Blue and German and House #1’s pet as Dogs before branching.For example, the RIGHT and LEFT relations remove endpoint candidates, while the Brit-left-of-Birds relation fixes House #3 as German and House #1 as Dogs.Source: §L.3 · pp. 64–68
  • With propagation leaving House #1’s color as Blue or Green, the trace branches on that category, tries Green, and propagates further assignments.The branch yields Red and Birds in House #2 and Fish in House #3, before the remaining nationalities are fixed.Source: §L.3 · pp. 69, 70, 76
  • The puzzle is solved with House #1 Green/Brit/Dogs, House #2 Red/Swede/Birds, and House #3 Blue/German/Fish.The trace reports no unsatisfied constraints after this assignment.Source: §L.3 · pp. 75–76
  • After propagation leaves constraints unsatisfied, branching on House #1’s color and trying Green yields a complete assignment for all three houses.House #1 is Green/Brit/Dogs, House #2 Red/Swede/Birds, and House #3 Blue/German/Fish.Source: §L.3 · pp. 76–77

Model Generation (Final Response)

Related papers

Loading 2503.14337v2…