Method

Caption: Illustration of the satisfiability-aided language modeling approach (right). SATLM parses an NL input into a declarative task specification (a set of logical constraints) using prompting, then uses a SAT solver to solve the problem. The chain-of-thought strategy in prior work (left) yields imperative reasoning processes.

SATLM can be viewed as parse → plan → execute, but with a deliberate division of labor: the LLM focuses on parsing (NL → constraints), while the solver handles planning/search + execution.

• 1) Declarative Parsing (parse)Prompt the LLM (few-shot) to output a declarative specification: a small set of logical constraints plus a query. This is “declarative” because it states what must be true, not how to solve it step-by-step.

• 2) Translation (parse → solver input) Convert LLM generated declarative parse into a solver-ready satisfiability instance

• 3) Solving (plan + execute) Run an automated theorem prover / SMT solver (Z3 in the paper’s implementation) to find a satisfying model

• 4) Using solver feedback Compared to executor-only approaches (which mostly detect “runtime” failures), the solver can return richer signals:

  • ERROR (invalid formulas / timeout)
  • UNSAT (constraints inconsistent)
  • AMBIG (multiple solutions / underconstrained, depending on the task/query)

  SATLM can use these signals to abstain when the parsed spec is likely wrong, inconsistent, or underspecified.

Experiments

Prompting Techniques

• STANDARD: direct answer prediction (few-shot).
• COT: chain-of-thought prompting.
• PAL / PROGLM: executor-augmented program-aided baseline (not applicable to all datasets; shown as “-” in the table when not used).

Decoding

• Report greedy and self-consistency.
• Self-consistency uses 40 samples on most datasets, and 5 on long/expensive ones (LSAT, BOARDGAMEQA, PROOFWRITER).

Language models

• Main results use code-davinci-002.
• Additional tests include gpt-3.5-turbo (0613), text-davinci-003, and code-davinci-001.

Datasets / abbreviations (as used in Table 1)

• GSM / GSM-SYS / ALGE: arithmetic reasoning (ALGE = algebra textbook problems).
• LSAT / BOARD / CLUTRR / PROOF: logical reasoning (PROOF = PROOFWRITER).
• COLOR: symbolic reasoning (Colored Object from BIG-bench).
• REGEX: structured regex synthesis (StructuredRegex / STREGEX).

Main results (Table 1)

The paper’s main table reports accuracy (%) across datasets/tasks with code-davinci-002 (greedy and self-consistency).

What parts matter

SATLM has two intertwined ideas: (1) make the LLM write a declarative spec (constraints + query), and (2) let a symbolic solver do the planning/search and execution. The paper disentangles them by holding the declarative prompt format fixed, and swapping out what does the “solve” step.

Caption: A variant of the approach which replaces the SAT solver with a “CoT solver” that takes the SAT problem as input and solves it in natural language.

On GSM-SYS, GSM, and CLUTRR (greedy decoding, code-davinci-002), they compare:

• Sat_SymSolver: the full SATLM pipeline (declarative spec + symbolic solver)
• Sat_CotSolver: same declarative spec, but the LLM tries to solve the spec in natural language (so the LLM is doing the planning/execution again)
• Sat_NoSolver: declarative prompting, but then directly answer (no separate solve stage)

Results (accuracy %, greedy):

Dataset	CoT	Sat_CotSolver	Sat_SymSolver
GSM-SYS	46.5	54.5	69.4
GSM	62.7	63.2	71.7
CLUTRR	40.8	48.9	68.3

• Declarative prompting helps even without a symbolic solver: Sat_CotSolver beats vanilla CoT on GSM-SYS (+8.0) and CLUTRR (+8.1). So parsing the problem before solving helps.

• Sat_SymSolver beats Sat_CotSolver by +14.9 (GSM-SYS), +8.5 (GSM), and +19.4 (CLUTRR).

• They manually analyze 40 cases where the symbolic solver succeeds but the CoT-solver fails, and find most errors are planning errors (not arithmetic slips). Reported planning-error rates are 72.5% (GSM-SYS), 42.5% (GSM), 47.5% (CLUTRR).

• SATLM relies on the LLM to do a strong job at “reading the problem” (including implicit commonsense premises), while the solver handles the structured reasoning.

Caption: Example outputs from GSM (left) and BOARDGAMEQA (right) show that LLMs can perform commonsense reasoning while parsing.

Limitations

• If the LLM misparses the problem into the wrong constraints, the solver will still solve the wrong problem perfectly.
• Solver-backed reasoning can be computationally expensive for complex formulas (e.g., nonlinear arithmetic, quantifiers).
• Practical performance depends on prompting/spec design (how you express constraints and queries so the model reliably produces well-formed specs).

Final Thought

SATLM fits into the tool-using & neuro-symbolic lines of work: LLMs parse; solvers reason. When the task stresses planning/search rather than just execution, that division of labor can pay off.