LogicSpace: A Dictionary-Based SAT Knowledge Compiler

Charles Dana
Tulane University • Monce SAS • ORCID: 0000-0002-0364-5379
April 2026

1. Core Data Structure

2. Operators

Pillar 1: Learn

SEED. The only operator that reads the CNF. From clause $(l_1 \vee \cdots \vee l_k)$:

CHAIN. Composition: $D[A]=B,\; D[C]=E,\; C \subseteq B \;\Longrightarrow\; D[A] := B \cup E$

CONFLICT. $D[A] \supseteq \{l, -l\} \;\Longrightarrow\;$ learn clause $(\neg a_1 \vee \cdots \vee \neg a_{|A|})$, SEED it.

RESOLVE. Pivot elimination on shared variable.

Pillar 2: Distribute

Deduce. Propagation fixpoint:

Extend. Tense the surface: deduce $\to$ chain $\to$ conflict $\to$ repeat until fixpoint. Free, no search.

Pillar 3: Reflect

UPHILL. The key novel operator. For entry $A \to B$ with $|A| \geq 2$:

PROBE. For each variable $v$: if $\text{deduce}(\{v\})$ contradicts, then $-v$ is a backbone.

Near-miss scoring:

3. Budgeted CDCL: $\text{cdcl}(a)$

Budget $= \lceil n^a \rceil$ decisions. Every step reads from and writes to $D$:

• Propagation via deduce() reads $D$
• Every successful path is documented as an entry in $D$
• Conflict → learned clause → SEED into $D$
• Surviving prefix after backjump is documented too

Key difference from standard CDCL: the dictionary gets smarter between searches. No SAT solver does this. CDCL learns clauses but propagation starts from scratch each time. Here, propagation gets compiled into single $O(1)$ lookups.

4. Prove and Extend

prove(left, right) — verify $\text{left} \Rightarrow \text{right}$ using bounded CDCL under assumptions. Shows $\text{left} \wedge \neg\text{right}$ is UNSAT. Each literal in right is proved independently.

extend(left) — free propagation fixpoint. No search. Tensed surface = maximum deduction achievable from $D$ alone. Documented as $\text{left} \to \text{result}$.

5. Properties

6. Experimental Results

Compiled Propagation

Near-Miss Decision Guidance

Integer Factoring

143 = 11 × 13, encoded as 8-bit multiplication circuit (711 vars, 2185 clauses):

7. The Supervisor

Given a total budget (in deduce evals), the supervisor allocates compute across phases:

1. Tense — extend baseline (free)
2. Probe — failed literal detection (medium cost)
3. Learn + Uphill — cdcl$(a)$ loop with dictionary enrichment
4. Targeted Prove — achilles heuristic picks where to search

The supervisor adapts: cheap ops first, targeted search as $D$ saturates.

8. Implication Set → Optimal CNF

A key application of the dictionary is exporting its accumulated knowledge as a reduced, equisatisfiable CNF. The dictionary compiles propagation chains into single lookups internally; the export translates that compiled knowledge back into a smaller clause set that any external solver can consume.

8.1 Tension of the Implication Set

We define the tension $\tau(D)$ of a dictionary as the fraction of the problem it has resolved:

A dictionary with $\tau = 0$ knows nothing. A dictionary with $\tau = 1$ has compiled the complete propagation table. The extend() operation brings $D$ to its tension fixpoint — the maximum $\tau$ achievable without search:

Each enrichment operation (CHAIN, PROBE, LEARN, UPHILL) strictly increases $\tau$. The tension is a monotonic measure of how much the dictionary has learned.

8.2 Unit Propagation from Backbones

Backbones live in $D[\emptyset]$. Let $\mathcal{B} = D[\emptyset]$ be the backbone set. Define:

$C_{\text{sat}}$ are clauses satisfied by backbones (removed entirely). $C_{\text{short}}$ are clauses shortened by removing false backbone literals. The result after Step 1:

8.3 Implication Subsumption

An entry $A \to B$ subsumes a clause $C$ when the entry guarantees $C$ under weaker conditions:

