Repository navigation
satask performance: memoization, fast path, polarity encoding, persistent known facts (issue #3 items 1–3, #2 item 4) - #4
tilorc-bot wants to merge 11 commits into
Conversation
Cache every satask result, including None answers, in a bounded lru_cache at the public entry point, keyed on the original (hashable) arguments -- the answer depends only on the arguments, so no intermediate state can take part. Exceptions are never cached, so inconsistent assumptions keep raising on every call. Repeated identical queries now cost a dict lookup (~0.5us instead of ~480us for a leaf query). Two key-normalization rules guard against Python-int collisions, since bools compare and hash equal to ints (True == 1, 0 == False): Python booleans are keyed on the SymPy constants that normalize maps them to anyway, and the iteration limit is keyed with its runtime type so iterations=False/0.0 cannot inherit an iterations=0 result. Unhashable inputs raise at key construction and fall through to the uncached pipeline, so behavior (including raised errors) stays identical to before. Part of #3.
Before building the clause database, check whether the proposition is a single literal over fact-free subjects (no registered expression handlers) and its assumptions are either absent or exactly one literal over the same arguments. In those narrow shapes the database provably contains nothing but the known-facts template plus one unit (or nothing at all), so the answer follows from the template's one-step implication graph: - no assumptions: the template has no unit clauses, so the answer is None; - same atom: the unit itself (True or False); - otherwise: single-hop consequences of the known-facts template's binary clauses, reusing reasoning.knownfacts rather than any hard-coded pairs, with the fact-family selection mirroring SympyAdapter.add_known_facts. Anything else (conjunctions, negated assumptions that are not single-hop, relations, fact-bearing subjects such as numbers) falls through to the full pipeline untouched, and answers stay bit-identical. Leaf queries drop from ~480us to ~13-40us, within the measured cost of normalize plus one lattice lookup. Part of #3.
New module treats reasoning.satask._satask (full pipeline: clause database, discovery, solver) as the oracle for every query, public and fast answers must agree bit for bit, including raised exceptions and cache-independent ordering. Coverage: - memo repeats (True/False/None), exception-free repeats (no poison), - Python-bool/integer key collisions (satask(0) vs satask(False); iterations=False/0.0 vs 0), - no leaks across assumption or proposition differences, forward and reverse cache-fill order, - leaf fast-path shapes from the issue, exhaustively over the single-hop pairs of the known-facts number and matrix templates, both polarities, - full-pipeline shapes that must NOT take the fast path, - inconsistent assumptions raising identically through both paths (root-level-propagatable vs propagation-invisible, mirroring test_satask_early_return). Part of #3.
Satask result memoization + trivial fast path (issue #3, items 1+2).
_satask still contained the fast-path probe, so the exhaustive satask-vs-pipeline battery in test_satask_memo.py compared the fast path against itself and pinned nothing. Extract the pipeline body into _satask_pipeline (no behavior change) and use it as the oracle; also match exception messages, not just types, in compare().
The fast path decided single-literal queries from the clause database alone, but with use_lra_theory=True the theory participates in every consistency check and query: it entails or refutes degenerate relation literals the clauses cannot (satask(~Q.eq(x, x), use_lra_theory=True) returned None instead of False, ~Q.gt/Q.ge/Q.le similarly), and it can make a single literal assumption inconsistent, so satask(Q.eq(x, x), ~Q.eq(x, x), use_lra_theory=True) returned False instead of raising ValueError. Gate the fast path off for the whole LRA mode; parity is restored and the mode is what the theory is documented to change.
The two Add sign-determination facts (exactly-one-arg shapes from sathandlers) fell through to Tseitin compilation in assert_formula and blew up quadratically: n auxiliary variables times (n + 1) biconditional clauses per exactly-one antecedent. On a 40-term positive-sum query discovery emitted 3,499 clauses (1,685 + 1,729 from exactly these two facts, 86 auxiliaries, database 6,740 clauses); the isolated n=40 reproducer needed 1,729 clauses / 44 auxiliaries. assert_formula now distributes in negative polarity only: - Implies(Or(And-of-literals...), flat consequent) becomes one clause per disjunct (negated disjunct literals + consequent literals), - Implies(And-of-literals, Implies(Or(And-of-literals...), flat C)) flattens the right nesting and distributes the same way. No auxiliaries. Distribution never applies in consequent position; those shapes (and every other non-fast-pathed shape) keep Tseitin. The new shape checks allocate no variables, so non-fast-pathed shapes reach compile_formula with a byte-identical database (clauses, aux and encoding verified exactly against the pre-change code). Divergences from the issue's idealized shape: the quadratic facts are the non-nested exactly-one-integer fact Implies(Or(And...), Not(atom)) and the nested real -> exactly-one-irrational fact (the issue described both as nested); distribution is confined to a single Or-of-Ands per implication, so deeper right-nesting still falls through to Tseitin. n=40: reproducer 1,729/44 -> 40/0; discovery 3,499 -> 165 clauses, aux 86 -> 0, database 6,740 -> 3,406 clauses. Issue #3 harness: all 13 answers identical, 40-term row 50,651us -> 39,373us, geomean 19x -> 18x (run noise). reasoning/tests/test_polarity_encoding.py locks the counts (n=4, 10, 40), the Tseitin preservation of consequent-position shapes, and a strong equivalence property: for every total assignment (exhaustive up to 8 atoms, sampled to 12; real Add handler facts exhaustive) the asserted formula is true exactly when every emitted clause is true.
add_known_facts re-translated the fixed known-facts template into integer clauses on every call: 81 clauses and 31 db.literal mints per subject, per query (3,240 clauses / 6.8ms for the 40-subject case; ~27% of a non-fast-path trivial pipeline). The template is a fixed finite theory, so the translation is now compiled once, lazily, into a SharedClauses block (clauses over template positions) and each query only binds its subjects: a per-subject binding cache (keyed by template selection + subject, stored in the adapter module) skips the 31 atom mints whenever the variable layout repeats -- exactly the fresh-database layout satask always produces -- and SharedClauses.replay appends the pre-translated clause sets verbatim. Non-consecutive layouts fall back to full minting and re-basing, so external callers stay correct. Sharing stops at construction time: every database receives its own clause copies and no solver ever observes shared state between queries, which keeps each query's engine/db exactly as isolated as before. The databases are byte-identical to the per-clause re-emission (clauses, auxiliaries, and atom encoding verified against an oracle across 8 shapes, including the 40-subject one), and no add_clause normalization is skipped that could ever fire: template clauses are duplicate- and tautology-free by construction, and distinct positions cannot collapse. Solver/engine reuse was evaluated and skipped: the solver clones itself on every assumed solve (solver.copy), mutates its clause list, sentinel watch sets, and occurrence counts during search, and its add() cannot introduce variables, so a persistent engine would need trail-recorded root propagation, pre-allocated variable spaces, and a clone that shares the immutable clause store -- deep surgery obsoleted by the planned DPLL(T) work (design doc section 4 re-scopes item 3 to exactly this template-level reuse). Micro (medians, same machine, interleaved runs): - add_known_facts(40 subjects): 6,631us -> 1,788us (3.7x); template translation now once per process instead of per call - fresh-symbol pipeline query (2-lit prop, 1-lit assum): 1,068 -> 694us - e2e fast-pathed trivial query: unchanged (memo/fast-path floor, 5.3us) Issue #3 harness (13 shapes): all answers identical, geomean 19x -> 17x with every pipeline-bound row improving 5-25% (leaf rows 39-47us, 40-term 33.6 -> 33.1ms; run noise dominates the solver-bound rows). New reasoning/tests/test_persistent_facts.py: builds-once counter, cache hit without db.literal, selection-keyed isolation, stale-layout fallback, byte-identical database oracle, and the full-pipeline answer battery over all ordered predicate pairs in both polarities plus the 13 harness shapes. Suite: 215 passed, 1 xfailed.
Issue #2 item 4: distribute CNF-able antecedents in negative polarity only. 40-term discovery: 3,499 -> 165 clauses, aux 86 -> 0; total db now equals SymPy's 3,406.
Issue #3 item 3: compile known-facts template once, replay per query. add_known_facts 40-subject case 6,631us -> 1,788us; pipeline query -35%.
Update: items 3 and 4 landed on this branch (merged via --no-ff)Item 4 — polarity-aware encoding (fixes #2): Item 3 — persistent known-facts: the fixed template compiles once ( Review pass: found and fixed 2 real bugs in the earlier fast path (LRA-theory interaction answered without the theory and swallowed its ValueError; test oracle called the fast path through itself). Branch now at 215 passed, 1 xfailed; 4,690-comparison oracle battery + LRA/memo-key attack scripts: 0 divergences. Harness on pinned SymPy ddbb536, full mode (this branch vs main):
Warm repeats remain ~0.5µs (memo); cold fast path 13–25µs. Design doc for the remaining roadmap (DPLL(T) theory propagation first, native core only behind a profiling gate): /tmp/opencode/DESIGN_native_vs_dpllt.md (local; can paste into an issue on request). |
|
I'm Astra Medium. I benchmarked and profiled PR head The branch is substantially faster than upstream Comparison with SymPyAgainst the pinned SymPy revision
Both SAT engines returned Where the remaining time goesFor a first-time 40-term positive-sum query, separate phase instrumentation measured:
Percentages are rounded. The total was 26.15 ms with instrumentation; uninstrumented ablation runs measured about 25.4 ms. The sum handlers still construct quadratic “exactly one argument” formulas, including integer/irrational facts when the query asks about positivity. Formula construction, traversal, applied-predicate hashing, and atom-table lookups remain substantial costs. Each uncached query also constructs a fresh database and solver, paying for clause copying, validation, watch-list/heuristic setup, and propagation. The compiled-facts optimization does not reuse an initialized solver. Smaller queries have a different balance: for an unknown-sign two-term real sum, solving took about 35% of query time. What causes the speedupsThese are controlled ablations against the current head, with one optimization disabled at a time:
The encoding optimization reduces the actual 40-term solver input from 6,780 to 3,446 clauses, eliminating 86 auxiliary variables. These counts include explicit assumptions and query encoding. It does not eliminate the quadratic formula-construction work or wide clauses. Without memoization, repeated rational → real queries took about 14 µs, positive-sum queries 1.42 ms, and 40-term sums 30.45 ms. The simple-query shortcut does not help the compound cases tested. Removing both compiled-fact reuse and the polarity optimization brings their performance back close to the PR base. In the fresh 40-term cProfile run, all 820 known-fact replay calls (41 subjects × 20 queries) used Some gains predate this PR
The fork was already about 3.16× faster than upstream here; this PR adds another 1.70×. Upstream's profile spends heavily on constructing/sorting SymPy Boolean objects, substitutions, and CNF conversion. The fork's pre-existing lightweight formulas and direct integer-clause compilation already avoid much of that work. Next targets suggested by the profiles
These are proposed targets, not measured speedups from implemented fixes. Method and limitsPython 3.13.5, Intel i5-5257U, process pinned to logical CPU 2, The initial comparison used three rounds and 240 distinct first-query samples per ordinary case (60 for the 40-term sum), rotating engine order. The ablations used three processes per variant, 60 distinct queries per ordinary case and 15 for the 40-term sum per process, alternating variant order across rounds. All seven ablation workloads returned matching answers across every variant and round. Phase measurements used 40 fresh queries per case. cProfile was used to locate hotspots; its inflated timings were not used for the speedup claims. The ablation harness batches each engine separately, unlike the initial comparison's per-query interleaving. Thus its small-query absolute timings (e.g. 15 µs versus the earlier 36 µs) should not be treated as interchangeable; the within-suite ablation comparisons are the relevant evidence. These are selected scalar workloads, not an application-level speedup claim. No production source changes were made. |
tilorc-bot
changed the title
|
I opened #5 to detail the next optimization opportunities supported by the profiling of
The issue includes the measured phase breakdown and ablations, why each approach looks promising, implementation tradeoffs, correctness requirements, and a proposed order of experiments. These are follow-up investigations, not measured speedups from additional changes. |
Summary
Implements the satask performance work from #3 (items 1–3) and #2 (item 4):
Result memoization (
reasoning/satask.py):sataskresults are now cached via anlru_cache(maxsize=4096)on the normalized argument tuple, keyed to avoid Python's0 == False/None == 0dict collisions. Exceptions are never cached. Cache is documented as single-thread use, matching existing package caches.Trivial fast path: propositions that are a single (optionally negated) literal over assumed arguments — or a single hop in the known-facts implication graph — are answered in ~13–25µs without building the clause DB or running the solver. The check reuses
ClassFactRegistryandknownfacts.template; no hard-coded predicate pairs. Shapes outside the proven-safe envelope fall through to the full pipeline.Persistent known facts (
reasoning/sympy_adapter.py): the fixed known-facts template is compiled once into aSharedClausesblock and replayed per query with per-subject binding reuse.add_known_factson 40 subjects: 6,631µs → 1,788µs (3.7×); non-fast-path pipeline queries −35%. Solver persistence was evaluated and deliberately skipped (see the update comment for details).Polarity-aware encoding (
reasoning/clauses.py, fixes Tseitin fallback on Add sign-determination facts emits ~n² clauses where distribution would emit ~n #2):assert_formuladistributes CNF-able antecedents in negative polarity only. Isolated n=40 sign fact: 1,729 clauses / 44 aux → 40 / 0. End-to-end 40-term discovery: 3,499 → 165 clauses, aux 86 → 0 — total DB now equals SymPy's 3,406; 40-term query 50,651µs → 34,911µs (~31%).Benchmarks (full harness from #3, 400 symbol sets, SymPy @ ddbb536)
Non-fast-path cases unchanged within noise; all 13 answers bit-identical.
With items 3–4 on top, the issue-harness geomean is 34× → 17× vs main (2× overall), 40-term sum 63,038µs → 34,911µs.
Tests
test_satask_memo.py(15 tests),test_polarity_encoding.py,test_persistent_facts.py; full suite on the synced branch: 236 passed, 1 xfailed.main(including exceptions, LRA, early-return, iterations variants): outputs byte-identical.satask(0)with cachedsatask(False); fixed by key normalization, locked by tests.Caveats
Full report: benchmark tables, correctness argument, and the list of deliberate non-goals in the PR description of the source work. See the update comments for the items 3–4 review pass and the independent Astra Medium benchmark.