diff --git a/README.md b/README.md index c09656f..6f8e1d0 100644 --- a/README.md +++ b/README.md @@ -64,7 +64,7 @@ solving remains future work. | --- | --- | | Yang–Zhang formula-to-region construction | Implemented and tested | | Reference serial solver | Implemented | -| Optimized serial path | Implemented with five isolated, measured mechanisms | +| Optimized serial path | Implemented with six isolated, measured mechanisms | | Independent native verifier | Implemented and required before SAT publication | | Boolean Z3 oracle | Implemented over the copied immutable `Formula` | | Wang Z3 oracle | Implemented over copied `Region + TILESET` | @@ -81,9 +81,10 @@ solving remains future work. | `TaskPlan` and native OpenMP solver | Not implemented; only the build scaffold exists | The optimized path preserves the reference path's Wang semantics and public -contract. Its five retained mechanisms are dynamic DFS storage, omission of +contract. Its six retained mechanisms are dynamic DFS storage, omission of non-consumable initial-propagation trail entries, SAT-domain ownership -transfer, byte-wise support aggregation, and queue deduplication. The +transfer, byte-wise support aggregation, queue deduplication, and a lazy +private MRV index that preserves the reference path's row-major tie break. The [optimization methodology](docs/solver_performance_scope.md) defines their acceptance boundary. Dated reports preserve the measurements and their host-specific limitations. @@ -155,10 +156,11 @@ diagram. ## Next milestones -Planned work remains separated into independently reviewed changes. The new -priority is explainability across the deterministic pipeline: +Planned work remains separated into independently reviewed changes. The next +serial-evidence packets are: -1. resume serial MRV and hard-UNSAT evidence; +1. extend the hard-UNSAT/scaling corpus and record the option matrix now that + the isolated MRV mechanism is measured; 2. define `TaskPlan` only after the serial evidence, then implement and measure real OpenMP execution. diff --git a/benchmarks/c/bench_solver.c b/benchmarks/c/bench_solver.c index a3fbbe9..0135f57 100644 --- a/benchmarks/c/bench_solver.c +++ b/benchmarks/c/bench_solver.c @@ -488,6 +488,8 @@ static bool metrics_equal( left->support_byte_lookups == right->support_byte_lookups && left->support_table_bytes == right->support_table_bytes && left->mrv_cells_scanned == right->mrv_cells_scanned && + left->mrv_index_word_probes == right->mrv_index_word_probes && + left->mrv_index_bytes == right->mrv_index_bytes && left->initial_trail_writes == right->initial_trail_writes && left->search_trail_writes == right->search_trail_writes && left->initial_trail_rewrites == right->initial_trail_rewrites && @@ -777,7 +779,7 @@ static bool run_benchmark( ); printf( - "benchmark_version=8 case=%s solver=%s scope=%s expected=%s " + "benchmark_version=9 case=%s solver=%s scope=%s expected=%s " "iterations=%zu metrics=%u capture_unsat=%u " "elapsed_ns=%" PRIu64 " ns_per_iteration=%" PRIu64 " " "process_peak_rss_kib=%ld peak_rss_source=%s " @@ -789,6 +791,8 @@ static bool run_benchmark( "support_byte_lookups=%" PRIu64 " " "support_table_bytes=%zu " "mrv_cells_scanned=%" PRIu64 " " + "mrv_index_word_probes=%" PRIu64 " " + "mrv_index_bytes=%zu " "initial_trail_writes=%" PRIu64 " " "search_trail_writes=%" PRIu64 " " "initial_trail_rewrites=%" PRIu64 " " @@ -823,6 +827,8 @@ static bool run_benchmark( reference_metrics.support_byte_lookups, reference_metrics.support_table_bytes, reference_metrics.mrv_cells_scanned, + reference_metrics.mrv_index_word_probes, + reference_metrics.mrv_index_bytes, reference_metrics.initial_trail_writes, reference_metrics.search_trail_writes, reference_metrics.initial_trail_rewrites, @@ -942,7 +948,7 @@ int main(int argc, char **argv) print_usage(argv[0]); return EXIT_FAILURE; } - printf("benchmark_version=8 "); + printf("benchmark_version=9 "); #if defined(__clang__) printf( "compiler=clang-%d.%d.%d ", diff --git a/docs/serial_solver_implementation_guide.md b/docs/serial_solver_implementation_guide.md index 4c65724..4df2f81 100644 --- a/docs/serial_solver_implementation_guide.md +++ b/docs/serial_solver_implementation_guide.md @@ -294,10 +294,19 @@ domain. Rollback walks entries in reverse to a saved marker and updates for the same cell are intentional because they reproduce every intermediate state exactly. -MRV selection scans active cells in row-major order and chooses the smallest -nonsingleton domain. Ties retain the lowest dense index, candidates are tried -in ascending tile-ID order, and propagation visits neighbors in `N`, `E`, `S`, -`W` order. These rules make each path deterministic for a fixed mechanism set. +The reference MRV selection scans active cells in row-major order and chooses +the smallest nonsingleton domain. The optimized path makes the same first +selection linearly, then lazily creates packed membership buckets for domain +sizes 2 through 23 only if search descends below the root. It selects the +smallest nonempty bucket and its lowest dense cell index. Every restriction and +rollback updates this private index while `domains` remains the source of +truth. Root conflicts, complete regions, and searches exhausted at the root +allocate no index. + +Both paths therefore retain the lowest dense index on ties. Candidates are +tried in ascending tile-ID order, and propagation visits neighbors in `N`, +`E`, `S`, `W` order. These rules make each path deterministic for a fixed +mechanism set. DFS uses a heap-allocated stack rather than the process stack. A frame holds the chosen cell, remaining candidates, and the trail position before the @@ -365,6 +374,7 @@ meanings: | --- | --- | | `dfs_nodes`, `decisions`, `backtracks`, `failed_leaves`, `max_depth` | Search states, attempted singleton branches, restored failed branches, observed conflicts, and deepest DFS level | | `domain_reductions`, `propagated_arcs`, `mrv_cells_scanned` | Effective narrowing operations, processed directed neighbor arcs, and active cells inspected by MRV | +| `mrv_index_word_probes`, `mrv_index_bytes` | Packed bucket words inspected by optimized MRV selection and combined bucket/cache storage; zero for the reference path and optimized runs that never build the lazy index | | `support_tile_visits`, `support_byte_lookups`, `support_table_bytes` | Reference set-tile work, optimized nonzero-byte work, and optimized table storage | | `initial_trail_writes`, `search_trail_writes` | Undo entries appended in initial propagation and DFS | | `initial_trail_rewrites`, `search_trail_rewrites` | Repeated entries for a cell within the initial interval or current branch interval | @@ -541,9 +551,9 @@ make cachegrind-check ``` The benchmark and profiler paths keep metrics runs separate from timings and -measure MRV scans, queue duplication, trail pressure, domain reductions, -support aggregation, SAT-copy bytes, process peak RSS, and instruction/cache -attribution. Dated reports in the +measure MRV scans and packed-word probes, queue duplication, trail pressure, +domain reductions, support aggregation, SAT-copy bytes, process peak RSS, and +instruction/cache attribution. Dated reports in the [solver optimization section]({{ '/#solver-optimization' | relative_url }}) record the evidence for each retained optimized mechanism. diff --git a/docs/solver_mrv_index_2026-08-28.md b/docs/solver_mrv_index_2026-08-28.md new file mode 100644 index 0000000..1aaf217 --- /dev/null +++ b/docs/solver_mrv_index_2026-08-28.md @@ -0,0 +1,290 @@ +--- +layout: page +title: Optimized solver MRV index +permalink: /solver_mrv_index_2026-08-28/ +description: Evidence for the optimized solver's private row-major MRV bucket index. +section: Solver optimization +document_kind: Benchmark report +status: Accepted mechanism +updated: 2026-08-28 +nav_order: 85 +--- + +# Optimized solver MRV index — 28 August 2026 + +This accepted sixth serial mechanism replaces repeated linear MRV scans only +inside `wang_solve_optimized()`. The reference solver retains its explanatory +row-major scan. The optimized path derives 22 private buckets for domain sizes +2 through 23, stores bucket membership in packed cell-index bitsets, and keeps +one cached domain-size byte per dense cell. Selecting the first nonempty size +bucket and then its lowest set cell bit preserves the existing minimum-domain, +row-major tie break. + +The index is created lazily only after a root branch propagates successfully +and search must descend to a child. Root conflicts, fully resolved regions, +no-search cases, and UNSAT runs that exhaust only the root frame allocate no +MRV index. Every later domain restriction and rollback moves the cell between +buckets; `domains` remains the semantic source of truth. Queue scheduling, +support aggregation, trail entries, trace events, SAT ownership, `TaskPlan`, +and OpenMP are outside this mechanism. + +## Reproduction identity + +The accepted base is the observed-run dossier squash commit: + +```text +ca8690ce31ae63b922f52bd7cae24c21c65a27eb +Add opt-in observed-run dossiers (#19) +``` + +Both comparison binaries use benchmark schema v9, the same source tree, +compiler flags, link order, public metric layout, and harness. They differ only +in the private switch `WANG_OPTIMIZED_MRV_INDEX`: + +```text +cdc3ff40840e4ef2e75865f6affa27328e15cb180bab6b420ad8b552497ff07c switch=0 +a79d2b78680e38090ef190c62ed87ce5bd064df0649d1f90aa5f36f1f0507722 switch=1 +``` + +Final implementation source identities: + +```text +611e60e4b34406318f7106b5a92daef5bc35cbe15775b061c6193c1c75dc6d68 include/wang/solver.h +94b992f6c1d167b91e978ab110eaa8a5aa758b8b7edac194bff8e3aad8145793 src/solver/solver_serial.c +34fcaed4bfb69cc71b37aa77a4d49158d5e10071c2c80be155094cb0e6289463 benchmarks/c/bench_solver.c +53062e8768acdd3cb21204e63c4e7baa721886303ecd8b6c029b8f41a1e754ab tests/c/test_solver.c +f57fba10f7452b97f3563fb13bec447cb8725a0541aff25294bf81d9951a4510 tests/c/test_solver_differential.c +e61b2be36fc0cd859e2fd1106118d383b223109e37fb2871c99bd64c4d7174ff python/native/witness_adapter.py +``` + +Environment: + +```text +Debian GNU/Linux 13 +Linux 6.12.105+deb13-amd64 x86_64 +AMD Ryzen 5 3600, 6 cores / 12 threads, boost enabled +GCC 14.2.0 +Clang 19.1.7 +C17, portable -O2; no -march=native or LTO +Valgrind/Callgrind/Cachegrind 3.24.0 +``` + +## Preventive red test and lifecycle + +The differential test first required optimized MRV storage and probes, lower +cell-scan work, zero reference storage, and correct cleanup through the +existing 4-by-4 backtracking case. Building that test failed because +`WangSolverMetrics` did not yet contain `mrv_index_word_probes` or +`mrv_index_bytes`. + +The retained test now observes the same SAT result, ten decisions, two failed +leaves, two backtracks, domain reductions, queue work, trail work, and verified +witness as before. Linear MRV inspects 83 active cells; the lazy indexed path +inspects 22 cells, probes seven packed words, and owns 192 bytes. Separate +controls require zero MRV bytes and probes for initial conflicts, no-arc +solutions, and Yang–Zhang UNSAT runs that never descend below the root frame. +Metrics-disabled differential runs still require the entire public metric +object to be zero. + +The storage formula for a search that descends is: + +```text +22 * ceil(cell_count / 64) * 8 + cell_count bytes +``` + +The first term is the 22 packed membership buckets. The second is the cached +domain size. Both live in one zero-initialized allocation owned by the solver +state. Allocation failure returns `ERROR` before a child frame is published; +normal destruction frees the combined allocation once. + +## Direct work evidence + +One metrics-enabled optimized solve per corpus case produced the following MRV +work. All non-MRV deterministic metrics were identical between the switch-off +and switch-on binaries. + +| Case | Cells scanned off | Cells scanned on | Packed-word probes | Index bytes | +| --- | ---: | ---: | ---: | ---: | +| generic forced thin SAT | 0 | 0 | 0 | 0 | +| generic result-copy SAT | 0 | 0 | 0 | 0 | +| generic unconstrained SAT | 43,897,478 | 18,274 | 663,473 | 34,560 | +| generic backtracking SAT | 83 | 22 | 7 | 192 | +| generic root UNSAT | 0 | 0 | 0 | 0 | +| Yang–Zhang SAT, 6 variables | 10,708 | 4 | 169 | 35,233 | +| Yang–Zhang UNSAT, 6 variables | 1 | 1 | 0 | 0 | +| Yang–Zhang SAT, 12 variables | 241,688 | 8 | 3,781 | 286,073 | +| Yang–Zhang UNSAT, 12 variables | 1 | 1 | 0 | 0 | + +Solver-only and end-to-end variants have identical solver metrics. The target +unconstrained case reduces direct cell inspection by 99.96 percent. The first +root selection remains linear because the index is deliberately lazy; later +selections use the buckets. The SAT Yang–Zhang rows also reduce scans, but +their shallow search means propagation and index maintenance still dominate +elapsed time. + +## Alternating native timings + +Seven passes alternated switch-off/switch-on order. Every process was pinned to +CPU 2; metrics were disabled; each case used its standard iteration count. +Medians are milliseconds per solve and ranges contain the seven process +results. + +| Case | Off ms (range) | On ms (range) | Delta | +| --- | ---: | ---: | ---: | +| generic forced thin SAT | 3.793595 (3.716627–3.871777) | 3.800794 (3.747187–4.039952) | +0.19% | +| generic result-copy SAT | 30.110315 (29.398272–30.172475) | 29.899809 (29.757931–30.110611) | −0.70% | +| generic unconstrained SAT | 149.782460 (148.374775–153.990558) | 5.792362 (5.742785–5.852633) | −96.13% | +| generic backtracking SAT | 0.015253 (0.015157–0.016194) | 0.015368 (0.014856–0.015613) | +0.75% | +| generic root UNSAT | 17.852612 (17.536820–18.509080) | 17.854586 (17.113958–18.215488) | +0.01% | +| Yang–Zhang SAT, 6 variables, solver | 2.813235 (2.784532–3.008656) | 2.871883 (2.817281–2.904339) | +2.08% | +| Yang–Zhang UNSAT, 6 variables, solver | 0.619917 (0.617603–0.627671) | 0.633805 (0.617902–0.648096) | +2.24% | +| Yang–Zhang SAT, 6 variables, end-to-end | 3.012863 (2.965086–3.067994) | 3.013121 (3.007202–3.270830) | +0.01% | +| Yang–Zhang UNSAT, 6 variables, end-to-end | 0.672688 (0.668433–0.693132) | 0.676430 (0.667295–0.691344) | +0.56% | +| Yang–Zhang SAT, 12 variables, solver | 23.720687 (23.585753–25.196313) | 23.888030 (23.728251–24.338521) | +0.71% | +| Yang–Zhang UNSAT, 12 variables, solver | 5.008624 (4.899301–5.039353) | 4.967982 (4.894292–4.990429) | −0.81% | +| Yang–Zhang SAT, 12 variables, end-to-end | 25.404906 (25.181259–25.547235) | 25.407636 (25.120834–25.629196) | +0.01% | +| Yang–Zhang UNSAT, 12 variables, end-to-end | 5.311455 (5.270625–5.420725) | 5.341665 (5.264354–5.392123) | +0.57% | + +The intended weakly constrained case improves by 96.13 percent. The largest +observed median regression is 2.24 percent, inside the predeclared approximate +3–5 percent corpus guardrail. The Yang–Zhang results support no speedup claim: +they remain controls showing that the index does not materially harm shallow +search. + +## Resident memory + +Seven alternating single-solve processes produced these peak-RSS medians and +ranges. Allocator granularity and process noise are larger than most index +allocations. + +| Case | Off KiB (range) | On KiB (range) | +| --- | ---: | ---: | +| generic unconstrained SAT | 3,204 (3,116–3,308) | 3,144 (3,064–3,180) | +| generic result-copy SAT | 23,832 (23,784–24,000) | 23,896 (23,864–23,960) | +| generic root UNSAT | 21,756 (21,732–21,876) | 21,804 (21,780–21,896) | +| Yang–Zhang SAT, 12 variables | 5,964 (5,812–5,996) | 5,980 (5,940–6,088) | +| Yang–Zhang UNSAT, 12 variables | 2,264 (2,224–2,440) | 2,296 (2,240–2,380) | + +There is no material process-level RSS regression. The direct metric remains +the authoritative storage evidence: 34,560 bytes on unconstrained SAT, +286,073 bytes on large SAT, and zero on the root-only UNSAT controls. + +## Callgrind and Cachegrind + +Metrics-disabled whole-process Callgrind runs recorded: + +| Case | Instructions off | Instructions on | Delta | +| --- | ---: | ---: | ---: | +| generic unconstrained SAT | 1,920,147,624 | 73,933,241 | −96.15% | +| Yang–Zhang SAT, 12 variables | 307,034,463 | 309,228,803 | +0.71% | + +Before the index, `select_mrv_cell()` accounts for 1,861,178,682 instructions, +96.93 percent of the unconstrained process. Afterward, propagation is the +largest named self cost at 44.97 percent; MRV selection no longer reaches the +0.1 percent annotation threshold. Large Yang–Zhang propagation instructions +remain identical, while index construction and maintenance explain the small +whole-process increase. + +Cachegrind reported: + +| Case | Data refs off/on | D1 misses off/on | LLd misses off/on | Branch mispredicts off/on | +| --- | ---: | ---: | ---: | ---: | +| generic unconstrained SAT | 190,708,286 / 18,342,553 | 5,663,856 / 113,979 | 30,801 / 29,780 | 16,883,851 / 525,650 | +| Yang–Zhang SAT, 12 variables | 74,337,594 / 75,594,598 | 363,273 / 343,120 | 74,993 / 76,439 | 1,802,268 / 1,802,465 | + +The target improvement is reduced work volume, not a cache-rate claim. On the +large shallow-search control, data references rise by about 1.7 percent, D1 +misses fall, LLd misses rise by about 1.9 percent, and branch mispredicts are +effectively unchanged. Cachegrind is a simulated cache model. + +## Decision + +Retain the lazy packed MRV index in `wang_solve_optimized()`. It removes the +measured linear-scan bottleneck from the weakly constrained case, preserves the +same deterministic MRV choice and every non-MRV work metric on the complete +corpus, keeps native controls inside the declared timing guardrail, and uses +bounded derived storage that is absent from root-only outcomes. The reference +solver remains the unchanged linear explanation. + +This result does not justify trail compaction, `TaskPlan`, OpenMP, structural +scheduling, or any parallel speedup claim. The next separate Phase C change is +the hard-UNSAT/scaling corpus and option-matrix inventory required before +parallel design. + +## Limitations + +- The benchmark host was not frequency-isolated; timing ranges are descriptive + host evidence, not confidence intervals. +- The generic unconstrained fixture is deliberately favorable to an MRV index + and does not represent Yang–Zhang decision depth. +- Packed-word probes and cell inspections are different work units and are + reported separately rather than summed into a synthetic score. +- `mrv_index_bytes` includes both packed buckets and the dense cached-size + array; allocator overhead is not included. +- The switch-off binary contains dormant schema-v9 plumbing common to both + sides. It isolates enabling the index, not historical source changes. +- Callgrind and Cachegrind include fixture construction, verification, and + teardown; only the native timing table is solver-section elapsed time. + +## Reproduction commands + +```sh +make clean +make build/benchmarks/c/bench_solver \ + CFLAGS='-std=c17 -Wall -Wextra -Wpedantic -O2 -DWANG_OPTIMIZED_MRV_INDEX=0' +cp build/benchmarks/c/bench_solver /tmp/tiling-foundry-t92-mrv-off + +make clean +make build/benchmarks/c/bench_solver +cp build/benchmarks/c/bench_solver /tmp/tiling-foundry-t92-mrv-on + +/tmp/tiling-foundry-t92-mrv-on \ + --case generic_unconstrained_sat --solver optimized \ + --iterations 1 --metrics +``` + +Timing samples should alternate the two binaries and pin both to the same CPU: + +```sh +taskset -c 2 /tmp/tiling-foundry-t92-mrv-off \ + --case generic_unconstrained_sat --solver optimized +taskset -c 2 /tmp/tiling-foundry-t92-mrv-on \ + --case generic_unconstrained_sat --solver optimized +``` + +Profilers use one metrics-disabled solve per output: + +```sh +valgrind --tool=callgrind --error-exitcode=1 \ + --callgrind-out-file=/tmp/mrv.callgrind.out \ + /tmp/tiling-foundry-t92-mrv-on \ + --case generic_unconstrained_sat --solver optimized --iterations 1 + +valgrind --tool=cachegrind --cache-sim=yes --branch-sim=yes \ + --error-exitcode=1 --cachegrind-out-file=/tmp/mrv.cachegrind.out \ + /tmp/tiling-foundry-t92-mrv-on \ + --case generic_unconstrained_sat --solver optimized --iterations 1 +``` + +## Verification status + +The focused differential and switch-off/switch-on metrics, timing, RSS, +Callgrind, and Cachegrind comparisons above are complete. On 30 August 2026, +the retained source identities passed the complete local gate set: + +- `make check`: all 17 C test binaries, 151 Python tests, 27 technical Pages + documents plus the index, native benchmark smoke, and the cross-engine + comparison smoke; +- 262 renderer tests and the real isolated pdfLaTeX dossier smoke; +- strict GCC and Clang, ASan/UBSan/LSan, GCC static analysis, Memcheck, and the + complete Cachegrind target; +- informational coverage (C: 90.0% lines, 100.0% functions, 80.0% branches; + Python: 83%) and the deterministic 2,000-run parser fuzz smoke; +- all 25 native benchmark cases in a fresh switch-off/switch-on comparison, + with identical status and every non-MRV deterministic metric; and +- source hashes, diff whitespace, file modes, secrets, and generated-artifact + checks. + +The GitHub-only Jekyll build and the required protected-branch checks remain +remote publication evidence and must be observed on the pull request before +merge. diff --git a/docs/solver_performance_scope.md b/docs/solver_performance_scope.md index 83d85cb..4b04e45 100644 --- a/docs/solver_performance_scope.md +++ b/docs/solver_performance_scope.md @@ -44,7 +44,7 @@ Conceptually: +------------+------------+ | | reference path performance path - linear MRV derived MRV index, if measured + linear MRV measured lazy MRV index simple FIFO queue queue deduplication, if measured serial propagation TaskPlan and OpenMP, if measured simple storage optimized private storage @@ -241,10 +241,11 @@ and reference baseline, then profiled allocation, initialization, propagation, MRV, trail, rollback, and verification costs. The validated Wang core was shared before the optimized entry point diverged in private mechanisms. -Five isolated mechanisms are now retained: dynamic DFS storage, +Six isolated mechanisms are now retained: dynamic DFS storage, initial-propagation trail removal, SAT result ownership transfer, byte-wise -support aggregation, and optimized queue deduplication. Each has a dated report -with direct-work evidence and corpus-wide controls. +support aggregation, optimized queue deduplication, and a lazy private MRV +index. Each has a dated report with direct-work evidence and corpus-wide +controls. `TaskPlan` and OpenMP remain conditional on their own evidence gates. Streaming, cancellation, resource budgets, and speculative scheduling remain outside the @@ -252,7 +253,7 @@ measured serial scope. ## Current implementation status -After the first five isolated performance mechanisms: +After the first six isolated performance mechanisms: - `wang_solve_serial()` and `wang_solve_optimized()` are implemented public entry points with the same contract; @@ -302,14 +303,16 @@ After the first five isolated performance mechanisms: - the [queue and trail profile]({{ '/solver_queue_trail_profile_2026-08-20/' | relative_url }}) records the direct pending queue, repeated trail-write, Callgrind, and Cachegrind evidence. It selects queue - deduplication as the next isolated mechanism, keeps MRV indexing as the distinct - weakly constrained candidate, and rejects trail compaction for now; + deduplication as its next isolated mechanism, identifies MRV indexing as a + distinct weakly constrained candidate, and rejects trail compaction for now; - the [queue-deduplication report]({{ '/solver_queue_dedup_2026-08-20/' | relative_url }}) records the retained packed pending index, direct scheduling work, native timings, memory, and post-change profiler attribution; -- MRV indexing, trail compaction, `TaskPlan`, and operational OpenMP are not - implemented yet. +- the [MRV-index report]({{ '/solver_mrv_index_2026-08-28/' | relative_url }}) + records the retained lazy packed buckets, row-major equivalence, direct scan + and storage work, corpus controls, memory, and profiler attribution; +- trail compaction, `TaskPlan`, and operational OpenMP are not implemented. These facts distinguish the implemented serial mechanisms from the still unimplemented parallel architecture. diff --git a/include/wang/solver.h b/include/wang/solver.h index 5bcdc1a..7b51e07 100644 --- a/include/wang/solver.h +++ b/include/wang/solver.h @@ -34,6 +34,8 @@ typedef struct { uint64_t support_byte_lookups; size_t support_table_bytes; uint64_t mrv_cells_scanned; + uint64_t mrv_index_word_probes; + size_t mrv_index_bytes; uint64_t initial_trail_writes; uint64_t search_trail_writes; uint64_t initial_trail_rewrites; diff --git a/python/native/witness_adapter.py b/python/native/witness_adapter.py index b37c091..008548a 100644 --- a/python/native/witness_adapter.py +++ b/python/native/witness_adapter.py @@ -61,6 +61,8 @@ class _WangSolverMetrics(Structure): ("support_byte_lookups", c_uint64), ("support_table_bytes", c_size_t), ("mrv_cells_scanned", c_uint64), + ("mrv_index_word_probes", c_uint64), + ("mrv_index_bytes", c_size_t), ("initial_trail_writes", c_uint64), ("search_trail_writes", c_uint64), ("initial_trail_rewrites", c_uint64), diff --git a/src/solver/solver_serial.c b/src/solver/solver_serial.c index 415e618..d125a1f 100644 --- a/src/solver/solver_serial.c +++ b/src/solver/solver_serial.c @@ -15,6 +15,15 @@ #define WANG_OPTIMIZED_QUEUE_DEDUP 1 #endif +#ifndef WANG_OPTIMIZED_MRV_INDEX +#define WANG_OPTIMIZED_MRV_INDEX 1 +#endif + +enum { + MRV_MIN_DOMAIN_SIZE = 2, + MRV_BUCKET_COUNT = TILE_COUNT - MRV_MIN_DOMAIN_SIZE + 1 +}; + typedef struct { uint32_t edge_mask[DIR_COUNT][COLOR_COUNT]; uint32_t compat[DIR_COUNT][TILE_COUNT]; @@ -43,6 +52,7 @@ typedef struct { bool transfer_sat_domains; bool use_bytewise_support; bool deduplicate_queue; + bool index_mrv; } SolverMechanisms; typedef enum { @@ -86,6 +96,13 @@ typedef struct { bool has_neighbor_arcs; bool deduplicate_queue; + uint64_t *mrv_bucket_bits; + uint8_t *mrv_domain_sizes; + size_t mrv_word_count; + size_t mrv_bucket_counts[MRV_BUCKET_COUNT]; + uint32_t mrv_nonempty_buckets; + bool index_mrv; + uint32_t *best_snapshot; size_t best_resolved_count; size_t best_depth; @@ -156,6 +173,8 @@ static bool metrics_are_zero(const WangSolverMetrics *metrics) metrics->support_byte_lookups == 0 && metrics->support_table_bytes == 0 && metrics->mrv_cells_scanned == 0 && + metrics->mrv_index_word_probes == 0 && + metrics->mrv_index_bytes == 0 && metrics->initial_trail_writes == 0 && metrics->search_trail_writes == 0 && metrics->initial_trail_rewrites == 0 && @@ -241,6 +260,7 @@ static void solver_state_destroy(SolverState *state) free(state->queue); free(state->queue_pending_bits); free(state->queue_pending_counts); + free(state->mrv_bucket_bits); free(state->best_snapshot); memset(state, 0, sizeof(*state)); state->writer.fd = -1; @@ -360,6 +380,197 @@ static bool allocate_queue_dedup_index(SolverState *state) return true; } +static size_t first_set_bit_u64(uint64_t value) +{ + size_t bit = 0; + while ((value & UINT64_C(1)) == 0) { + value >>= 1; + ++bit; + } + return bit; +} + +static size_t first_set_bit_u32(uint32_t value) +{ + size_t bit = 0; + while ((value & UINT32_C(1)) == 0) { + value >>= 1; + ++bit; + } + return bit; +} + +static bool mrv_size_is_indexed(unsigned size) +{ + return size >= MRV_MIN_DOMAIN_SIZE && size <= TILE_COUNT; +} + +static size_t mrv_bucket_for_size(unsigned size) +{ + return (size_t)(size - MRV_MIN_DOMAIN_SIZE); +} + +static uint64_t *mrv_bucket_word( + SolverState *state, + size_t bucket, + size_t word +) +{ + return &state->mrv_bucket_bits[ + bucket * state->mrv_word_count + word + ]; +} + +static void mrv_index_add( + SolverState *state, + size_t cell_index, + unsigned size +) +{ + const size_t bucket = mrv_bucket_for_size(size); + uint64_t *word = mrv_bucket_word( + state, + bucket, + cell_index / 64u + ); + *word |= UINT64_C(1) << (cell_index % 64u); + ++state->mrv_bucket_counts[bucket]; + state->mrv_nonempty_buckets |= UINT32_C(1) << bucket; +} + +static bool mrv_index_move( + SolverState *state, + size_t cell_index, + uint32_t new_domain +) +{ + if (state->mrv_bucket_bits == NULL) { + return true; + } + + const uint32_t old_domain = state->domains[cell_index]; + const unsigned old_size = state->mrv_domain_sizes[cell_index]; + const uint32_t removed = old_domain & ~new_domain; + const uint32_t added = new_domain & ~old_domain; + unsigned new_size; + if (added == 0) { + const unsigned removed_count = domain_popcount(removed); + if (removed_count > old_size) { + return false; + } + new_size = old_size - removed_count; + } else if (removed == 0) { + const unsigned added_count = domain_popcount(added); + if (old_size > TILE_COUNT - added_count) { + return false; + } + new_size = old_size + added_count; + } else { + new_size = domain_popcount(new_domain); + } + if (old_size == new_size) { + return true; + } + + if (mrv_size_is_indexed(old_size)) { + const size_t old_bucket = mrv_bucket_for_size(old_size); + uint64_t *old_word = mrv_bucket_word( + state, + old_bucket, + cell_index / 64u + ); + const uint64_t bit = UINT64_C(1) << (cell_index % 64u); + if ((*old_word & bit) == 0 || + state->mrv_bucket_counts[old_bucket] == 0) { + return false; + } + } + if (mrv_size_is_indexed(new_size)) { + const size_t new_bucket = mrv_bucket_for_size(new_size); + const uint64_t new_word = *mrv_bucket_word( + state, + new_bucket, + cell_index / 64u + ); + if ((new_word & (UINT64_C(1) << (cell_index % 64u))) != 0) { + return false; + } + } + + if (mrv_size_is_indexed(old_size)) { + const size_t old_bucket = mrv_bucket_for_size(old_size); + uint64_t *old_word = mrv_bucket_word( + state, + old_bucket, + cell_index / 64u + ); + *old_word &= ~(UINT64_C(1) << (cell_index % 64u)); + --state->mrv_bucket_counts[old_bucket]; + if (state->mrv_bucket_counts[old_bucket] == 0) { + state->mrv_nonempty_buckets &= + ~(UINT32_C(1) << old_bucket); + } + } + if (mrv_size_is_indexed(new_size)) { + mrv_index_add(state, cell_index, new_size); + } + state->mrv_domain_sizes[cell_index] = (uint8_t)new_size; + return true; +} + +static bool allocate_mrv_index(SolverState *state) +{ + if (!state->index_mrv || + state->resolved_count == state->active_count) { + return true; + } + + state->mrv_word_count = state->cell_count / 64u + + (state->cell_count % 64u != 0 ? 1u : 0u); + size_t bucket_word_count; + size_t bucket_bytes; + size_t size_bytes; + if (!checked_mul_size( + MRV_BUCKET_COUNT, + state->mrv_word_count, + &bucket_word_count + ) || + !checked_mul_size( + bucket_word_count, + sizeof(*state->mrv_bucket_bits), + &bucket_bytes + ) || + !checked_mul_size( + state->cell_count, + sizeof(*state->mrv_domain_sizes), + &size_bytes + ) || + bucket_bytes > SIZE_MAX - size_bytes) { + return false; + } + + const size_t total_bytes = bucket_bytes + size_bytes; + state->mrv_bucket_bits = calloc(1, total_bytes); + if (state->mrv_bucket_bits == NULL) { + return false; + } + state->mrv_domain_sizes = + (uint8_t *)state->mrv_bucket_bits + bucket_bytes; + + for (size_t cell = 0; cell < state->cell_count; ++cell) { + const unsigned size = domain_popcount(state->domains[cell]); + state->mrv_domain_sizes[cell] = (uint8_t)size; + if (state->region->cells[cell].active && + mrv_size_is_indexed(size)) { + mrv_index_add(state, cell, size); + } + } + if (state->collect_metrics) { + state->metrics.mrv_index_bytes = total_bytes; + } + return true; +} + static bool queue_cell_is_pending( const SolverState *state, size_t cell_index @@ -518,6 +729,10 @@ static bool restrict_domain( } } + if (!mrv_index_move(state, cell_index, new_domain)) { + return false; + } + if (domain_is_singleton(old_domain) && !domain_is_singleton(new_domain)) { --state->resolved_count; @@ -561,12 +776,20 @@ static bool restrict_domain( return true; } -static void rollback_to(SolverState *state, size_t mark) +static bool rollback_to(SolverState *state, size_t mark) { while (state->trail_count > mark) { const TrailEntry entry = state->trail[--state->trail_count]; const uint32_t current = state->domains[entry.cell_index]; + if (!mrv_index_move( + state, + entry.cell_index, + entry.old_domain + )) { + return false; + } + if (domain_is_singleton(current) && !domain_is_singleton(entry.old_domain)) { --state->resolved_count; @@ -577,6 +800,7 @@ static void rollback_to(SolverState *state, size_t mark) state->domains[entry.cell_index] = entry.old_domain; } + return true; } static size_t neighbor_index( @@ -777,6 +1001,38 @@ static bool record_failed_leaf( static size_t select_mrv_cell(SolverState *state) { + if (state->mrv_bucket_bits != NULL) { + if (state->mrv_nonempty_buckets == 0) { + return SIZE_MAX; + } + + const size_t bucket = first_set_bit_u32( + state->mrv_nonempty_buckets + ); + for (size_t word = 0; word < state->mrv_word_count; ++word) { + if (state->collect_metrics) { + ++state->metrics.mrv_index_word_probes; + } + const uint64_t candidates = *mrv_bucket_word( + state, + bucket, + word + ); + if (candidates != 0) { + const size_t selected = word * 64u + + first_set_bit_u64(candidates); + if (selected >= state->cell_count) { + return SIZE_MAX; + } + if (state->collect_metrics) { + ++state->metrics.mrv_cells_scanned; + } + return selected; + } + } + return SIZE_MAX; + } + size_t selected = SIZE_MAX; unsigned best_size = TILE_COUNT + 1u; @@ -945,7 +1201,9 @@ static WangSolveStatus search( break; } - rollback_to(state, entry_mark); + if (!rollback_to(state, entry_mark)) { + break; + } if (state->trace_events) { state->trace_change_mark = state->trace_search_base + entry_mark; @@ -1003,7 +1261,7 @@ static WangSolveStatus search( WANG_TRACE_REASON_DECISION, branch_depth )) { - rollback_to(state, mark); + (void)rollback_to(state, mark); break; } @@ -1016,7 +1274,7 @@ static WangSolveStatus search( ); if (propagated == PROPAGATE_ERROR) { - rollback_to(state, mark); + (void)rollback_to(state, mark); break; } @@ -1056,7 +1314,7 @@ static WangSolveStatus search( conflict_cell, branch_depth )) { - rollback_to(state, mark); + (void)rollback_to(state, mark); break; } } else { @@ -1068,6 +1326,12 @@ static WangSolveStatus search( break; } + if (state->index_mrv && + state->mrv_bucket_bits == NULL && + !allocate_mrv_index(state)) { + (void)rollback_to(state, mark); + break; + } const size_t child_cell = select_mrv_cell(state); if (child_cell == SIZE_MAX || !search_stack_push(&stack, (SearchFrame) { @@ -1075,14 +1339,16 @@ static WangSolveStatus search( .candidates = state->domains[child_cell], .entry_mark = mark, })) { - rollback_to(state, mark); + (void)rollback_to(state, mark); break; } note_search_stack_capacity(state, &stack); continue; } - rollback_to(state, mark); + if (!rollback_to(state, mark)) { + break; + } if (state->trace_events) { state->trace_change_mark = state->trace_search_base + mark; solver_event_trace_record( @@ -1361,6 +1627,7 @@ static WangSolveStatus solve_wang_core( (options->flags & WANG_SOLVE_CAPTURE_UNSAT_SNAPSHOT) != 0; state.record_trail = mechanisms.record_initial_trail; state.deduplicate_queue = mechanisms.deduplicate_queue; + state.index_mrv = mechanisms.index_mrv; build_solver_tables(&state.tables); if (!solver_tables_are_valid(&state.tables)) { return WANG_SOLVE_ERROR; @@ -1620,6 +1887,7 @@ WangSolveStatus wang_solve_serial( .transfer_sat_domains = false, .use_bytewise_support = false, .deduplicate_queue = false, + .index_mrv = false, }, NULL, NULL @@ -1642,6 +1910,7 @@ WangSolveStatus wang_solve_optimized( .transfer_sat_domains = true, .use_bytewise_support = true, .deduplicate_queue = WANG_OPTIMIZED_QUEUE_DEDUP != 0, + .index_mrv = WANG_OPTIMIZED_MRV_INDEX != 0, }, NULL, NULL @@ -1675,6 +1944,7 @@ WangSolveStatus wang_solve_serial_traced( .transfer_sat_domains = false, .use_bytewise_support = false, .deduplicate_queue = false, + .index_mrv = false, }, trace_options, &out_result->trace @@ -1701,6 +1971,7 @@ WangSolveStatus wang_solve_optimized_traced( .transfer_sat_domains = true, .use_bytewise_support = true, .deduplicate_queue = WANG_OPTIMIZED_QUEUE_DEDUP != 0, + .index_mrv = WANG_OPTIMIZED_MRV_INDEX != 0, }, trace_options, &out_result->trace diff --git a/tests/c/test_solver.c b/tests/c/test_solver.c index f1a6a04..d91e86a 100644 --- a/tests/c/test_solver.c +++ b/tests/c/test_solver.c @@ -32,6 +32,8 @@ static bool metrics_are_zero(const WangSolverMetrics *metrics) metrics->support_byte_lookups == 0 && metrics->support_table_bytes == 0 && metrics->mrv_cells_scanned == 0 && + metrics->mrv_index_word_probes == 0 && + metrics->mrv_index_bytes == 0 && metrics->initial_trail_writes == 0 && metrics->search_trail_writes == 0 && metrics->enqueue_attempts == 0 && diff --git a/tests/c/test_solver_differential.c b/tests/c/test_solver_differential.c index 561c178..f18b0ba 100644 --- a/tests/c/test_solver_differential.c +++ b/tests/c/test_solver_differential.c @@ -412,6 +412,12 @@ static void test_generic_backtracking_case(void) ); assert(reference_metrics.backtracks > 0); assert(optimized_metrics.backtracks == reference_metrics.backtracks); + assert(reference_metrics.mrv_index_word_probes == 0); + assert(reference_metrics.mrv_index_bytes == 0); + assert(reference_metrics.mrv_cells_scanned == 83); + assert(optimized_metrics.mrv_index_word_probes == 7); + assert(optimized_metrics.mrv_index_bytes == 192); + assert(optimized_metrics.mrv_cells_scanned == 22); assert(reference_metrics.initial_trail_writes > 0); assert(optimized_metrics.initial_trail_writes == 0); assert(reference_metrics.search_trail_writes > 0); @@ -523,15 +529,39 @@ static bool boolean_oracle(const Cm13Formula *formula) static void assert_yang_zhang_pair(Cm13Formula *formula) { YangZhangReduction reduction = {0}; + const WangSolveStatus expected = boolean_oracle(formula) + ? WANG_SOLVE_SAT + : WANG_SOLVE_UNSAT; assert(yang_zhang_build(formula, &reduction)); assert_semantic_pair( &reduction.region, NULL, NULL, - boolean_oracle(formula) ? WANG_SOLVE_SAT : WANG_SOLVE_UNSAT, + expected, NULL, NULL ); + + const WangSolverOptions options = { + .flags = WANG_SOLVE_COLLECT_METRICS, + }; + WangSolverMetrics reference_metrics = {0}; + WangSolverMetrics optimized_metrics = {0}; + assert_semantic_pair( + &reduction.region, + &options, + &options, + expected, + &reference_metrics, + &optimized_metrics + ); + if (expected == WANG_SOLVE_UNSAT && + optimized_metrics.dfs_nodes == 1) { + assert(reference_metrics.mrv_index_word_probes == 0); + assert(optimized_metrics.mrv_index_word_probes == 0); + assert(reference_metrics.mrv_index_bytes == 0); + assert(optimized_metrics.mrv_index_bytes == 0); + } yang_zhang_reduction_destroy(&reduction); } @@ -595,6 +625,10 @@ static void test_unsat_diagnostic_modes(void) assert(optimized_metrics.enqueue_attempts == 0); assert(reference_metrics.queue_dedup_index_bytes == 0); assert(optimized_metrics.queue_dedup_index_bytes == 0); + assert(reference_metrics.mrv_index_word_probes == 0); + assert(optimized_metrics.mrv_index_word_probes == 0); + assert(reference_metrics.mrv_index_bytes == 0); + assert(optimized_metrics.mrv_index_bytes == 0); char reference_path[] = "/tmp/wang-reference-diff-XXXXXX"; char optimized_path[] = "/tmp/wang-optimized-diff-XXXXXX"; @@ -663,6 +697,10 @@ static void test_queue_dedup_index_skips_no_arc_case(void) assert(optimized_metrics.queue_peak == 1); assert(reference_metrics.queue_dedup_index_bytes == 0); assert(optimized_metrics.queue_dedup_index_bytes == 0); + assert(reference_metrics.mrv_index_word_probes == 0); + assert(optimized_metrics.mrv_index_word_probes == 0); + assert(reference_metrics.mrv_index_bytes == 0); + assert(optimized_metrics.mrv_index_bytes == 0); region_destroy(®ion); } @@ -706,6 +744,14 @@ static void assert_invalid_contract(SolveFunction solve) assert(solve(®ion, NULL, &result) == WANG_SOLVE_ERROR); result.metrics.support_table_bytes = 0; + result.metrics.mrv_index_word_probes = 1; + assert(solve(®ion, NULL, &result) == WANG_SOLVE_ERROR); + result.metrics.mrv_index_word_probes = 0; + + result.metrics.mrv_index_bytes = 1; + assert(solve(®ion, NULL, &result) == WANG_SOLVE_ERROR); + result.metrics.mrv_index_bytes = 0; + result.metrics.enqueue_attempts = 1; assert(solve(®ion, NULL, &result) == WANG_SOLVE_ERROR); result.metrics.enqueue_attempts = 0;