Interpretation: if every literal in the entry's key is the negation of some clause literal (the "false" side triggers the entry), and the entry's gain contains at least one clause literal (the entry forces it true), then the clause is always satisfied — either some key literal is false (clause satisfied directly) or all key literals are true and the entry fires, satisfying the clause via its gain.

8.4 Baseline Deduction

Beyond entry-level subsumption, the full deduction fixpoint from $D[\emptyset]$ may satisfy additional clauses through chained implications:

Any clause $C$ with $C \cap T^* \neq \emptyset$ is satisfied by the baseline deduction and can be removed. This catches clauses that no single entry subsumes but that the chained propagation covers:

8.5 Variable Elimination

Backbone variables have fixed truth values. After propagation, they can be removed from the variable set entirely. Let $V_{\text{bb}} = \{|l| : l \in \mathcal{B}\}$:

8.6 Learned Clause Injection

This is the key insight: the optimal CNF doesn't just remove clauses — it adds new ones derived from the dictionary's compiled implications.

Each entry $A \to B$ in the dictionary encodes a set of implications. These can be exported as clauses:

These clauses are sound (they are implied by the original CNF, proved by the dictionary) and provide structure that helps external solvers:

An entry $\{x_1\} \to \{x_1, x_5, x_9, x_{12}\}$ (a single-literal entry with gain 3) produces three binary clauses:

These encode a propagation chain that might have required 10 BCP steps in the original CNF. The external solver gets it as three binary clauses — three $O(1)$ propagation steps.

8.7 The Optimal CNF

The full optimal CNF $\mathcal{F}^*$ combines all three sources:

The optimal CNF is not just smaller — it is structurally enriched. The dictionary has discovered the problem's internal implication structure and exported it as explicit clauses that any solver can exploit without rediscovering it.

8.8 The Continuous Improvement Loop

This creates a feedback cycle:

1. Submit a CNF $\mathcal{F}_0$ to LogicSpace. SEED produces $D_0$.
2. Enrich: $D_0 \xrightarrow{\text{learn}} D_1 \xrightarrow{\text{learn}} \cdots \xrightarrow{\text{learn}} D_k$
3. Export: $\mathcal{F}^*_k = \text{optimal}(D_k, \mathcal{F}_0)$
4. Feed $\mathcal{F}^*_k$ to an external solver — it solves faster because of the learned clauses.
5. Or: re-submit $\mathcal{F}^*_k$ for further enrichment.

The tension gap $1 - \tau(D_k)$ measures how much room remains for improvement. The gap monotonically shrinks with each enrichment round.

The tension gap $1 - \tau(D_k)$ measures how much room remains for improvement. At $\tau = 1$ the dictionary has fully compiled the problem; at $\tau = 0$ it has learned nothing. The supervisor allocates compute budget to maximize $\Delta\tau$ per eval.

In practice, structured instances (circuit SAT, graph coloring) reach high tension quickly because their constraint structure creates long implication chains that CHAIN compiles into single lookups. Random instances at the phase transition have low backbone density and plateau at moderate tension — their knowledge is conditional (high-leverage entries with $|A| \geq 2$) rather than unconditional (backbones).

9. Experimental Results: Preprocessing Speedup

We measure whether LogicSpace's polynomial-time preprocessing (SEED + CHAIN, no solver calls) produces clauses that reduce an industrial solver's work. The protocol:

1. Glucose3 on original CNF → $T_{\text{orig}}$, $C_{\text{orig}}$ (conflicts)
2. LogicSpace SEED + CHAIN → dictionary $D$, learned clauses
3. Export optimal CNF = backbone units + surviving originals + learned binary/ternary
4. Glucose3 on optimal CNF → $T_{\text{opt}}$, $C_{\text{opt}}$

9.1 Circuit SAT (Integer Factoring)

Binary multiplication circuit encoding $N = p \times q$ with $k$-bit factors. The circuit structure creates long carry chains that CHAIN compiles into implication entries. Backbones arise from fixed output bits propagating through the circuit.

The speedup increases with instance size: 4.2× at 9-bit, 14.6× at 16-bit. Larger circuits have longer carry chains — CHAIN compiles deeper propagation paths into single entries, which export as binary clauses that give Glucose free BCP. The 648 backbones at 16-bit mean 22% of variables are resolved by preprocessing alone.

The conflict reduction formula:

