LogicSpace: A Dictionary-Based SAT Knowledge Compiler

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

Executive Summary

Experimental Results

Circuit SAT (Integer Factoring)

Binary multiplication circuit $N = p \times q$. CHAIN compiles carry propagation into binary clauses. SEED+CHAIN preprocessing discovers 356–858 backbone variables and exports binary implications that eliminate most solver conflicts.

v1 (SEED+CHAIN only):

v2 (DualTree): On factoring circuits, the DualTree discovers enough backbones via BCP alone to eliminate all solver conflicts:

The DualTree's compile time is higher than v1 preprocessing (the full binary tree has thousands of nodes), but the result is strictly stronger: the solver has nothing left to search. Half the tree nodes are dead (contradictions), confirming that the carry chain structure creates deep propagation chains that BCP under assumptions can fully exploit.

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

Does preprocessing pay for itself? On hard random 3-SAT ($n \geq 250$). These timings were measured on a t3.small EC2 (eu-west-3, 2 vCPU, 2GB RAM) with Glucose3 via pysat. Conflict counts are deterministic (same seed = same conflicts); wall-clock times vary by hardware.

Multi-Solver Comparison

Does it help all solvers? Tested on hard 3-SAT ($n=300$, seed=123) on t3.small EC2. Wall-clock speedups are machine-specific; conflict reduction is deterministic.

Theory

Core Data Structure

Operators

SEED. Clause $C = (l_1 \vee \cdots \vee l_k)$: for each $l_i$, emit $\{-l_j : j \neq i\} \to \{-l_j : j \neq i\} \cup \{l_i\}$.

CHAIN. $D[A]=B,\; D[C]=E,\; C \subseteq B \;\Longrightarrow\; D[A] := B \cup E$. Compiles multi-step BCP into single lookups.

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

EXPORT. Entry $\{a_1, \ldots, a_m\} \to B$ with gain $G = B \setminus A$ emits $|G|$ clauses: $$\forall\, g \in G: \quad (\neg a_1 \vee \cdots \vee \neg a_m \vee g)$$

The Optimal CNF

Tension

The tension $\tau(D)$ measures dictionary completeness:

$\tau = 0$: knows nothing. $\tau = 1$: complete propagation table.

Prove, Extend, Prune

Every operation maps to a SAT call on the optimal CNF:

The Dictionary as a Knowledge Base

Architecture

For large instances (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. Multiple solver threads can work different assumptions concurrently, all writing to the same dictionary.

The Dual Implication Tree

An implication in LogicSpace v2 is a two-output object:

The left output is the standard forced-literal set (AND). The right output is the reduced instance $\mathcal{F}' = \text{BCP}(\mathcal{F} \mid l_i)$: the formula simplified under the assumptions.

Construction: $O(n \log n)$

The DualTree is compiled in three steps:

1. Vocabulary. The achilles heuristic scores each variable by $\text{score}(v) = \max(\text{pos}, \text{neg}) \times (\text{pos} + \text{neg})$, where pos/neg are literal occurrence counts. This produces a full permutation of unassigned variables — computed once, constant, passed downhill.
2. Binary tree. Depth $= \lceil\log_2 n\rceil$. At each node, branch on the next vocabulary variable. Each node calls solver.propagate(assumptions) — pysat's BCP in C, $O(m)$ per call. No search, no decisions, no backtracking.
3. Lift. Every literal forced by BCP under assumptions $\{a_1,\ldots,a_k\}$ lifts to root via the deduction theorem: $$\mathcal{F} \wedge a_1 \wedge \cdots \wedge a_k \vdash l \quad\Longrightarrow\quad \mathcal{F} \vdash (\neg a_1 \vee \cdots \vee \neg a_k \vee l)$$ If both children of a node force the same literal, it lifts with one fewer assumption (AND-lift). Dead branches (contradiction) force the opposite polarity.

Vocabulary determines quality

At depth $d$, a unit clause discovered by BCP lifts to a clause of width $d+1$ at root. The branching order determines how constrained each sub-instance is. A good vocabulary produces sub-instances where BCP finds many forced literals — lifting short, powerful clauses. A bad vocabulary produces sub-instances where BCP finds nothing.

The achilles heuristic selects variables that are both frequent (high occurrence) and polarized (one polarity dominates). Branching on such variables maximizes the asymmetry between the two children, which is when BCP discovers the most.

On-demand deepening: $O(n^2)$

The base compile uses only BCP (fast, shallow). For nodes that deserve richer analysis, deepen() runs the full dictionary pipeline (SEED+CHAIN+CONFLICT) on the sub-instance. This is $O(n^2)$ per node but discovers implications invisible to BCP alone.

Performance

Distributed compilation via recursive Lambda workers

The DualTree is embarrassingly parallel: each node is independent once its assumptions are fixed. This maps directly to a recursive Lambda architecture where each invocation is a full knowledge compiler — not just BCP, but the entire polynomial toolkit. Workers spawn workers, achieving spot exponential branching with pay-per-node pricing.

# Lambda handler — each invocation is a full knowledge compiler
def handler(event, context):
    clauses     = event["clauses"]
    vocab       = event["vocabulary"]
    assumptions = event["assumptions"]
    depth       = event["depth"]
    max_depth   = event["max_depth"]
    n_vars      = event["n_vars"]

    # ── Phase 1: Simplify under assumptions ── O(m)
    assigned = set(assumptions)
    sub_clauses = []
    for clause in clauses:
        if any(lit in assigned for lit in clause):
            continue  # satisfied
        reduced = [lit for lit in clause if -lit not in assigned]
        if not reduced:
            return {"dead": True,
                    "learned": [[-a for a in assumptions[:-1]] + [-assumptions[-1]]]}
        sub_clauses.append(reduced)

    # ── Phase 2: Full DualTree compile ── O(n · log n)
    tree = DualTree.compile(n_vars, sub_clauses)
    forced = tree.backbones
    learned = [[-a for a in assumptions] + [l] for l in forced]

    # Lift all short clauses from sub-tree to root
    for clause in tree.optimal_cnf():
        if len(clause) <= 3 and clause not in sub_clauses:
            lifted = [-a for a in assumptions] + clause
            learned.append(lifted)

    # ── Phase 3: Deepen (optional) ── O(n²)
    tree.deepen_all()
    for lit in tree.backbones:
        if lit not in forced:
            learned.append([-a for a in assumptions] + [lit])

    if depth >= max_depth:
        return {"dead": False, "forced": forced,
                "learned": learned, "insights": tree.insights()}

    # ── Phase 4: Recurse — spawn two child Lambdas ──
    assigned_vars = {abs(l) for l in forced} | {abs(a) for a in assumptions}
    var = next((v for v in vocab if v not in assigned_vars), None)
    if var is None:
        return {"dead": False, "forced": forced, "learned": learned}

    import boto3, json, concurrent.futures
    client = boto3.client("lambda")

    def invoke_child(polarity):
        resp = client.invoke(
            FunctionName="logicspace-dual-worker",
            InvocationType="RequestResponse",
            Payload=json.dumps({
                "clauses": clauses, "vocabulary": vocab,
                "assumptions": assumptions + [polarity],
                "depth": depth + 1, "max_depth": max_depth,
                "n_vars": n_vars,
            }),
        )
        return json.loads(resp["Payload"].read())

    # Both children run concurrently
    with concurrent.futures.ThreadPoolExecutor(2) as ex:
        child_pos, child_neg = ex.submit(invoke_child, var), ex.submit(invoke_child, -var)
        children = [child_pos.result(), child_neg.result()]

    # AND-lift: both children force same lit → forced at parent depth
    if not children[0].get("dead") and not children[1].get("dead"):
        left_f = set(children[0].get("forced", []))
        right_f = set(children[1].get("forced", []))
        for lit in left_f & right_f:
            learned.append([-a for a in assumptions] + [lit])

    # Dead branch → opposite polarity forced
    for child in children:
        learned.extend(child.get("learned", []))
        if child.get("dead") and child.get("learned"):
            learned.extend(child["learned"])

    return {"dead": False, "forced": forced,
            "learned": learned, "children": children}

Each worker is a full compiler. Not a thin BCP probe — every Lambda runs the complete polynomial toolkit on its sub-instance: $O(n \cdot \log n)$ DualTree compilation (BCP propagation tree with vocabulary-ordered branching), then optionally $O(n^2)$ dictionary enrichment (SEED+CHAIN+CONFLICT). The sub-instance is already simplified under the parent's assumptions, so the effective $n$ shrinks at each depth. A worker at depth $d$ with $k$ backbones from its parent operates on $n - d - k$ effective variables.

Cost model. At depth $d = \lceil\log_2 n\rceil$, the tree has at most $2n - 1$ nodes. Each Lambda runs the full compile + deepen pipeline in ~100–500ms with 256MB. On structured instances, 50%+ of branches are dead (no recursion). For $n = 1000$: ~1000 Lambda invocations × 500ms × $0.0000067/GB-s = ~$0.001 per full compile. Wall-clock time = depth × Lambda overhead: $\lceil\log_2 1000\rceil \times 500\text{ms} \approx 5\text{s}$ end-to-end for a 1000-variable instance with full polynomial analysis at every node.

Why this works. The branching factor is 2 and each node is stateless (receives clauses + assumptions, returns learned clauses). No shared memory, no coordination. The parent waits for both children (concurrent invocations), merges their lifted clauses, and returns uphill. The deduction theorem guarantees soundness at every level. The vocabulary (achilles permutation) is computed once by the coordinator and passed to all workers — deterministic branching, reproducible results.

DualTree.compile() accepts a vocabulary parameter: the coordinator computes it once via achilles, every Lambda worker receives it and branches deterministically without recomputing. Same pattern as Snake v6's oppose() literal passed to child workers.

Rephrasing into $\log n$ vocabulary

At depth $d = \lceil\log_2 n\rceil$, the tree branches on $d$ vocabulary variables. At every node, the enriched BCP oracle vivifies the original clauses under the current assumptions. Even if a branch is only locally UNSAT (contradicts under specific assumptions), the vivification shortens the original clause — removing a literal that was provably redundant in that context.

After the full tree completes, every local contradiction at every depth has been used to vivify the original formula. The result: the problem is rephrased in terms of the remaining variables — the ones the vocabulary didn't branch on. If achilles picked the $\log n$ most discriminative variables, the remaining variables are the least connected, the easiest to resolve.

Simplified CNF

The DualTree produces two CNF outputs from one compile:

The simplified CNF applies everything the tree discovered to reduce the original:

1. Global BCP. Load original + all learned clauses into pysat. propagate() with no assumptions discovers forced literals invisible to BCP on the original alone. Remove satisfied clauses, shorten others.
2. Vivification. For each surviving clause $(l_1 \vee l_2 \vee \cdots \vee l_k)$: assume the negation of all literals except one on the enriched solver. If BCP contradicts, that literal is redundant — the clause is shortened. The original formula doesn't know this, but the enriched oracle does.
3. Cascade. Shortened clauses may become units. Propagate iteratively until fixpoint. Deduplicate.

Result: isomorphic to the original, fewer clauses, shorter clauses, same satisfiability. The learned clauses are never in the output — they are the lens, not the picture.

Why vivification on the enriched formula is strictly stronger than on the original. The enriched formula contains learned binary and ternary clauses that create BCP propagation chains absent from the original. When we assume the negation of literals in an original clause, BCP on the enriched formula follows these chains further — reaching contradictions the original cannot see. Every contradiction proves a literal redundant, shortening the clause. This is vivification, but with a polynomial-time compiled oracle (the DualTree's learned clauses) providing the extra propagation power.

On structured instances (factoring), vivification shortens clauses from width 3 to width 2 and removes 40–44% of total literals. On random 3-SAT (n=50), the enriched oracle finds enough to vivify 9 clauses. On larger random instances, shrunk = false — honest. The synthesis boolean tells the recursive Lambda architecture whether to pass the simplified formula downhill: if shrunk = false, further recursion cannot help.

PolySAT integration: 16 techniques by tier

After the DualTree compile (BCP) and vivification, polysat_simplify(max_tier) runs the full PolySAT polynomial pipeline on the simplified formula. Each tier adds techniques at increasing cost:

Factoring 323 (9-bit): original 2,800 clauses / 7,026 literals.

76.3% literal reduction — from 7,026 to 1,667 literals. DualTree compile provides the BCP foundation (43.6%), XOR+Gauss finds parity constraints in the carry chain (62.3%), BCE eliminates blocked clauses (76.3%). Each tier is logged with per-technique fire counts.

tree = DualTree.compile(n_vars, clauses, vocabulary=vocab)

# O(1) — precomputed by compile
tree.simplified_cnf()             # original - BCP knowledge
tree.optimal_cnf()                # original + learned
tree.backbones                    # forced variables
tree.shrunk                       # did it compress?

# On demand — polynomial by tier
tree.polysat_simplify(max_tier=2) # + BCE, HBR, TSER
tree.polysat_simplify(max_tier=4) # + vivify, probe

# Portable
tree.to_json("model.json")
tree = DualTree.from_json("model.json")

The compiled tree is self-documenting: every node records its assumptions, forced literals, and lifted clauses. The JSON artifact can be loaded on any machine without pysat — both the optimal and simplified CNFs are precomputed and served in $O(1)$.

API

POST /instances/clauses              submit CNF as JSON
POST /instances/dimacs               submit CNF as DIMACS text
POST /instances/{id}/preprocess      export optimal CNF (~20ms)
POST /instances/{id}/solve           solve with industrial solver
POST /instances/{id}/prove           verify left => right
POST /instances/{id}/deduce          propagate partial assignment
POST /instances/{id}/entry/detail    inspect an implication
POST /instances/{id}/entry/prune     shrink assumption set
POST /instances/{id}/entry/extend_right  grow deduction set
GET  /instances/{id}/entries         top implications by leverage
GET  /instances/{id}/backbones       forced literals
GET  /instances/{id}/achilles        highest-value variables
GET  /instances/{id}/kpis            tension, coverage, compute
GET  /instances/{id}/export/annotated  optimal CNF with comments
POST /instances/{id}/dual/compile    compile DualTree (O(n log n))
GET  /instances/{id}/dual/insights   tree summary & statistics
GET  /instances/{id}/dual/optimal    optimal CNF from DualTree
POST /instances/{id}/dual/deepen     enrich leaves (O(n^2) on demand)
GET  /instances/{id}/dual/tree       export DualTree as JSON
GET  /ui/{id}                        live resolution dashboard

Discussion

What is new. LogicSpace v1 compiles multi-step BCP into single $O(1)$ lookups, reducing solver conflicts by 62–94% on integer factoring circuits (reproduced). The DualTree (v2) goes further: every implication is a two-output object producing both forced literals and a reduced sub-instance. The $O(n \cdot m)$ compilation via pysat BCP produces a JSON-serializable knowledge artifact that serves the optimal CNF in $O(1)$.

The deduction theorem lift. The key theoretical insight: anything discovered under assumptions lifts to the root as a short clause. At depth $d$, a BCP-forced unit becomes a $(d+1)$-clause at root. Both children forcing the same literal yields the AND-lift — the literal is forced at the parent's depth. Dead branches force the opposite polarity. Every lifted clause is sound by construction.

Structured vs. random. The DualTree's power depends on instance structure. On factoring circuits, BCP under assumptions propagates deeply through carry chains — the DualTree eliminates 100% of conflicts with 82–157 backbones. On hard random 3-SAT, BCP under assumptions finds little — the conflict reduction is modest (7–17%). The DualTree excels where the instance has long implication chains that BCP can exploit. Random 3-SAT at the phase transition has short, tangled chains where search dominates.

Limitations. CaDiCaL/Kissat already do internally what CHAIN does. The DualTree's BCP-only tier discovers what propagation discovers — it cannot find implications that require search. The on-demand deepen() tier adds full dictionary power but at $O(n^2)$ cost per leaf. The depth parameter trades clause width (quality) for coverage (quantity). DualTree compile time scales as $O(n \cdot m)$; on large structured instances (2000+ vars), the tree can have thousands of nodes and produce millions of learned clauses — the compile is still polynomial but wall-clock time grows to seconds.

Reproducibility. The DualTree performance table (nodes, learned counts) is fully deterministic and reproduces exactly across machines. The factoring conflict reductions (94%, 74%, 62%, 87%) reproduce. Wall-clock speedups are hardware-dependent: the factoring table was measured on Apple Silicon, the random 3-SAT table on t3.small EC2. Conflict counts are the reproducible metric; timing ratios vary by ±2× across hardware.

The unique contribution is the compiled tree as a portable artifact. A DualTree JSON file can be loaded without pysat, without the original solver, on any machine. The optimal CNF is precomputed. The insights are immediate. No existing SAT tool produces a self-documenting, JSON-serializable knowledge base from a CNF formula.

Connection to AUMA. LogicSpace is the SAT-domain specialization of AUMA's universal maximization framework (Dana, 2023). The Dana Theorem guarantees polynomial SAT encoding; LogicSpace exploits the structure for fast inference. The dictionary's entries are the SAT analogue of AUMA's Fourier coefficients. The DualTree's depth parameter is the analogue of AUMA's exponent $a$: polynomial budget per node, binary branching on a fixed vocabulary, sound by construction.

Ecosystem

LogicSpace is a library. It runs on a potato. Pure Python, zero native dependencies beyond pysat (optional). pip install it, call DualTree.compile(), get a simplified CNF. The theory is self-contained: DualTree + 16 PolySAT techniques + vivification via enriched BCP. Every operation is polynomial, every result is sound, every output is a valid DIMACS CNF.

npdollars.aws.monce.ai is where LogicSpace scales. The npdollars solver uses LogicSpace as its compilation engine inside recursive Lambda workers. Depth escalation ($d=1$ cheapest first, escalate on stall) controls the cost dial. Each round the formula shrinks, the vocabulary evolves, and $d=1$ finds new simplifications on the easier formula.

The npdollars paper documents the production results: SATLIB UF250 100/100 solved in 3.7s average, 18 workers at $d=1$, $0.0015 per solve. The economics page breaks down the cost model: $0.00003 per round at $d=1$, sub-dollar for any 250-variable instance. The depth dial is the dollar dial.

© 2026 Charles Dana. LogicSpace is open research.
ORCID • GitHub • API • npdollars