9.2 Random 3-SAT

Uniform random 3-SAT at clause/variable ratio 4.26 (phase transition).

9.3 The Golden Test: $T_{\text{pre}} + T_{\text{opt}} < T_{\text{orig}}$

The critical question: does the preprocessing pay for itself? Is the total time (preprocessing + solving the optimal CNF) less than solving the original?

On hard random 3-SAT instances ($n \geq 250$, where Glucose takes seconds):

The preprocessing is essentially free compared to the solve: $T_{\text{pre}} \approx 20\text{ms}$ while $T_{\text{raw}} \in [2\text{s}, 13\text{s}]$. The learned clauses from CHAIN reduce Glucose's conflict count, which translates directly to wall-clock savings. The effect is strongest on instances where Glucose takes many conflicts — exactly the hard instances where preprocessing matters most.

9.4 Analysis

The key mechanism: CHAIN compiles multi-step propagation paths into single dictionary entries. When exported as binary/ternary clauses, these give the industrial solver pre-compiled BCP — propagation steps it would otherwise discover through conflict analysis. The preprocessing cost is polynomial ($O(|D|^2 \cdot \bar{k})$ per CHAIN round) and instance-independent: ~20ms for $n=300$.

10. Discussion

What is new. The dictionary is not a clause database. A clause $(a \vee b \vee c)$ is a single constraint. An entry $\{-a\} \to \{-a, b, c, d, e, f\}$ is a compiled propagation chain — it replaces 5 BCP steps with a single $O(1)$ lookup. When exported as clauses, these compiled chains give industrial solvers pre-computed propagation that reduces conflicts by up to 94%.

LogicSpace as a SAT solving hub. The dictionary is a coordination layer between solver calls. Every operation (prove, extend, prune) maps to a SAT call dispatched to an industrial solver. The dictionary stores results permanently. The optimal CNF is the dictionary's knowledge exported as clauses — a one-way ratchet that makes each subsequent solve faster.

Parallelism. Since $D$ grows monotonically, multiple workers can enrich it concurrently with zero conflicts. Worker 1 extends from entry $A$, Worker 2 prunes entry $B$, both write to $D$. This brings parallelism to SAT preprocessing.

Architecture: complementing industrial solvers. LogicSpace is not a solver — it is a knowledge manager that makes industrial solvers smarter. The architecture on a processing machine:

  CNF instance
       |
       v
  +-----------------+
  | LogicSpace      |   SEED + CHAIN (polynomial)
  | Dictionary D    |   -> backbones, implications, entries
  +-----------------+
       |
       | export optimal CNF
       | (original - subsumed + backbone units + learned clauses)
       |
       v
  +-----------------+
  | Industrial      |   Glucose / CaDiCaL / Kissat
  | SAT Solver      |   -> SAT/UNSAT in reduced search space
  +-----------------+
       |
       | learned clauses flow back
       v
  +-----------------+
  | Dictionary D    |   prove(), extend(), prune()
  | (enriched)      |   each = one solver.solve(assumptions=...)
  +-----------------+
       |
       v
  next query (incremental) or export

For large instances (millions of clauses, e.g. SHA-256 circuit SAT), the dictionary identifies which assumptions are worth probing via the achilles heuristic, and dispatches targeted solver.solve(assumptions=[...]) calls. Each result enriches $D$, which identifies the next probe target. Multiple solver threads can work different assumptions concurrently, all writing to the same dictionary. The dictionary is the shared knowledge base; the solvers are the compute muscle.

Limitations. The current Python implementation is 1000× slower than C-based solvers on raw solving. The value is not in competing with Glucose/CaDiCaL on single-shot solving, but in knowledge compilation: building a reusable dictionary that makes multiple related queries faster. The preprocessing overhead (684ms for 2,959 vars) is acceptable when amortized over multiple solves or incremental settings.

Connection to AUMA. LogicSpace is the SAT-domain specialization of AUMA's universal maximization framework. The Dana Theorem guarantees polynomial SAT encoding; LogicSpace exploits the structure for fast inference. The dictionary's implication entries are the SAT analogue of AUMA's Fourier coefficients — both compile a function's structure into a lookup table.

© 2026 Charles Dana. LogicSpace is open research.