diff --git a/Cargo.lock b/Cargo.lock index ee4c9b8..64dcc57 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -20,6 +20,15 @@ dependencies = [ "cc", ] +[[package]] +name = "android_system_properties" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "819e7219dbd41043ac279b19830f2efc897156490d7fd6ea916720117ee66311" +dependencies = [ + "libc", +] + [[package]] name = "anes" version = "0.1.6" @@ -32,6 +41,12 @@ version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "940b3a0ca603d1eade50a4846a2afffd5ef57a9feac2c0e2ec2e14f9ead76000" +[[package]] +name = "anyhow" +version = "1.0.104" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470" + [[package]] name = "autocfg" version = "1.5.1" @@ -47,7 +62,7 @@ dependencies = [ "bitflags", "cexpr", "clang-sys", - "itertools", + "itertools 0.13.0", "log", "prettyplease", "proc-macro2", @@ -72,6 +87,8 @@ dependencies = [ "optimal-branching", "rayon", "rustc-hash", + "rustsat", + "rustsat-cadical", "serde", "serde_json", "smallvec", @@ -104,6 +121,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e228eec9be7c17ccb640b59b36a5cd805ea2a564a4c5e162c2f659fea30d3b96" dependencies = [ "find-msvc-tools", + "jobserver", + "libc", "shlex 2.0.1", ] @@ -122,6 +141,19 @@ version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" +[[package]] +name = "chrono" +version = "0.4.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1aa79e62e7697b8e29b513a68abacf485adcd1fe8284a4316c5ae868e6633327" +dependencies = [ + "iana-time-zone", + "js-sys", + "num-traits", + "wasm-bindgen", + "windows-link", +] + [[package]] name = "ciborium" version = "0.2.2" @@ -194,6 +226,22 @@ dependencies = [ "cc", ] +[[package]] +name = "core-foundation-sys" +version = "0.8.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" + +[[package]] +name = "cpu-time" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e9e393a7668fe1fad3075085b86c781883000b4ede868f43627b34a87c8b7ded" +dependencies = [ + "libc", + "winapi", +] + [[package]] name = "criterion" version = "0.8.2" @@ -206,7 +254,7 @@ dependencies = [ "ciborium", "clap", "criterion-plot", - "itertools", + "itertools 0.13.0", "num-traits", "oorandom", "page_size", @@ -226,7 +274,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d8d80a2f4f5b554395e47b5d8305bc3d27813bacb73493eb1001e8f76dae29ea" dependencies = [ "cast", - "itertools", + "itertools 0.13.0", ] [[package]] @@ -266,6 +314,22 @@ version = "1.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "91622ff5e7162018101f2fea40d6ebf4a78bbe5a49736a2020649edf9693679e" +[[package]] +name = "errno" +version = "0.3.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" +dependencies = [ + "libc", + "windows-sys", +] + +[[package]] +name = "fastrand" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da7c62ceae207dd37ea5b845da6a0696c799f85e97da1ab5b7910be3c1c80223" + [[package]] name = "find-msvc-tools" version = "0.1.9" @@ -310,10 +374,21 @@ checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd" dependencies = [ "cfg-if", "libc", - "r-efi", + "r-efi 5.3.0", "wasip2", ] +[[package]] +name = "getrandom" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "300e883d756b2e4ec94e02791f39b04b522276138852cfc41d9fb7e904106099" +dependencies = [ + "cfg-if", + "libc", + "r-efi 6.0.0", +] + [[package]] name = "glob" version = "0.3.3" @@ -361,6 +436,30 @@ dependencies = [ "cmake", ] +[[package]] +name = "iana-time-zone" +version = "0.1.65" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e31bc9ad994ba00e440a8aa5c9ef0ec67d5cb5e5cb0cc7f8b744a35b389cc470" +dependencies = [ + "android_system_properties", + "core-foundation-sys", + "iana-time-zone-haiku", + "js-sys", + "log", + "wasm-bindgen", + "windows-core", +] + +[[package]] +name = "iana-time-zone-haiku" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f31827a206f56af32e590ba56d5d2d085f558508192593743f16b2306495269f" +dependencies = [ + "cc", +] + [[package]] name = "itertools" version = "0.13.0" @@ -370,20 +469,40 @@ dependencies = [ "either", ] +[[package]] +name = "itertools" +version = "0.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b192c782037fadd9cfa75548310488aabdbf3d2da73885b31bd0abd03351285" +dependencies = [ + "either", +] + [[package]] name = "itoa" version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" +[[package]] +name = "jobserver" +version = "0.1.35" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1c00acbd29eabad4a2392fa0e921c874934dbbf4194312ad20f04a0ed67a3cb3" +dependencies = [ + "getrandom 0.4.3", + "libc", +] + [[package]] name = "js-sys" -version = "0.3.103" +version = "0.3.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "53b44bfcdb3f8d5837a46dae1ca9660a837176eee74a28b229bc626816589102" +checksum = "142bc4740e452c1e57ade0cbc129f139c9093e354346f0872ef985f4f5cf5f11" dependencies = [ "cfg-if", "futures-util", + "once_cell", "wasm-bindgen", ] @@ -403,6 +522,12 @@ dependencies = [ "windows-link", ] +[[package]] +name = "linux-raw-sys" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53" + [[package]] name = "log" version = "0.4.33" @@ -550,6 +675,12 @@ version = "5.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f" +[[package]] +name = "r-efi" +version = "6.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" + [[package]] name = "rand" version = "0.9.4" @@ -576,7 +707,7 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" dependencies = [ - "getrandom", + "getrandom 0.3.4", ] [[package]] @@ -634,6 +765,48 @@ version = "2.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6b1e7f9a428571be2dc5bc0505c13fb6bf936822b894ec87abf8a08a4e51742d" +[[package]] +name = "rustix" +version = "1.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6fe4565b9518b83ef4f91bb47ce29620ca828bd32cb7e408f0062e9930ba190" +dependencies = [ + "bitflags", + "errno", + "libc", + "linux-raw-sys", + "windows-sys", +] + +[[package]] +name = "rustsat" +version = "0.7.5" +source = "git+https://github.com/isPANN/rustsat.git?rev=24c202c205513b93bcc111510c3245b1ee0b6fe8#24c202c205513b93bcc111510c3245b1ee0b6fe8" +dependencies = [ + "anyhow", + "cpu-time", + "itertools 0.14.0", + "nom", + "rustc-hash", + "tempfile", + "thiserror", + "web-time", +] + +[[package]] +name = "rustsat-cadical" +version = "0.7.5" +source = "git+https://github.com/isPANN/rustsat.git?rev=24c202c205513b93bcc111510c3245b1ee0b6fe8#24c202c205513b93bcc111510c3245b1ee0b6fe8" +dependencies = [ + "anyhow", + "bindgen", + "cc", + "chrono", + "glob", + "rustsat", + "thiserror", +] + [[package]] name = "rustversion" version = "1.0.22" @@ -736,6 +909,19 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "tempfile" +version = "3.27.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd" +dependencies = [ + "fastrand", + "getrandom 0.4.3", + "once_cell", + "rustix", + "windows-sys", +] + [[package]] name = "thiserror" version = "2.0.18" @@ -784,18 +970,18 @@ dependencies = [ [[package]] name = "wasip2" -version = "1.0.4+wasi-0.2.12" +version = "1.0.3+wasi-0.2.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487" +checksum = "20064672db26d7cdc89c7798c48a0fdfac8213434a1186e5ef29fd560ae223d6" dependencies = [ "wit-bindgen", ] [[package]] name = "wasm-bindgen" -version = "0.2.126" +version = "0.2.122" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4b067c0c11094aef6b7a801c1e34a26affafdf3d051dba08456b868789aaf9a4" +checksum = "3ed04576f974d2b2fba0f38c51dbc5518011e38c36bf1143164be765528fd409" dependencies = [ "cfg-if", "once_cell", @@ -806,9 +992,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.126" +version = "0.2.122" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "167ce5e579f6bcf889c4f7175a8a5a585de84e8ff93976ce393efa5f2837aab1" +checksum = "916151b09da36bd82f6615cbf3a419e2f0ba23a03c6160e8e92eb6bd4aa1dec6" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -816,9 +1002,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.126" +version = "0.2.122" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f3997c7839262f4ef12cf90b818d6340c18e80f263f1a94bf157d0ec4420380e" +checksum = "299047362ccbfce148b67ab7e73349f77748e00c8296f9542adfad2ad82c5c5e" dependencies = [ "bumpalo", "proc-macro2", @@ -829,18 +1015,28 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.126" +version = "0.2.122" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc1b4cb0cc549fcf58d7dfc081778139b3d283a081644e833e84682ad71cea24" +checksum = "9a929b2c61f11ba3e9bc35b50c1f25cb38e0e892c0c231ae2b8cf78d5dad4437" dependencies = [ "unicode-ident", ] [[package]] name = "web-sys" -version = "0.3.103" +version = "0.3.99" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d621441cfc37b84979402712047321980c178f299193a3589d05b99e8763436" +dependencies = [ + "js-sys", + "wasm-bindgen", +] + +[[package]] +name = "web-time" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8622dcb61c0bcc9fffa6938bed81210af2da9a7e4a1a834b2e37a59b6dfb6141" +checksum = "5a6580f308b1fad9207618087a65c04e7a10bc77e02c8e84e9b00dd4b12fa0bb" dependencies = [ "js-sys", "wasm-bindgen", @@ -887,12 +1083,65 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +[[package]] +name = "windows-core" +version = "0.62.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b8e83a14d34d0623b51dce9581199302a221863196a1dde71a7663a4c2be9deb" +dependencies = [ + "windows-implement", + "windows-interface", + "windows-link", + "windows-result", + "windows-strings", +] + +[[package]] +name = "windows-implement" +version = "0.60.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "053e2e040ab57b9dc951b72c264860db7eb3b0200ba345b4e4c3b14f67855ddf" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "windows-interface" +version = "0.59.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f316c4a2570ba26bbec722032c4099d8c8bc095efccdc15688708623367e358" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "windows-link" version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" +[[package]] +name = "windows-result" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7781fa89eaf60850ac3d2da7af8e5242a5ea78d1a11c49bf2910bb5a73853eb5" +dependencies = [ + "windows-link", +] + +[[package]] +name = "windows-strings" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7837d08f69c77cf6b07689544538e017c1bfcf57e34b4c0ff58e6c2cd3b37091" +dependencies = [ + "windows-link", +] + [[package]] name = "windows-sys" version = "0.61.2" diff --git a/Cargo.toml b/Cargo.toml index db97513..7b934d3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -18,6 +18,10 @@ thiserror = "2" serde = { version = "1", features = ["derive"] } serde_json = "1" rayon = { version = "1", optional = true } +rustsat = { git = "https://github.com/isPANN/rustsat.git", rev = "24c202c205513b93bcc111510c3245b1ee0b6fe8" } +# Pin the small wrapper patch that removes propagation debug output and exposes +# CaDiCaL's native learned-clause maintenance schedule. +rustsat-cadical = { git = "https://github.com/isPANN/rustsat.git", rev = "24c202c205513b93bcc111510c3245b1ee0b6fe8", features = ["quiet"] } [features] default = [] diff --git a/benchmarks/cnc/README.md b/benchmarks/cnc/README.md index 56e751e..cb9ba27 100644 --- a/benchmarks/cnc/README.md +++ b/benchmarks/cnc/README.md @@ -59,16 +59,65 @@ DIMACS. The `.csp` format retains each ` : ` line as one relation tensor; it is intended for transfer tests where the structure-aware cuber must see semantics that a flattened CNF does not expose. +Add `--propagation cdcl --propagate-cnf INSTANCE.cnf` to retain native regions +while using one persistent CaDiCaL 2.2.1 instance. Each branch query is expressed +using only the current cube's decision literals as assumptions and invokes +CaDiCaL's standard assumptions-propagation path. Native implications are not +reintroduced as artificial assumptions: CaDiCaL reconstructs their reasons, +BCP runs to a fixpoint, a conflict is analyzed, and globally valid learned +clauses remain available to later queries. Because this propagation entry point +sits outside CaDiCaL's normal search loop, the wrapper invokes CaDiCaL's own +scheduled learned-clause reduction after conflicts. CaDiCaL stops after applying +the assumptions. The cuber never invokes `solve`/`solve_assumps`, never searches +beyond the branch assumptions, and never publishes a SAT model. + +With `--propagation cdcl`, the same propagation-and-learning path is also used +for the many hypothetical branches evaluated by the region-rule optimizer. +Those clauses are sound consequences of the base CNF, so they may safely help +later candidates and committed nodes. + +`--propagation hybrid --propagate-cnf INSTANCE.cnf` is the production hybrid: +region construction, feasibility probes, and the many hypothetical +branch-candidate evaluations use the native CT engine, while the persistent +CaDiCaL companion is called only after a selected branch is applied. This keeps +candidate scoring on CT while retaining conflict learning across committed +branches. + +Before descending, the cuber converts the optimizer's potentially overlapping +DNF cover into an equivalent pairwise-disjoint DNF. Consequently the emitted +frontier is a true CnC partition rather than a collection that can submit the +same residual assignment through multiple branches. + +An open decision-only cube is submitted to Kissat only after the online cutoff +fires. Kissat is the conquer solver and performs unrestricted modern CDCL. +A cuber-side propagation conflict closes that branch without submission. In +streaming `--solve-cnf` mode, SAT from any Kissat worker stops cubing and the +other in-flight workers through the shared first-answer signal. Global UNSAT is +reported only after cubing finishes and every submitted cube is UNSAT (except +for a root contradiction proved by propagation). + +For DIMACS input, `--propagate-cnf` is optional; in streaming mode, +`--solve-cnf` is also reused automatically. The native and CNF files must +describe the same formula, with native variables occupying the corresponding +leading DIMACS ids. The trace records the CDCL search mode, and stderr reports +internal conflicts/decisions/propagations, cumulative learned clauses, and the +current redundant-clause database size. + Both `--branch-solver` and `--measure` are mandatory so an artifact cannot silently inherit a changed default. `--branch-solver tail-greedy` starts from the full-row branches and rejects any GreedyMerge whose measured reduction is worse than the weakest initial child. Measures are selected as `vars`, `tensors`, or `hard-tensors`. -Trace schema v2 records the selected `measure` and `rule_diagnostics` for every -structure-aware branch: +The trace records propagation/CDCL provenance, the selected `measure`, and +`rule_diagnostics` for every structure-aware branch: the focus variable, region tensor/variable/boundary counts, joined and probe-surviving row counts, closed-region status, branching vector, and gamma. +`optimized_rule_clauses` is the cover to which those optimizer diagnostics +belong; `rule_clauses` is the disjoint CnC partition actually traversed, with +`rule_partition_sources` linking each partition branch back to its optimizer +clause. Trace producers and analysis tools use this current format directly; +older layouts are not accepted. It declares `search_semantics: "sat-decision"`. Ordinary open-region rules are configuration covers; closed regions may select one representative witness, so the full frontier is satisfiability-preserving but is neither a model-space diff --git a/benchmarks/cnc/trace_mechanism.py b/benchmarks/cnc/trace_mechanism.py index 70761f8..70f94d9 100644 --- a/benchmarks/cnc/trace_mechanism.py +++ b/benchmarks/cnc/trace_mechanism.py @@ -1,4 +1,4 @@ -"""Validate and summarize cnc_cuber mechanism traces (schema v2). +"""Validate and summarize current cnc_cuber mechanism traces. This deliberately aggregates raw local evidence without claiming that local gamma predicts conquer cost. Join the output to per-cube residual/conquer data @@ -169,10 +169,18 @@ def _clauses_may_overlap(left: dict[str, Any], right: dict[str, Any]) -> bool: def _validate_record(record: dict[str, Any], index: int) -> None: - if record.get("schema_version") != 2: - raise TraceError(f"record {index}: expected schema_version 2") if record.get("search_semantics") != "sat-decision": raise TraceError(f"record {index}: expected sat-decision semantics") + propagation = record.get("propagation") + cdcl_mode = record.get("cdcl_mode") + if propagation not in {"ct", "cdcl", "hybrid"}: + raise TraceError(f"record {index}: invalid propagation provenance") + if (propagation, cdcl_mode) not in { + ("ct", "off"), + ("cdcl", "branch-learning"), + ("hybrid", "branch-learning"), + }: + raise TraceError(f"record {index}: invalid CDCL search provenance") if record.get("selector") not in (None, "region", "structure-blind"): raise TraceError(f"record {index}: invalid selector provenance") if record.get("branch_solver") not in (None, "greedy", "tail-greedy", "naive"): @@ -202,6 +210,34 @@ def _validate_record(record: dict[str, Any], index: int) -> None: raise TraceError(f"record {index}: invalid rule clause mask/value") if value & ~mask: raise TraceError(f"record {index}: rule clause value exceeds its mask") + optimized_clauses = record.get("optimized_rule_clauses") + if not isinstance(optimized_clauses, list) or not all( + isinstance(clause, dict) for clause in optimized_clauses + ): + raise TraceError(f"record {index}: optimized_rule_clauses must be an array") + for clause in optimized_clauses: + mask = clause.get("mask") + value = clause.get("value") + if ( + type(mask) is not int + or type(value) is not int + or mask < 0 + or value < 0 + or value & ~mask + ): + raise TraceError(f"record {index}: invalid optimized rule clause") + partition_sources = record.get("rule_partition_sources") + if ( + not isinstance(partition_sources, list) + or len(partition_sources) != len(clauses) + or any( + type(source) is not int + or source < 0 + or source >= len(optimized_clauses) + for source in partition_sources + ) + ): + raise TraceError(f"record {index}: invalid rule_partition_sources") diagnostics = record.get("rule_diagnostics") if diagnostics is None: @@ -252,7 +288,7 @@ def _validate_record(record: dict[str, Any], index: int) -> None: if semantics == "cover": if closed or feasible_rows == 0 or record["kind"] != "branch": raise TraceError(f"record {index}: inconsistent cover semantics") - if len(clauses) != len(vector) or not clauses: + if len(optimized_clauses) != len(vector) or not optimized_clauses: raise TraceError(f"record {index}: selected branch/vector count mismatch") _validate_gamma(gamma, vector, "gamma", index) elif semantics == "closed-witness": @@ -260,7 +296,7 @@ def _validate_record(record: dict[str, Any], index: int) -> None: not closed or feasible_rows == 0 or record["kind"] != "branch" - or len(clauses) != 1 + or len(optimized_clauses) != 1 or vector or gamma != 1.0 ): @@ -268,7 +304,7 @@ def _validate_record(record: dict[str, Any], index: int) -> None: elif ( feasible_rows != 0 or record["kind"] != "refuted" - or clauses + or optimized_clauses or vector or gamma is not None ): @@ -360,14 +396,18 @@ def summarize( if unverified: raise TraceError(f"cover not verified at nodes {unverified[:8]}") - selected_branches = sum(len(record.get("rule_clauses", [])) for record, _ in rule_nodes) + selected_branches = sum( + len(record["optimized_rule_clauses"]) + for record, _ in rule_nodes + ) selected_literals = sum( int(clause["mask"]).bit_count() for record, _ in rule_nodes - for clause in record.get("rule_clauses", []) + for clause in record["optimized_rule_clauses"] ) single_branch_nodes = sum( - len(record.get("rule_clauses", [])) == 1 for record, _ in rule_nodes + len(record["optimized_rule_clauses"]) == 1 + for record, _ in rule_nodes ) sibling_pairs = 0 potentially_overlapping_pairs = 0 @@ -446,8 +486,6 @@ def summarize( } return { - "schema_version": 1, - "trace_schema_version": 2, "nodes": len(records), "rule_nodes": len(rule_nodes), "cover_nodes": len(cover_nodes), @@ -614,24 +652,26 @@ def link_conquer( "rule_diagnostics.branching_vector", int(node["node_id"]), ) + partition_sources = node["rule_partition_sources"] + source_index = partition_sources[child_index] if not vector and diagnostics.get("rule_semantics") == "closed-witness": - if child_index != 0: + if source_index != 0: raise TraceError( f"cube {cube_index}: closed witness has a nonzero child_index" ) selected_reductions.append(0.0) - elif child_index < 0 or child_index >= len(vector): + elif source_index < 0 or source_index >= len(vector): raise TraceError( - f"cube {cube_index}: child_index exceeds branching vector" + f"cube {cube_index}: partition source exceeds branching vector" ) else: - selected_reductions.append(vector[child_index]) + selected_reductions.append(vector[source_index]) replay = diagnostics.get("same_state_replay") if isinstance(replay, dict) and selected is not None and selected > 0: naive = _finite_gamma(replay["naive"].get("gamma")) if naive is not None and naive > 0: gamma_advantage_naive += math.log(naive) - math.log(selected) - if len(node.get("rule_clauses", [])) == 1: + if len(node["optimized_rule_clauses"]) == 1: single_branch_nodes += 1 root_node, root_child_index = path_edges[0] root_reduction = selected_reductions[0] diff --git a/src/adapter.rs b/src/adapter.rs index 42ca0ce..1be8bf9 100644 --- a/src/adapter.rs +++ b/src/adapter.rs @@ -23,6 +23,7 @@ use optimal_branching_core::{ IPSolver, LPSolver, Measure as ObMeasure, NaiveBranch, OptimalBranchingResult, }; +use crate::cdcl::CdclPropagator; use crate::ct::{RSparseBitSet, TableMasks}; use crate::domain::DomainMask; use crate::measure::{measure_core, Measure}; @@ -81,13 +82,20 @@ pub(crate) fn with_measure_scratch( /// A clone-cheap view of the SAT problem at one search node, sized to feed /// `optimal_branching_rule`. Cloning bumps the network `Arc` refcount and -/// deep-copies only `doms`. CT tables are shared via `masks` so `apply_branch` -/// can propagate with CT via the thread-local measure scratch. +/// deep-copies only `doms`. Candidate propagation uses either the optional +/// shared CDCL engine or CT via the thread-local measure scratch. #[derive(Clone)] pub struct RuleProblem { pub cn: Arc, pub masks: Arc>, pub doms: Vec, + /// Optional flattened-CNF propagation engine. Candidate evaluation uses + /// assumption-only BCP, so cloned rule problems share one clause database + /// while keeping their own projected native-domain snapshots. + pub cdcl: Option, + /// Actual cube decisions leading to this node. Native implications in + /// `doms` are intentionally excluded from the CaDiCaL assumption prefix. + pub decisions: Vec<(usize, bool)>, } impl RuleProblem { @@ -96,7 +104,19 @@ impl RuleProblem { masks: Arc>, doms: Vec, ) -> RuleProblem { - RuleProblem { cn, masks, doms } + RuleProblem { + cn, + masks, + doms, + cdcl: None, + decisions: Vec::new(), + } + } + + pub fn with_cdcl(mut self, cdcl: CdclPropagator, decisions: Vec<(usize, bool)>) -> RuleProblem { + self.cdcl = Some(cdcl); + self.decisions = decisions; + self } } @@ -111,13 +131,11 @@ impl BranchAndReduceProblem for RuleProblem { self.doms.iter().all(|d| d.is_fixed()) } - /// Apply `clause` over `variables` on the thread-local measure scratch (the - /// node's live CT store, at base), run CT to a fixpoint, snapshot the - /// resulting domains as the returned sub-problem, and restore the scratch to - /// base. Behavior-identical to the old clone-doms + rescan path (CT and rescan - /// reach the same GAC fixpoint) but ~2-3x faster and allocation-free. - /// Precondition (ob-core guarantee): called only single-level from the root, - /// with the scratch primed by `with_measure_scratch`. + /// Apply `clause` over `variables`, propagate with assumption-only CDCL when + /// configured, otherwise use the node's live CT store in the thread-local + /// measure scratch. Return the projected domain snapshot without changing + /// the base node. Precondition (ob-core guarantee): called only single-level + /// from the root, with CT scratch primed by `with_measure_scratch`. /// /// No per-node memo here: `GreedyMerge` (the only rule solver that re-evaluates /// the same clause) now memoizes `size_reduction` by `(mask, val)` in ob-core, @@ -125,15 +143,22 @@ impl BranchAndReduceProblem for RuleProblem { /// would never be hit. `IPSolver`/`LPSolver`/`NaiveBranch` evaluate each /// candidate clause exactly once, so they never needed one. fn apply_branch(&self, clause: &Clause, variables: &[usize]) -> (RuleProblem, f64) { - let snapshot = MEASURE_SCRATCH.with(|s| { - let s = &mut *s.borrow_mut(); - apply_branch_fresh(&self.cn, &self.masks, s, clause, variables) - }); + let snapshot = match &self.cdcl { + Some(cdcl) => cdcl + .propagate_clause(&self.doms, &self.decisions, clause, variables) + .expect("CDCL candidate propagation failed"), + None => MEASURE_SCRATCH.with(|s| { + let s = &mut *s.borrow_mut(); + apply_branch_fresh(&self.cn, &self.masks, s, clause, variables) + }), + }; ( RuleProblem { cn: Arc::clone(&self.cn), masks: Arc::clone(&self.masks), doms: snapshot, + cdcl: self.cdcl.clone(), + decisions: self.decisions.clone(), }, 0.0, ) @@ -226,7 +251,10 @@ impl BranchSolver { #[cfg(test)] mod tests { + use std::io::Cursor; + use super::*; + use crate::cdcl::CdclPropagator; use crate::ct::build_tables; use crate::network::setup_problem; use crate::problem::SolverBuffer; @@ -240,7 +268,7 @@ mod tests { setup_problem(3, vec![vec![0, 1], vec![1, 2]], vec![or2.clone(), or2]) } - /// Build a `RuleProblem` at `doms` with CT masks (apply_branch uses CT scratch). + /// Build a CT-scored `RuleProblem` at `doms`. fn rule_problem(cn: &ConstraintNetwork, doms: Vec) -> RuleProblem { let (masks, _tables) = build_tables(cn); RuleProblem::new(Arc::new(cn.clone()), Arc::new(masks), doms) @@ -305,6 +333,36 @@ mod tests { assert!(Arc::ptr_eq(&p.cn, &sub.cn)); } + #[test] + fn cdcl_apply_branch_matches_ct_and_is_order_independent_on_cnf() { + let cn = or_chain(); + let base = vec![DomainMask::BOTH; 3]; + let (masks, mut tables) = build_tables(&cn); + let masks = Arc::new(masks); + let mut buf = SolverBuffer::new(&cn); + let mut trail = Trail::new(); + let ct = RuleProblem::new(Arc::new(cn.clone()), Arc::clone(&masks), base.clone()); + let cdcl = CdclPropagator::from_dimacs( + &mut Cursor::new(b"p cnf 3 2\n1 2 0\n2 3 0\n"), + vec![0, 1, 2], + ) + .unwrap(); + let hybrid = RuleProblem::new(Arc::new(cn), Arc::clone(&masks), base.clone()) + .with_cdcl(cdcl, Vec::new()); + let variables = [0, 1, 2]; + let first = Clause::new(0b001, 0); // x0=0 => x1=1 + let other = Clause::new(0b100, 0); // x2=0 => x1=1 + + let ct_result = with_measure_scratch(&base, &mut tables, &mut buf, &mut trail, || { + ct.apply_branch(&first, &variables).0.doms + }); + let hybrid_first = hybrid.apply_branch(&first, &variables).0.doms; + let _ = hybrid.apply_branch(&other, &variables); + let hybrid_repeated = hybrid.apply_branch(&first, &variables).0.doms; + assert_eq!(hybrid_first, ct_result); + assert_eq!(hybrid_repeated, hybrid_first); + } + #[test] fn is_empty_tracks_unfixed_vars() { let cn = or_chain(); diff --git a/src/bin/cnc_cuber.rs b/src/bin/cnc_cuber.rs index 8dd488a..60f0265 100644 --- a/src/bin/cnc_cuber.rs +++ b/src/bin/cnc_cuber.rs @@ -10,12 +10,14 @@ use std::num::NonZeroUsize; use std::path::{Path, PathBuf}; use boolean_inference::adapter::BranchSolver; +use boolean_inference::cdcl::CdclPropagator; use boolean_inference::circuit::network_from_circuit_sat; use boolean_inference::conquer::{ConquerResult, StreamingConquer}; use boolean_inference::csp::network_from_csp; use boolean_inference::cube::{ - generate_cubes_with_cutoff, generate_cubes_with_cutoff_trace, CubeCutoff, CubeNodeKind, - CubeNodeTrace, CubeRefutationReason, + generate_cubes_configured, generate_cubes_configured_with_trace, CdclIntegrationMode, + CncSatPolicy, CubeCdclOptions, CubeCutoff, CubeGenerationOptions, CubeNodeKind, CubeNodeTrace, + CubeRefutationReason, }; use boolean_inference::dimacs::network_from_dimacs; use boolean_inference::measure::Measure; @@ -30,9 +32,9 @@ const USAGE: &str = (-o | --solve-cnf --kissat --workers ) \ --branch-solver \ --measure \ + [--propagation ] [--propagate-cnf ] \ [--selector ] \ [--max-rows ] [--trace ] [--trace-replay]"; -const SOLVED: &str = "streaming-conquer-found-sat"; #[derive(Clone, Copy, Debug)] enum SelectorKind { @@ -40,6 +42,41 @@ enum SelectorKind { StructureBlind, } +#[derive(Clone, Copy, Debug)] +enum PropagationKind { + Ct, + Cdcl, + Hybrid, +} + +impl PropagationKind { + fn parse(value: &str) -> Result { + match value { + "ct" => Ok(Self::Ct), + "cdcl" => Ok(Self::Cdcl), + "hybrid" => Ok(Self::Hybrid), + _ => Err(format!( + "invalid --propagation value: {value}; expected ct, cdcl, or hybrid" + )), + } + } + + fn label(self) -> &'static str { + match self { + Self::Ct => "ct", + Self::Cdcl => "cdcl", + Self::Hybrid => "hybrid", + } + } +} + +fn cdcl_mode_label(propagation: PropagationKind) -> &'static str { + match propagation { + PropagationKind::Ct => "off", + PropagationKind::Cdcl | PropagationKind::Hybrid => "branch-learning", + } +} + impl SelectorKind { fn parse(value: &str) -> Result { match value { @@ -91,12 +128,14 @@ struct Args { input: PathBuf, output: Option, solve_cnf: Option, + propagate_cnf: Option, kissat: Option, workers: Option, cutoff: CubeCutoff, selector: SelectorKind, branch_solver: BranchSolverKind, measure: Measure, + propagation: PropagationKind, max_rows: usize, trace: Option, trace_replay: bool, @@ -104,7 +143,7 @@ struct Args { enum Command { Help, - Run(Args), + Run(Box), } fn take_value(args: &[String], index: &mut usize, option: &str) -> Result { @@ -119,6 +158,7 @@ fn parse_args() -> Result { let mut input = None; let mut output = None; let mut solve_cnf = None; + let mut propagate_cnf = None; let mut kissat = None; let mut workers = None; let mut cutoff_vars = None; @@ -127,6 +167,7 @@ fn parse_args() -> Result { let mut selector = SelectorKind::Region; let mut branch_solver = None; let mut measure = None; + let mut propagation = PropagationKind::Ct; let mut trace = None; let mut trace_replay = false; let mut i = 0usize; @@ -154,6 +195,7 @@ fn parse_args() -> Result { } "-o" => output = Some(take_value(&raw, &mut i, "-o")?), "--solve-cnf" => solve_cnf = Some(take_value(&raw, &mut i, "--solve-cnf")?), + "--propagate-cnf" => propagate_cnf = Some(take_value(&raw, &mut i, "--propagate-cnf")?), "--kissat" => kissat = Some(take_value(&raw, &mut i, "--kissat")?), "--workers" => { let value = take_value(&raw, &mut i, "--workers")?; @@ -180,6 +222,9 @@ fn parse_args() -> Result { "--measure" => { measure = Some(Measure::parse(&take_value(&raw, &mut i, "--measure")?)?); } + "--propagation" => { + propagation = PropagationKind::parse(&take_value(&raw, &mut i, "--propagation")?)?; + } "--max-rows" => { let value = take_value(&raw, &mut i, "--max-rows")?; max_rows = value @@ -217,10 +262,22 @@ fn parse_args() -> Result { if trace_replay && matches!(selector, SelectorKind::StructureBlind) { return Err("--trace-replay requires --selector region".to_string()); } - Ok(Command::Run(Args { - input: PathBuf::from(input.ok_or_else(|| "missing input instance".to_string())?), + let input = PathBuf::from(input.ok_or_else(|| "missing input instance".to_string())?); + if matches!(propagation, PropagationKind::Cdcl | PropagationKind::Hybrid) + && solve_cnf.is_none() + && propagate_cnf.is_none() + && input.extension().and_then(|extension| extension.to_str()) != Some("cnf") + { + return Err(format!( + "--propagation {} requires --propagate-cnf, --solve-cnf, or a DIMACS input instance", + propagation.label() + )); + } + Ok(Command::Run(Box::new(Args { + input, output: output.map(PathBuf::from), solve_cnf: solve_cnf.map(PathBuf::from), + propagate_cnf: propagate_cnf.map(PathBuf::from), kissat: kissat.map(PathBuf::from), workers, cutoff, @@ -231,10 +288,11 @@ fn parse_args() -> Result { measure: measure.ok_or_else(|| { "missing --measure (experiments must select it explicitly)".to_string() })?, + propagation, max_rows, trace: trace.map(PathBuf::from), trace_replay, - })) + }))) } fn load_network(path: &Path) -> Result { @@ -277,9 +335,11 @@ fn refutation_reason(reason: CubeRefutationReason) -> &'static str { CubeRefutationReason::RootPropagation => "root-propagation-contradiction", CubeRefutationReason::SelectorNoFeasibleConfig => "selector-no-feasible-config", CubeRefutationReason::BranchPropagation => "branch-propagation-contradiction", + CubeRefutationReason::CdclPropagationConflict => "cdcl-propagation-conflict", } } +#[allow(clippy::too_many_arguments)] fn write_trace_node( writer: &mut dyn Write, node: CubeNodeTrace, @@ -287,6 +347,8 @@ fn write_trace_node( selector: &str, branch_solver: &str, measure: &str, + propagation: &str, + cdcl_mode: &str, input_kind: &str, ) -> Result<(), String> { let literals: Vec = node @@ -311,6 +373,11 @@ fn write_trace_node( .iter() .map(|clause| serde_json::json!({"mask": clause.mask, "value": clause.value})) .collect(); + let optimized_clauses: Vec<_> = node + .optimized_clauses + .iter() + .map(|clause| serde_json::json!({"mask": clause.mask, "value": clause.value})) + .collect(); let rule_diagnostics = node.rule_diagnostics.as_ref().map(|diagnostics| { let rule_semantics = if diagnostics.feasible_rows == 0 { "local-refutation" @@ -356,11 +423,12 @@ fn write_trace_node( }) }); let record = serde_json::json!({ - "schema_version": 2, "search_semantics": "sat-decision", "selector": selector, "branch_solver": branch_solver, "measure": measure, + "propagation": propagation, + "cdcl_mode": cdcl_mode, "input_kind": input_kind, "node_id": node.node_id, "parent_id": node.parent_id, @@ -374,7 +442,9 @@ fn write_trace_node( "freevars": node.freevars, "rule_diagnostics": rule_diagnostics, "rule_variables": variables, + "optimized_rule_clauses": optimized_clauses, "rule_clauses": clauses, + "rule_partition_sources": node.partition_sources, }); serde_json::to_writer(&mut *writer, &record) .map_err(|error| format!("serialize trace: {error}"))?; @@ -458,12 +528,16 @@ fn run(args: Args) -> Result { freevars: nvars, rule_diagnostics: None, variables: Vec::new(), + optimized_clauses: Vec::new(), clauses: Vec::new(), + partition_sources: Vec::new(), }, &new_to_orig, args.selector.label(), args.branch_solver.label(), args.measure.label(), + args.propagation.label(), + cdcl_mode_label(args.propagation), input_kind, )?; trace_writer @@ -473,11 +547,14 @@ fn run(args: Args) -> Result { writer.flush().map_err(|e| format!("flush output: {e}"))?; eprintln!( "status=UNSAT_AT_ROOT cubes=0 refuted=1 sat_leaves=0 cutoff={:?} \ - selector={} branch_solver={} measure={} max_rows={}", + selector={} branch_solver={} measure={} propagation={} cdcl_mode={} \ + max_rows={}", args.cutoff, args.selector.label(), args.branch_solver.label(), args.measure.label(), + args.propagation.label(), + cdcl_mode_label(args.propagation), args.max_rows ); if let Some(conquer) = conquer.take() { @@ -490,6 +567,27 @@ fn run(args: Args) -> Result { } }; let root_unfixed = problem.count_unfixed(); + let cdcl = match args.propagation { + PropagationKind::Ct => None, + PropagationKind::Cdcl | PropagationKind::Hybrid => { + let cnf = args + .propagate_cnf + .as_ref() + .or(args.solve_cnf.as_ref()) + .unwrap_or(&args.input); + Some(CdclPropagator::from_dimacs_path(cnf, new_to_orig.clone())?) + } + }; + let cdcl_integration = match args.propagation { + PropagationKind::Hybrid => CdclIntegrationMode::HybridCtCandidates, + PropagationKind::Ct | PropagationKind::Cdcl => CdclIntegrationMode::FullPropagation, + }; + let sat_policy = if conquer.is_some() { + CncSatPolicy::StopDecision + } else { + CncSatPolicy::CompleteFrontier + }; + let termination = conquer.as_ref().map(StreamingConquer::termination_signal); let mut emitted = 0usize; let mut min_remaining = usize::MAX; @@ -518,19 +616,12 @@ fn run(args: Args) -> Result { if leaf_sat { if let Some(conquer) = conquer.as_ref() { conquer.mark_sat(); - return Err(SOLVED.to_string()); } + return Ok(()); } let remaining = nvars - cube.sigma_all; - let stopped = match args.cutoff { - CubeCutoff::RemainingVars(n) => remaining < n.get(), - CubeCutoff::CcDifficulty(threshold) => { - (cube.sigma_dec as u128).pow(2) * (cube.sigma_all as u128) - > threshold * (nvars as u128) - } - }; - if !leaf_sat && !stopped { + if !args.cutoff.stops(cube.sigma_dec, cube.sigma_all, remaining) { return Err(format!( "internal cutoff error: emitted cube does not satisfy {:?}", args.cutoff @@ -548,7 +639,7 @@ fn run(args: Args) -> Result { .submit(literals) .map_err(|error| error.to_string())? { - return Err(SOLVED.to_string()); + return Ok(()); } } else { writer @@ -567,13 +658,22 @@ fn run(args: Args) -> Result { max_remaining = max_remaining.max(remaining); Ok(()) }; + let generation_options = CubeGenerationOptions { + cutoff: args.cutoff, + cdcl: cdcl.as_ref().map(|cdcl| CubeCdclOptions { + propagator: cdcl.clone(), + integration: cdcl_integration, + }), + sat_policy, + termination, + }; let generated = match trace_writer.as_mut() { - Some(trace_writer) => generate_cubes_with_cutoff_trace( + Some(trace_writer) => generate_cubes_configured_with_trace( &mut problem, selector, args.measure, &solver, - args.cutoff, + generation_options, &mut emit, |node| { write_trace_node( @@ -583,23 +683,27 @@ fn run(args: Args) -> Result { args.selector.label(), args.branch_solver.label(), args.measure.label(), + args.propagation.label(), + cdcl_mode_label(args.propagation), input_kind, ) }, ), - None => generate_cubes_with_cutoff( + None => generate_cubes_configured( &mut problem, selector, args.measure, &solver, - args.cutoff, + generation_options, &mut emit, ), }; - let stopped_on_sat = matches!(&generated, Err(error) if error == SOLVED); + let stopped_during_generation = generated.as_ref().is_ok_and(|stats| stats.stopped_early); + let cdcl_stats = cdcl.as_ref().map(CdclPropagator::stats); + let stopped_on_sat = stopped_during_generation; let stats = match generated { + Ok(stats) if stats.stopped_early => None, Ok(stats) => Some(stats), - Err(error) if error == SOLVED => None, Err(error) => { if let Some(conquer) = conquer.take() { let _ = conquer.finish(false); @@ -622,7 +726,8 @@ fn run(args: Args) -> Result { if let Some(stats) = stats { eprintln!( "status=OK cubes={} refuted={} sat_leaves={} visited={} cutoff={:?} \ - root_unfixed={} remaining_range={} selector={} branch_solver={} measure={} max_rows={}", + root_unfixed={} remaining_range={} selector={} branch_solver={} measure={} \ + propagation={} cdcl_mode={} max_rows={}", stats.cubes, stats.refuted, stats.sat_leaves, @@ -633,6 +738,8 @@ fn run(args: Args) -> Result { args.selector.label(), args.branch_solver.label(), args.measure.label(), + args.propagation.label(), + cdcl_mode_label(args.propagation), args.max_rows ); let expected = stats.cubes + stats.sat_leaves; @@ -644,12 +751,31 @@ fn run(args: Args) -> Result { } } else { eprintln!( - "status=SAT_EARLY cubes_submitted={} cutoff={:?} selector={} branch_solver={} measure={}", + "status=SAT_EARLY cubes_submitted={} cutoff={:?} selector={} branch_solver={} \ + measure={} propagation={} cdcl_mode={}", emitted, args.cutoff, args.selector.label(), args.branch_solver.label(), - args.measure.label() + args.measure.label(), + args.propagation.label(), + cdcl_mode_label(args.propagation) + ); + } + if let Some(stats) = cdcl_stats { + eprintln!( + "cdcl propagation_calls={} propagation_conflicts={} assumption_literals={} \ + full_search_calls={} conflicts={} decisions={} propagations={} \ + learned_total={} redundant_current={}", + stats.propagation_calls, + stats.propagation_conflicts, + stats.assumption_literals, + stats.full_search_calls, + stats.conflicts, + stats.decisions, + stats.propagations, + stats.total_learned_clauses, + stats.current_redundant_clauses ); } if let Some(conquer) = conquer.take() { @@ -682,7 +808,7 @@ fn run(args: Args) -> Result { fn main() { match parse_args() { Ok(Command::Help) => println!("{USAGE}"), - Ok(Command::Run(args)) => match run(args) { + Ok(Command::Run(args)) => match run(*args) { Ok(0) => {} Ok(code) => std::process::exit(code), Err(message) => { diff --git a/src/cdcl.rs b/src/cdcl.rs new file mode 100644 index 0000000..3dfc253 --- /dev/null +++ b/src/cdcl.rs @@ -0,0 +1,419 @@ +//! Persistent CDCL propagation for cube generation. +//! +//! The cuber owns one CaDiCaL instance for the whole run. Every query applies +//! the current cube decisions as assumptions and invokes CaDiCaL's standard +//! assumptions-propagation entry point. Native implications are deliberately +//! not promoted to assumptions: CaDiCaL must reconstruct their reasons so +//! conflict analysis learns clauses over the actual cube decisions. The entry +//! point performs BCP and conflict analysis, so globally valid learned clauses +//! remain in the solver for later nodes. It stops after the assumptions: the +//! cuber never calls `solve` or lets CaDiCaL make search decisions beyond the +//! cube. + +use std::cell::{Cell, RefCell}; +use std::io::BufRead; +use std::path::Path; +use std::rc::Rc; + +use optimal_branching_core::Clause as BranchClause; +use rustsat::instances::SatInstance; +use rustsat::solvers::{FreezeVar, GetInternalStats, Learn, Propagate, Solve}; +use rustsat::types::{Lit, TernaryVal, Var}; +use rustsat_cadical::{CaDiCaL, Config}; + +use crate::domain::DomainMask; + +/// Aggregate counters from the persistent CaDiCaL instance. +#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)] +pub struct CdclStats { + /// Number of assumption-propagation queries issued by the cuber. + pub propagation_calls: u64, + /// Queries whose BCP/conflict-analysis result refuted the assumptions. + pub propagation_conflicts: u64, + /// Total number of literals supplied as assumptions across all queries. + pub assumption_literals: u64, + /// Full CDCL searches started inside the cuber. This is an architectural + /// invariant and is always zero. + pub full_search_calls: u64, + pub conflicts: u64, + pub decisions: u64, + pub propagations: u64, + /// Clauses reported by CaDiCaL's learner callback over the whole run. + pub total_learned_clauses: u64, + /// Redundant clauses currently retained in CaDiCaL's clause database. + pub current_redundant_clauses: usize, +} + +/// Cloneable handle to one persistent, single-threaded CaDiCaL instance. +/// +/// Region scoring and cube generation are single-threaded. Clones therefore +/// share the solver through `Rc>`; every learned clause immediately +/// benefits later committed branches and, when enabled, later candidate probes. +#[derive(Clone)] +pub struct CdclPropagator { + inner: Rc, +} + +struct CdclInner { + solver: RefCell>, + native_to_cnf: Vec, + cnf_to_native: Vec>, + propagation_calls: Cell, + propagation_conflicts: Cell, + assumption_literals: Cell, + total_learned_clauses: Rc>, +} + +impl CdclPropagator { + /// Load a DIMACS formula. `native_to_cnf[v]` is the zero-based DIMACS + /// variable corresponding to compressed native variable `v`. + pub fn from_dimacs_path(path: &Path, native_to_cnf: Vec) -> Result { + let instance = SatInstance::from_dimacs_path(path) + .map_err(|error| format!("parse CDCL CNF {}: {error}", path.display()))?; + Self::from_instance(instance, native_to_cnf) + } + + /// Reader form used by tests and embedders. + pub fn from_dimacs( + reader: &mut R, + native_to_cnf: Vec, + ) -> Result { + let instance = + SatInstance::from_dimacs(reader).map_err(|error| format!("parse CDCL CNF: {error}"))?; + Self::from_instance(instance, native_to_cnf) + } + + fn from_instance(instance: SatInstance, native_to_cnf: Vec) -> Result { + let formula_vars = instance.max_var().map_or(0, |var| var.idx() + 1); + let mapped_vars = native_to_cnf.iter().copied().max().map_or(0, |var| var + 1); + let n_cnf_vars = formula_vars.max(mapped_vars); + let mut seen = vec![false; n_cnf_vars]; + for &cnf_var in &native_to_cnf { + if cnf_var > Var::MAX_IDX as usize { + return Err(format!( + "flattened CNF variable {} exceeds the RustSAT limit", + cnf_var + 1 + )); + } + if std::mem::replace(&mut seen[cnf_var], true) { + return Err(format!( + "two native variables map to flattened CNF variable {}", + cnf_var + 1 + )); + } + } + + let mut solver = CaDiCaL::default(); + solver + .set_configuration(Config::Default) + .map_err(|error| format!("configure CaDiCaL: {error}"))?; + if n_cnf_vars > 0 { + solver + .reserve(Var::new((n_cnf_vars - 1) as u32)) + .map_err(|error| format!("reserve CaDiCaL variables: {error}"))?; + } + for clause in instance.cnf() { + solver + .add_clause_ref(clause) + .map_err(|error| format!("load CaDiCaL clause: {error}"))?; + } + // Native variables recur as assumptions and must keep stable external + // identities across CaDiCaL inprocessing rounds. + for &cnf_var in &native_to_cnf { + solver + .freeze_var(Var::new(cnf_var as u32)) + .map_err(|error| format!("freeze CaDiCaL variable {}: {error}", cnf_var + 1))?; + } + let total_learned_clauses = Rc::new(Cell::new(0u64)); + let learner_count = Rc::clone(&total_learned_clauses); + solver.attach_learner( + move |_| learner_count.set(learner_count.get().saturating_add(1)), + n_cnf_vars, + ); + let mut cnf_to_native = vec![None; n_cnf_vars]; + for (native, &cnf_var) in native_to_cnf.iter().enumerate() { + cnf_to_native[cnf_var] = Some(native); + } + + Ok(Self { + inner: Rc::new(CdclInner { + solver: RefCell::new(solver), + native_to_cnf, + cnf_to_native, + propagation_calls: Cell::new(0), + propagation_conflicts: Cell::new(0), + assumption_literals: Cell::new(0), + total_learned_clauses, + }), + }) + } + + /// Propagate a hypothetical optimal-branching clause from `base`. + pub fn propagate_clause( + &self, + base: &[DomainMask], + prefix: &[(usize, bool)], + clause: &BranchClause, + variables: &[usize], + ) -> Result, String> { + let mut decisions = Vec::with_capacity(prefix.len() + clause.mask.count_ones() as usize); + decisions.extend_from_slice(prefix); + for (index, &var) in variables.iter().enumerate() { + if (clause.mask >> index) & 1 != 0 { + decisions.push((var, (clause.val >> index) & 1 != 0)); + } + } + self.propagate_decisions(base, &decisions) + } + + /// Propagate the explicit cube `decisions` and overlay the resulting native + /// implications on `base`. + /// + /// Only `decisions` are passed to CaDiCaL as assumptions. Fixed values in + /// `base` are a projection maintained by native propagation and are kept in + /// the returned snapshot, but are not turned into artificial decision + /// levels. This distinction is essential for useful first-UIP learning. + /// + /// A conflict is represented by the existing solver convention + /// `snapshot[0] == DomainMask::NONE`. CaDiCaL's propagation call analyzes + /// such a conflict before returning, retaining the learned clause globally. + pub fn propagate_decisions( + &self, + base: &[DomainMask], + decisions: &[(usize, bool)], + ) -> Result, String> { + if base.len() != self.inner.native_to_cnf.len() { + return Err(format!( + "native domain length {} does not match CDCL map length {}", + base.len(), + self.inner.native_to_cnf.len() + )); + } + + let mut snapshot = base.to_vec(); + for &(var, value) in decisions { + let requested = fixed_domain(value); + match snapshot.get_mut(var) { + Some(domain) if *domain == DomainMask::BOTH || *domain == requested => { + *domain = requested; + } + Some(_) => { + mark_conflict(&mut snapshot); + return Ok(snapshot); + } + None => return Err(format!("native branch variable {var} is out of range")), + } + } + + let assumptions = assumptions_from_decisions(&self.inner, decisions)?; + self.inner + .propagation_calls + .set(self.inner.propagation_calls.get() + 1); + self.inner.assumption_literals.set( + self.inner.assumption_literals.get() + + u64::try_from(assumptions.len()).unwrap_or(u64::MAX), + ); + + let mut solver = self.inner.solver.borrow_mut(); + let result = solver + .propagate(&assumptions, false) + .map_err(|error| format!("CaDiCaL branch propagation failed: {error}"))?; + if result.conflict { + self.inner + .propagation_conflicts + .set(self.inner.propagation_conflicts.get() + 1); + // Assumption propagation analyzes conflicts outside CaDiCaL's + // normal search loop. Run its own scheduled reduction policy at + // this reset-to-root boundary so retained clauses stay managed. + solver.maintain_learned_clauses(); + mark_conflict(&mut snapshot); + return Ok(snapshot); + } + + // `propagated` contains the assumption trail. `current_lit_val` also + // exposes root-fixed projected variables that predate the first + // assumption and therefore may not appear in that returned suffix. + for (native, &cnf_var) in self.inner.native_to_cnf.iter().enumerate() { + let literal = Var::new(cnf_var as u32).pos_lit(); + let implied = match solver.current_lit_val(literal) { + TernaryVal::True => Some(DomainMask::D1), + TernaryVal::False => Some(DomainMask::D0), + TernaryVal::DontCare => None, + }; + if let Some(implied) = implied { + let domain = &mut snapshot[native]; + if *domain == DomainMask::BOTH || *domain == implied { + *domain = implied; + } else { + mark_conflict(&mut snapshot); + return Ok(snapshot); + } + } + } + + for literal in result.propagated { + let Some(Some(native)) = self.inner.cnf_to_native.get(literal.vidx()) else { + continue; + }; + let implied = fixed_domain(literal.is_pos()); + let domain = &mut snapshot[*native]; + if *domain == DomainMask::BOTH || *domain == implied { + *domain = implied; + } else { + mark_conflict(&mut snapshot); + break; + } + } + Ok(snapshot) + } + + pub fn stats(&self) -> CdclStats { + let solver = self.inner.solver.borrow(); + CdclStats { + propagation_calls: self.inner.propagation_calls.get(), + propagation_conflicts: self.inner.propagation_conflicts.get(), + assumption_literals: self.inner.assumption_literals.get(), + full_search_calls: 0, + conflicts: solver.conflicts().try_into().unwrap_or(u64::MAX), + decisions: solver.decisions().try_into().unwrap_or(u64::MAX), + propagations: solver.propagations().try_into().unwrap_or(u64::MAX), + total_learned_clauses: self.inner.total_learned_clauses.get(), + current_redundant_clauses: solver.get_redundant().max(0) as usize, + } + } +} + +fn assumptions_from_decisions( + inner: &CdclInner, + decisions: &[(usize, bool)], +) -> Result, String> { + let mut assumptions = Vec::with_capacity(decisions.len()); + for &(native, value) in decisions { + if native >= inner.native_to_cnf.len() { + return Err(format!("native decision variable {native} is out of range")); + } + let cnf_var: u32 = inner.native_to_cnf[native] + .try_into() + .map_err(|_| "flattened CNF variable exceeds u32".to_string())?; + assumptions.push(Lit::new(cnf_var, !value)); + } + Ok(assumptions) +} + +fn mark_conflict(doms: &mut [DomainMask]) { + if let Some(sentinel) = doms.first_mut() { + *sentinel = DomainMask::NONE; + } +} + +#[inline] +fn fixed_domain(value: bool) -> DomainMask { + if value { + DomainMask::D1 + } else { + DomainMask::D0 + } +} + +#[cfg(test)] +mod tests { + use std::io::Cursor; + + use super::*; + + fn solver(cnf: &str, variables: usize) -> CdclPropagator { + CdclPropagator::from_dimacs(&mut Cursor::new(cnf.as_bytes()), (0..variables).collect()) + .unwrap() + } + + #[test] + fn projects_gate_implications_to_native_domains() { + // z <-> (a AND b): + // (¬z∨a)(¬z∨b)(z∨¬a∨¬b) + let cdcl = solver("p cnf 3 3\n-3 1 0\n-3 2 0\n3 -1 -2 0\n", 3); + let base = vec![DomainMask::BOTH; 3]; + + let z_true = cdcl.propagate_decisions(&base, &[(2, true)]).unwrap(); + assert_eq!(z_true, vec![DomainMask::D1, DomainMask::D1, DomainMask::D1]); + + let a_false = cdcl.propagate_decisions(&base, &[(0, false)]).unwrap(); + assert_eq!(a_false[0], DomainMask::D0); + assert_eq!(a_false[2], DomainMask::D0); + } + + #[test] + fn repeated_probes_do_not_leak_assumptions() { + let cdcl = solver("p cnf 2 1\n1 2 0\n", 2); + let base = vec![DomainMask::BOTH; 2]; + let x0_false = cdcl.propagate_decisions(&base, &[(0, false)]).unwrap(); + assert_eq!(x0_false, vec![DomainMask::D0, DomainMask::D1]); + + let x0_true = cdcl.propagate_decisions(&base, &[(0, true)]).unwrap(); + assert_eq!(x0_true[0], DomainMask::D1); + assert_eq!(x0_true[1], DomainMask::BOTH); + } + + #[test] + fn contradictory_assumptions_return_the_native_sentinel() { + let cdcl = solver("p cnf 1 1\n1 0\n", 1); + let result = cdcl + .propagate_decisions(&[DomainMask::BOTH], &[(0, false)]) + .unwrap(); + assert_eq!(result, vec![DomainMask::NONE]); + } + + #[test] + fn auxiliary_implications_are_projected_but_auxiliaries_stay_hidden() { + // Native variables are a,b,c (CNF 1,2,3); variable 4 is a Tseitin + // auxiliary. a -> aux -> c, while b is unrelated. + let cdcl = solver("p cnf 4 4\n-1 4 0\n1 -4 0\n-4 3 0\n4 -3 0\n", 3); + let result = cdcl + .propagate_decisions(&[DomainMask::BOTH; 3], &[(0, true)]) + .unwrap(); + assert_eq!(result[0], DomainMask::D1); + assert_eq!(result[1], DomainMask::BOTH); + assert_eq!(result[2], DomainMask::D1); + } + + #[test] + fn propagation_conflict_learns_for_later_parent_bcp() { + // Resolving the three clauses shows that the formula entails a. Root + // BCP initially cannot see it. Under a=0 it forces both b and c before + // conflicting, producing the learned unit a. + let cdcl = solver("p cnf 3 3\n1 2 0\n1 3 0\n1 -2 -3 0\n", 3); + let parent = vec![DomainMask::BOTH; 3]; + assert_eq!(cdcl.propagate_decisions(&parent, &[]).unwrap(), parent); + + let child = cdcl.propagate_decisions(&parent, &[(0, false)]).unwrap(); + assert_eq!(child[0], DomainMask::NONE); + + let after = cdcl.propagate_decisions(&parent, &[]).unwrap(); + assert_eq!(after[0], DomainMask::D1); + let stats = cdcl.stats(); + assert_eq!(stats.propagation_conflicts, 1); + assert_eq!(stats.full_search_calls, 0); + assert!(stats.conflicts >= 1); + assert!(stats.total_learned_clauses >= 1); + } + + #[test] + fn open_formula_is_not_solved_by_the_cuber_cdcl() { + // No root implication. A full CDCL solve could return SAT immediately, + // but branch propagation must leave the formula open. + let cdcl = solver("p cnf 3 2\n1 2 0\n-1 2 0\n", 3); + let base = vec![DomainMask::BOTH; 3]; + assert_eq!(cdcl.propagate_decisions(&base, &[]).unwrap(), base); + let stats = cdcl.stats(); + assert_eq!(stats.full_search_calls, 0); + assert_eq!(stats.propagation_calls, 1); + } + + #[test] + fn projected_implications_are_not_reintroduced_as_assumptions() { + let cdcl = solver("p cnf 3 2\n-1 2 0\n-2 3 0\n", 3); + let projected = vec![DomainMask::D1, DomainMask::D1, DomainMask::D1]; + let result = cdcl.propagate_decisions(&projected, &[(0, true)]).unwrap(); + assert_eq!(result, projected); + assert_eq!(cdcl.stats().assumption_literals, 1); + } +} diff --git a/src/conquer.rs b/src/conquer.rs index 09d2eda..c53588c 100644 --- a/src/conquer.rs +++ b/src/conquer.rs @@ -4,10 +4,12 @@ use std::fs; use std::io::{BufRead, BufReader, Write}; use std::path::{Path, PathBuf}; use std::process::{Command, Stdio}; -use std::sync::atomic::{AtomicBool, AtomicUsize, Ordering}; +use std::sync::atomic::{AtomicUsize, Ordering}; use std::sync::{mpsc, Arc, Mutex}; use std::thread::{self, JoinHandle}; +use crate::termination::TerminationSignal; + #[derive(Debug, thiserror::Error)] pub enum ConquerError { #[error("read CNF {path}: {source}")] @@ -86,7 +88,7 @@ pub struct ConquerSummary { } struct Shared { - stopped: AtomicBool, + stopped: TerminationSignal, submitted: AtomicUsize, sat: AtomicUsize, unsat: AtomicUsize, @@ -97,7 +99,7 @@ struct Shared { impl Shared { fn new() -> Self { Self { - stopped: AtomicBool::new(false), + stopped: TerminationSignal::new(), submitted: AtomicUsize::new(0), sat: AtomicUsize::new(0), unsat: AtomicUsize::new(0), @@ -140,7 +142,7 @@ impl StreamingConquer { /// Submit one open cube. Returns `false` once another cube has proved SAT. pub fn submit(&self, cube: Vec) -> Result { - if self.shared.stopped.load(Ordering::Acquire) { + if self.shared.stopped.is_requested() { return Ok(false); } let sent = self @@ -149,27 +151,36 @@ impl StreamingConquer { .ok_or(ConquerError::Disconnected)? .send(cube); if sent.is_err() { - return if self.shared.stopped.load(Ordering::Acquire) { + return if self.shared.stopped.is_requested() { Ok(false) } else { Err(ConquerError::Disconnected) }; } self.shared.submitted.fetch_add(1, Ordering::Relaxed); - Ok(!self.shared.stopped.load(Ordering::Acquire)) + Ok(!self.shared.stopped.is_requested()) + } + + /// Clone the global first-answer signal so the cuber can stop at its own + /// safe boundaries when a conquer worker wins. + pub fn termination_signal(&self) -> TerminationSignal { + self.shared.stopped.clone() } /// Record a satisfying leaf found by the cuber itself. pub fn mark_sat(&self) { self.shared.sat.fetch_add(1, Ordering::Relaxed); - self.shared.stopped.store(true, Ordering::Release); + self.shared.stopped.request(); + } + + /// Stop all conquer workers after an integrated solver found a model. + pub fn mark_sat_with_witness(&self, witness: String) { + *self.shared.witness.lock().expect("witness lock") = Some(witness); + self.mark_sat(); } pub fn finish(mut self, cubing_complete: bool) -> Result { - self.sender.take(); - for worker in self.workers.drain(..) { - worker.join().map_err(|_| ConquerError::WorkerPanicked)?; - } + self.close_and_join(false)?; let submitted = self.shared.submitted.load(Ordering::Relaxed); let sat = self.shared.sat.load(Ordering::Relaxed); let unsat = self.shared.unsat.load(Ordering::Relaxed); @@ -191,6 +202,31 @@ impl StreamingConquer { witness, }) } + + fn close_and_join(&mut self, request_stop: bool) -> Result<(), ConquerError> { + if request_stop { + self.shared.stopped.request(); + } + self.sender.take(); + let mut worker_panicked = false; + for worker in self.workers.drain(..) { + worker_panicked |= worker.join().is_err(); + } + if worker_panicked { + Err(ConquerError::WorkerPanicked) + } else { + Ok(()) + } + } +} + +impl Drop for StreamingConquer { + fn drop(&mut self) { + // Error paths must not detach workers or leave their Kissat children + // behind. Each worker observes this signal in its polling loop, kills + // its active child, and is joined here before the pool disappears. + let _ = self.close_and_join(true); + } } fn worker_loop( @@ -200,21 +236,21 @@ fn worker_loop( kissat: PathBuf, ) { loop { - if shared.stopped.load(Ordering::Acquire) { + if shared.stopped.is_requested() { break; } let cube = match receiver.lock().expect("cube receiver lock").recv() { Ok(cube) => cube, Err(_) => break, }; - if shared.stopped.load(Ordering::Acquire) { + if shared.stopped.is_requested() { break; } match solve_cube(&template, &kissat, &shared, &cube) { Ok(CubeResult::Sat(output)) => { shared.sat.fetch_add(1, Ordering::Relaxed); *shared.witness.lock().expect("witness lock") = Some(output); - shared.stopped.store(true, Ordering::Release); + shared.stopped.request(); } Ok(CubeResult::Unsat) => { shared.unsat.fetch_add(1, Ordering::Relaxed); @@ -281,14 +317,21 @@ fn solve_cube( } let status = loop { - if shared.stopped.load(Ordering::Acquire) { + if shared.stopped.is_requested() { let _ = child.kill(); let _ = child.wait(); reader.join().expect("Kissat output reader panicked")?; return Ok(CubeResult::Cancelled); } - if let Some(status) = child.try_wait().map_err(ConquerError::StartKissat)? { - break status; + match child.try_wait() { + Ok(Some(status)) => break status, + Ok(None) => {} + Err(error) => { + let _ = child.kill(); + let _ = child.wait(); + let _ = reader.join(); + return Err(ConquerError::StartKissat(error)); + } } thread::sleep(std::time::Duration::from_millis(5)); }; diff --git a/src/cube.rs b/src/cube.rs index bdbd0ad..20b4147 100644 --- a/src/cube.rs +++ b/src/cube.rs @@ -21,7 +21,10 @@ use std::num::NonZeroUsize; use std::sync::Arc; use crate::adapter::BranchSolver; -use crate::ct::{apply_masked_assignment, ct_propagate, RSparseBitSet, TableMasks}; +use crate::cdcl::CdclPropagator; +use crate::ct::{ + apply_masked_assignment, ct_propagate, enqueue_var_change, RSparseBitSet, TableMasks, +}; use crate::domain::DomainMask; use crate::measure::Measure; use crate::network::ConstraintNetwork; @@ -29,6 +32,7 @@ use crate::problem::{SolverBuffer, Stats, TnProblem}; use crate::propagate::{dominate_fixpoint, failed_literal_fixpoint}; use crate::selector::{occurrence_pool, Selector, FAILED_LITERAL_POOL}; use crate::table::RegionRuleDiagnostics; +use crate::termination::TerminationSignal; use crate::trail::Trail; use crate::util::count_unfixed; @@ -49,6 +53,8 @@ pub struct CubeStats { pub cubes: usize, pub refuted: usize, pub sat_leaves: usize, + /// A decision-mode component found SAT before the frontier was complete. + pub stopped_early: bool, /// Nodes visited (branch decisions applied). pub visited: u64, } @@ -68,6 +74,7 @@ pub enum CubeRefutationReason { RootPropagation, SelectorNoFeasibleConfig, BranchPropagation, + CdclPropagationConflict, } /// One branching clause in the bit encoding over `CubeNodeTrace::variables`. @@ -96,7 +103,13 @@ pub struct CubeNodeTrace { /// control arm, which deliberately does not run the region machinery. pub rule_diagnostics: Option, pub variables: Vec, + /// Clauses selected by the branching-rule optimizer. Diagnostics such as + /// `branching_vector` and `gamma` describe this cover. + pub optimized_clauses: Vec, + /// Pairwise-disjoint clauses actually traversed by the CnC search. pub clauses: Vec, + /// For each traversed clause, the optimizer clause from which it was split. + pub partition_sources: Vec, } struct CubeCtx<'a> { @@ -105,6 +118,28 @@ struct CubeCtx<'a> { measure: Measure, solver: &'a BranchSolver, cutoff: CubeCutoff, + cdcl: Option, + cdcl_integration: CdclIntegrationMode, + sat_policy: CncSatPolicy, + termination: Option, +} + +impl CubeCtx<'_> { + fn candidate_cdcl(&self) -> Option<&CdclPropagator> { + match self.cdcl_integration { + CdclIntegrationMode::FullPropagation => self.cdcl.as_ref(), + CdclIntegrationMode::HybridCtCandidates => None, + } + } + + fn should_stop_for_sat(&self) -> bool { + if self.sat_policy != CncSatPolicy::StopDecision { + return false; + } + self.termination + .as_ref() + .is_some_and(TerminationSignal::is_requested) + } } /// Online stopping rule evaluated at each post-reduction search node. @@ -116,8 +151,58 @@ pub enum CubeCutoff { CcDifficulty(u128), } +/// Which propagation work is delegated to the persistent CDCL companion. +#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)] +pub enum CdclIntegrationMode { + /// Use CaDiCaL for real-node fixpoints and repeated branching-candidate BCP. + #[default] + FullPropagation, + /// Keep repeated candidate scoring on native CT while CaDiCaL propagates + /// selected branches and retains clauses learned from their conflicts. + HybridCtCandidates, +} + +/// Whether cube generation is exhaustive or participates in first-answer CnC. +#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)] +pub enum CncSatPolicy { + /// Preserve a complete exported frontier even when a solver finds SAT. + #[default] + CompleteFrontier, + /// Stop when the native cuber or any conquer worker proves SAT. + StopDecision, +} + +/// Optional persistent-CDCL integration for one cube-generation run. +#[derive(Clone)] +pub struct CubeCdclOptions { + pub propagator: CdclPropagator, + pub integration: CdclIntegrationMode, +} + +/// Orthogonal generation policies collected in one value to avoid a public +/// function for every cutoff/CDCL/termination combination. +#[derive(Clone)] +pub struct CubeGenerationOptions { + pub cutoff: CubeCutoff, + pub cdcl: Option, + pub sat_policy: CncSatPolicy, + pub termination: Option, +} + +impl CubeGenerationOptions { + pub fn new(cutoff: CubeCutoff) -> Self { + Self { + cutoff, + cdcl: None, + sat_policy: CncSatPolicy::CompleteFrontier, + termination: None, + } + } +} + impl CubeCutoff { - fn stops(self, sigma_dec: usize, sigma_all: usize, freevars: usize) -> bool { + /// Return whether a post-reduction node satisfies this cutoff. + pub fn stops(self, sigma_dec: usize, sigma_all: usize, freevars: usize) -> bool { match self { Self::RemainingVars(n) => freevars < n.get(), Self::CcDifficulty(threshold) => { @@ -193,6 +278,29 @@ pub fn generate_cubes_with_cutoff( cutoff: CubeCutoff, emit: F, ) -> Result +where + F: FnMut(Cube) -> Result<(), E>, +{ + generate_cubes_configured( + problem, + selector, + measure, + solver, + CubeGenerationOptions::new(cutoff), + emit, + ) +} + +/// Primary streaming entry point. This also covers CT-only cubing: a conquer +/// worker can stop the cuber even when no companion CDCL solver is configured. +pub fn generate_cubes_configured( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + options: CubeGenerationOptions, + emit: F, +) -> Result where F: FnMut(Cube) -> Result<(), E>, { @@ -201,12 +309,135 @@ where selector, measure, solver, - cutoff, + options, emit, None::<&mut fn(CubeNodeTrace) -> Result<(), E>>, ) } +/// Compatibility wrapper for callers that configure only SAT termination. +#[allow(clippy::too_many_arguments)] +pub fn generate_cubes_with_cutoff_policy( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + cutoff: CubeCutoff, + sat_policy: CncSatPolicy, + termination: Option, + emit: F, +) -> Result +where + F: FnMut(Cube) -> Result<(), E>, +{ + generate_cubes_configured( + problem, + selector, + measure, + solver, + CubeGenerationOptions { + cutoff, + cdcl: None, + sat_policy, + termination, + }, + emit, + ) +} + +/// CDCL-propagated form of [`generate_cubes_with_cutoff`]. The native network +/// still grows regions and maintains CT tables, while one persistent CaDiCaL +/// instance performs assumption propagation and retains conflict clauses. +#[allow(clippy::too_many_arguments)] +pub fn generate_cubes_with_cutoff_cdcl( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + cutoff: CubeCutoff, + cdcl: CdclPropagator, + emit: F, +) -> Result +where + F: FnMut(Cube) -> Result<(), E>, +{ + generate_cubes_with_cutoff_cdcl_mode( + problem, + selector, + measure, + solver, + cutoff, + cdcl, + CdclIntegrationMode::FullPropagation, + emit, + ) +} + +/// CDCL-assisted generation with an explicit propagation-integration policy. +#[allow(clippy::too_many_arguments)] +pub fn generate_cubes_with_cutoff_cdcl_mode( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + cutoff: CubeCutoff, + cdcl: CdclPropagator, + integration: CdclIntegrationMode, + emit: F, +) -> Result +where + F: FnMut(Cube) -> Result<(), E>, +{ + generate_cubes_with_cutoff_cdcl_policy( + problem, + selector, + measure, + solver, + cutoff, + cdcl, + integration, + CncSatPolicy::CompleteFrontier, + None, + emit, + ) +} + +/// CDCL-assisted generation with explicit propagation and SAT termination +/// policies. +#[allow(clippy::too_many_arguments)] +pub fn generate_cubes_with_cutoff_cdcl_policy( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + cutoff: CubeCutoff, + cdcl: CdclPropagator, + integration: CdclIntegrationMode, + sat_policy: CncSatPolicy, + termination: Option, + emit: F, +) -> Result +where + F: FnMut(Cube) -> Result<(), E>, +{ + generate_cubes_configured( + problem, + selector, + measure, + solver, + CubeGenerationOptions { + cutoff, + cdcl: Some(CubeCdclOptions { + propagator: cdcl, + integration, + }), + sat_policy, + termination, + }, + emit, + ) +} + /// Streaming cube generation with an additional callback for every tree node. /// The trace callback observes data already computed by the normal search and /// must not mutate solver state, so enabling it does not alter the frontier. @@ -242,18 +473,178 @@ pub fn generate_cubes_with_cutoff_trace( solver: &BranchSolver, cutoff: CubeCutoff, emit: F, + trace: T, +) -> Result +where + F: FnMut(Cube) -> Result<(), E>, + T: FnMut(CubeNodeTrace) -> Result<(), E>, +{ + generate_cubes_with_cutoff_trace_policy( + problem, + selector, + measure, + solver, + cutoff, + CncSatPolicy::CompleteFrontier, + None, + emit, + trace, + ) +} + +/// Traced generation with a shared first-answer signal. +#[allow(clippy::too_many_arguments)] +pub fn generate_cubes_with_cutoff_trace_policy( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + cutoff: CubeCutoff, + sat_policy: CncSatPolicy, + termination: Option, + emit: F, mut trace: T, ) -> Result where F: FnMut(Cube) -> Result<(), E>, T: FnMut(CubeNodeTrace) -> Result<(), E>, { - generate_cubes_impl( + generate_cubes_configured_with_trace( + problem, + selector, + measure, + solver, + CubeGenerationOptions { + cutoff, + cdcl: None, + sat_policy, + termination, + }, + emit, + &mut trace, + ) +} + +/// Traced counterpart of [`generate_cubes_with_cutoff_cdcl`]. +#[allow(clippy::too_many_arguments)] +pub fn generate_cubes_with_cutoff_trace_cdcl( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + cutoff: CubeCutoff, + cdcl: CdclPropagator, + emit: F, + trace: T, +) -> Result +where + F: FnMut(Cube) -> Result<(), E>, + T: FnMut(CubeNodeTrace) -> Result<(), E>, +{ + generate_cubes_with_cutoff_trace_cdcl_mode( + problem, + selector, + measure, + solver, + cutoff, + cdcl, + CdclIntegrationMode::FullPropagation, + emit, + trace, + ) +} + +/// Traced CDCL-assisted generation with an explicit integration policy. +#[allow(clippy::too_many_arguments)] +pub fn generate_cubes_with_cutoff_trace_cdcl_mode( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + cutoff: CubeCutoff, + cdcl: CdclPropagator, + integration: CdclIntegrationMode, + emit: F, + trace: T, +) -> Result +where + F: FnMut(Cube) -> Result<(), E>, + T: FnMut(CubeNodeTrace) -> Result<(), E>, +{ + generate_cubes_with_cutoff_trace_cdcl_policy( problem, selector, measure, solver, cutoff, + cdcl, + integration, + CncSatPolicy::CompleteFrontier, + None, + emit, + trace, + ) +} + +/// Traced CDCL-assisted generation with explicit propagation and SAT +/// termination policies. +#[allow(clippy::too_many_arguments)] +pub fn generate_cubes_with_cutoff_trace_cdcl_policy( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + cutoff: CubeCutoff, + cdcl: CdclPropagator, + integration: CdclIntegrationMode, + sat_policy: CncSatPolicy, + termination: Option, + emit: F, + mut trace: T, +) -> Result +where + F: FnMut(Cube) -> Result<(), E>, + T: FnMut(CubeNodeTrace) -> Result<(), E>, +{ + generate_cubes_configured_with_trace( + problem, + selector, + measure, + solver, + CubeGenerationOptions { + cutoff, + cdcl: Some(CubeCdclOptions { + propagator: cdcl, + integration, + }), + sat_policy, + termination, + }, + emit, + &mut trace, + ) +} + +/// Traced form of [`generate_cubes_configured`]. +pub fn generate_cubes_configured_with_trace( + problem: &mut TnProblem, + selector: Selector, + measure: Measure, + solver: &BranchSolver, + options: CubeGenerationOptions, + emit: F, + mut trace: T, +) -> Result +where + F: FnMut(Cube) -> Result<(), E>, + T: FnMut(CubeNodeTrace) -> Result<(), E>, +{ + generate_cubes_impl( + problem, + selector, + measure, + solver, + options, emit, Some(&mut trace), ) @@ -264,7 +655,7 @@ fn generate_cubes_impl( selector: Selector, measure: Measure, solver: &BranchSolver, - cutoff: CubeCutoff, + options: CubeGenerationOptions, mut emit: F, mut trace: Option<&mut T>, ) -> Result @@ -273,12 +664,24 @@ where T: FnMut(CubeNodeTrace) -> Result<(), E>, { problem.stats.reset(); + let (cdcl, cdcl_integration) = options + .cdcl + .map(|options| (Some(options.propagator), options.integration)) + .unwrap_or((None, CdclIntegrationMode::FullPropagation)); + let termination = match (options.sat_policy, options.termination) { + (CncSatPolicy::StopDecision, None) => Some(TerminationSignal::new()), + (_, termination) => termination, + }; let ctx = CubeCtx { cn: &problem.static_cn, selector, measure, solver, - cutoff, + cutoff: options.cutoff, + cdcl, + cdcl_integration, + sat_policy: options.sat_policy, + termination, }; let masks = &problem.masks; let stats = &mut problem.stats; @@ -291,9 +694,13 @@ where let mut decisions: Vec<(usize, bool)> = Vec::new(); let mut next_node_id = 0u64; let mark = trail.mark(); + let root_cdcl_refuted = + cdcl_propagate_then_ct(&ctx, doms, masks, tables, buffer, trail, &decisions); // Root already propagated; if it is already solved or refuted, that is a // single (degenerate) cube. - let result = if doms[0] == DomainMask::NONE { + let result = if ctx.should_stop_for_sat() { + Ok(()) + } else if doms[0] == DomainMask::NONE { if let Some(trace) = trace.as_deref_mut() { trace(CubeNodeTrace { node_id: 0, @@ -301,14 +708,20 @@ where child_index: None, depth: 0, kind: CubeNodeKind::Refuted, - refutation_reason: Some(CubeRefutationReason::RootPropagation), + refutation_reason: Some(if root_cdcl_refuted { + CubeRefutationReason::CdclPropagationConflict + } else { + CubeRefutationReason::RootPropagation + }), decisions: Vec::new(), sigma_dec: 0, sigma_all: 0, freevars: doms.len(), rule_diagnostics: None, variables: Vec::new(), + optimized_clauses: Vec::new(), clauses: Vec::new(), + partition_sources: Vec::new(), })?; } emit_cube( @@ -344,6 +757,7 @@ where trail.restore_to(mark, doms, tables); result?; + cube_stats.stopped_early = ctx.should_stop_for_sat(); cube_stats.visited = stats.total_visited_nodes; Ok(cube_stats) } @@ -384,6 +798,9 @@ where F: FnMut(Cube) -> Result<(), E>, T: FnMut(CubeNodeTrace) -> Result<(), E>, { + if ctx.should_stop_for_sat() { + return Ok(()); + } let node_id = *next_node_id; *next_node_id += 1; // march_cu -n cutoff on the current post-reduction node. The reductions run @@ -407,7 +824,9 @@ where freevars, rule_diagnostics: None, variables: Vec::new(), + optimized_clauses: Vec::new(), clauses: Vec::new(), + partition_sources: Vec::new(), })?; } return emit_cube( @@ -442,9 +861,17 @@ where freevars, rule_diagnostics: None, variables: Vec::new(), + optimized_clauses: Vec::new(), clauses: Vec::new(), + partition_sources: Vec::new(), })?; } + if ctx.sat_policy == CncSatPolicy::StopDecision { + ctx.termination + .as_ref() + .expect("decision mode always has a termination signal") + .request(); + } return emit_cube( cube_stats, emit, @@ -468,8 +895,13 @@ where tables, trail, &scope, + ctx.candidate_cdcl(), + decisions, trace.is_some(), ); + if ctx.should_stop_for_sat() { + return Ok(()); + } let clauses = match selection.clauses { // No rule (region proved locally UNSAT): refuted cube. None => { @@ -487,7 +919,9 @@ where freevars, rule_diagnostics: selection.diagnostics, variables: selection.variables, + optimized_clauses: Vec::new(), clauses: Vec::new(), + partition_sources: Vec::new(), })?; } return emit_cube( @@ -504,10 +938,32 @@ where } Some(clauses) => clauses, }; + // Optimal-branching rules are set covers: their conjunctions may overlap. + // That is acceptable for branch-and-reduce, but a CnC frontier must be a + // partition or the same residual search space can be submitted repeatedly. + // Subtract earlier cubes from each later cube to obtain an equivalent + // disjoint DNF before descending. + let optimized_clauses = clauses; + let partition = disjointize_clauses_with_sources(&optimized_clauses); + let clauses = partition + .iter() + .map(|(clause, _)| *clause) + .collect::>(); + let partition_sources = partition + .iter() + .map(|(_, source)| *source) + .collect::>(); let variables = selection.variables; let rule_diagnostics = selection.diagnostics; if let Some(trace) = trace.as_deref_mut() { + let trace_optimized_clauses = optimized_clauses + .iter() + .map(|clause| TraceClause { + mask: clause.mask, + value: clause.val, + }) + .collect(); let trace_clauses = clauses .iter() .map(|clause| TraceClause { @@ -528,11 +984,16 @@ where freevars, rule_diagnostics, variables: variables.clone(), + optimized_clauses: trace_optimized_clauses, clauses: trace_clauses, + partition_sources: partition_sources.clone(), })?; } for (branch_index, cl) in clauses.iter().enumerate() { + if ctx.should_stop_for_sat() { + break; + } stats.record_visit(); trail.open(); let mark = trail.mark(); @@ -545,15 +1006,24 @@ where } } apply_masked_assignment(ctx.cn, doms, buffer, trail, &variables, cl.mask, cl.val); - ct_propagate(ctx.cn, doms, masks, tables, buffer, trail); - if doms[0] != DomainMask::NONE { + // The selected branch reaches CaDiCaL before native CT propagation. + // Thus an immediate branch conflict is analyzed and learned by CDCL + // instead of being consumed first by the native propagator. + let cdcl_refuted = + cdcl_propagate_then_ct(ctx, doms, masks, tables, buffer, trail, decisions); + let mut stop_for_sat = ctx.should_stop_for_sat(); + if !stop_for_sat && doms[0] != DomainMask::NONE { dominate_fixpoint(ctx.cn, doms, masks, tables, buffer, trail); } - if doms[0] != DomainMask::NONE { + stop_for_sat |= ctx.should_stop_for_sat(); + if !stop_for_sat && doms[0] != DomainMask::NONE { let pool = occurrence_pool(ctx.cn, doms, buffer, masks, FAILED_LITERAL_POOL); failed_literal_fixpoint(ctx.cn, doms, masks, tables, buffer, trail, &pool); } - let branch_result = if doms[0] == DomainMask::NONE { + stop_for_sat |= ctx.should_stop_for_sat(); + let branch_result = if stop_for_sat { + Ok(()) + } else if doms[0] == DomainMask::NONE { // Branch closed by propagation: refuted cube (no conquer needed). let branch_freevars = count_unfixed(doms); let child_node_id = *next_node_id; @@ -565,14 +1035,20 @@ where child_index: Some(branch_index), depth: depth + 1, kind: CubeNodeKind::Refuted, - refutation_reason: Some(CubeRefutationReason::BranchPropagation), + refutation_reason: Some(if cdcl_refuted { + CubeRefutationReason::CdclPropagationConflict + } else { + CubeRefutationReason::BranchPropagation + }), decisions: decisions.clone(), sigma_dec: decisions.len(), sigma_all: doms.len() - branch_freevars, freevars: branch_freevars, rule_diagnostics: None, variables: Vec::new(), + optimized_clauses: Vec::new(), clauses: Vec::new(), + partition_sources: Vec::new(), })?; } emit_cube( @@ -608,15 +1084,144 @@ where decisions.truncate(decision_base); trail.restore_to(mark, doms, tables); branch_result?; + if stop_for_sat || ctx.should_stop_for_sat() { + break; + } } Ok(()) } +/// Convert a DNF cube cover into an equivalent pairwise-disjoint cube cover. +/// +/// Clauses are processed in order. Each new cube has the union of all earlier +/// output cubes subtracted from it; subtraction of one conjunction from another +/// uses the standard prefix split of `A ∧ ¬B`. +#[cfg(test)] +fn disjointize_clauses( + clauses: &[optimal_branching_core::Clause], +) -> Vec { + disjointize_clauses_with_sources(clauses) + .into_iter() + .map(|(clause, _)| clause) + .collect() +} + +fn disjointize_clauses_with_sources( + clauses: &[optimal_branching_core::Clause], +) -> Vec<(optimal_branching_core::Clause, usize)> { + let mut disjoint = Vec::new(); + for (source, &clause) in clauses.iter().enumerate() { + let mut pieces = vec![clause]; + for &(covered, _) in &disjoint { + pieces = pieces + .into_iter() + .flat_map(|piece| subtract_clause(piece, covered)) + .collect(); + if pieces.is_empty() { + break; + } + } + disjoint.extend(pieces.into_iter().map(|piece| (piece, source))); + } + disjoint +} + +fn subtract_clause( + minuend: optimal_branching_core::Clause, + subtrahend: optimal_branching_core::Clause, +) -> Vec { + let shared = minuend.mask & subtrahend.mask; + if ((minuend.val ^ subtrahend.val) & shared) != 0 { + return vec![minuend]; + } + + let mut remaining = subtrahend.mask & !minuend.mask; + if remaining == 0 { + return Vec::new(); + } + + let mut prefix = minuend; + let mut pieces = Vec::with_capacity(remaining.count_ones() as usize); + while remaining != 0 { + let bit = remaining & remaining.wrapping_neg(); + let required = subtrahend.val & bit; + pieces.push(optimal_branching_core::Clause::new( + prefix.mask | bit, + prefix.val | (required ^ bit), + )); + prefix = optimal_branching_core::Clause::new(prefix.mask | bit, prefix.val | required); + remaining &= !bit; + } + pieces +} + +/// Apply the committed decision path to persistent CaDiCaL exactly once, then +/// project its native implications into one native CT fixpoint. CDCL auxiliaries +/// stay private to CaDiCaL; every newly fixed native variable is trailed and +/// sent through CT so later region work sees a coherent native store. +/// +/// Returns true exactly when CaDiCaL's assumption propagation found the +/// conflict. A native CT conflict returns false so traces preserve provenance. +fn cdcl_propagate_then_ct( + ctx: &CubeCtx<'_>, + doms: &mut [DomainMask], + masks: &[TableMasks], + tables: &mut [RSparseBitSet], + buffer: &mut SolverBuffer, + trail: &mut Trail, + decisions: &[(usize, bool)], +) -> bool { + let Some(cdcl) = &ctx.cdcl else { + ct_propagate(ctx.cn, doms, masks, tables, buffer, trail); + return false; + }; + if doms.first() == Some(&DomainMask::NONE) { + return false; + } + let projected = cdcl + .propagate_decisions(doms, decisions) + .expect("CDCL node propagation failed"); + if projected.first() == Some(&DomainMask::NONE) { + set_contradiction(doms, trail); + return true; + } + for (var, &implied) in projected.iter().enumerate() { + if !implied.is_fixed() { + continue; + } + match doms[var] { + DomainMask::BOTH => { + trail.record_dom(var, doms[var]); + doms[var] = implied; + enqueue_var_change(ctx.cn, buffer, var); + } + current if current == implied => {} + _ => { + set_contradiction(doms, trail); + return true; + } + } + } + ct_propagate(ctx.cn, doms, masks, tables, buffer, trail); + false +} + +fn set_contradiction(doms: &mut [DomainMask], trail: &mut Trail) { + if let Some(sentinel) = doms.first_mut() { + if *sentinel != DomainMask::NONE { + trail.record_dom(0, *sentinel); + *sentinel = DomainMask::NONE; + } + } +} + #[cfg(test)] mod tests { use super::*; + use crate::cdcl::CdclPropagator; use crate::dimacs::network_from_dimacs; use optimal_branching_core::GreedyMerge; + use std::io::Cursor; fn xor_chain() -> TnProblem { let cnf = "p cnf 3 4\n1 2 0\n-1 -2 0\n2 3 0\n-2 -3 0\n"; @@ -628,6 +1233,28 @@ mod tests { NonZeroUsize::new(value).expect("test cutoff must be nonzero") } + #[test] + fn overlapping_branch_cover_is_disjointized_without_changing_union() { + use optimal_branching_core::Clause; + + // x0=0 and x1=0 overlap on 00*. The third cube also overlaps both. + let cover = vec![ + Clause::new(0b001, 0), + Clause::new(0b010, 0), + Clause::new(0b100, 0b100), + ]; + let partition = disjointize_clauses(&cover); + + for assignment in 0..8 { + let covered = cover.iter().any(|clause| clause.covered_by(assignment)); + let partition_count = partition + .iter() + .filter(|clause| clause.covered_by(assignment)) + .count(); + assert_eq!(partition_count, usize::from(covered)); + } + } + /// A cutoff larger than the root residual emits the empty decision path, /// while a cutoff equal to the residual must branch because `-n` is strict. #[test] @@ -659,6 +1286,134 @@ mod tests { .all(|c| !c.decisions.is_empty())); } + #[test] + fn hybrid_keeps_cdcl_at_committed_nodes_not_candidate_probes() { + const CNF: &str = "p cnf 3 4\n1 2 0\n-1 -2 0\n2 3 0\n-2 -3 0\n"; + + fn run(integration: CdclIntegrationMode) -> (Vec, CubeStats, crate::cdcl::CdclStats) { + let mut problem = xor_chain(); + let mut reader = Cursor::new(CNF.as_bytes()); + let cdcl = CdclPropagator::from_dimacs(&mut reader, vec![0, 1, 2]) + .expect("create CaDiCaL companion"); + let mut cubes = Vec::new(); + let stats = generate_cubes_with_cutoff_cdcl_mode( + &mut problem, + Selector::MostOccurrence { max_rows: 1 }, + Measure::NumUnfixedVars, + &BranchSolver::Greedy(GreedyMerge), + CubeCutoff::RemainingVars(n(3)), + cdcl.clone(), + integration, + |cube| { + cubes.push(cube); + Ok::<(), Infallible>(()) + }, + ) + .expect("infallible callback"); + let cdcl_stats = cdcl.stats(); + (cubes, stats, cdcl_stats) + } + + let (full_cubes, full_stats, full_cdcl) = run(CdclIntegrationMode::FullPropagation); + let (hybrid_cubes, hybrid_stats, hybrid_cdcl) = + run(CdclIntegrationMode::HybridCtCandidates); + + assert_eq!(full_stats.cubes, hybrid_stats.cubes); + assert_eq!(full_stats.refuted, hybrid_stats.refuted); + assert_eq!(full_stats.sat_leaves, hybrid_stats.sat_leaves); + assert_eq!(full_stats.visited, hybrid_stats.visited); + assert_eq!(full_cubes.len(), hybrid_cubes.len()); + for (full, hybrid) in full_cubes.iter().zip(&hybrid_cubes) { + assert_eq!(full.decisions, hybrid.decisions); + assert_eq!(full.sigma_dec, hybrid.sigma_dec); + assert_eq!(full.sigma_all, hybrid.sigma_all); + assert_eq!(full.refuted, hybrid.refuted); + assert_eq!(full.sat, hybrid.sat); + } + assert!( + hybrid_cdcl.propagation_calls < full_cdcl.propagation_calls, + "hybrid should eliminate candidate BCP calls: full={}, hybrid={}", + full_cdcl.propagation_calls, + hybrid_cdcl.propagation_calls + ); + assert!( + hybrid_cdcl.propagation_calls > 0, + "hybrid must still propagate at committed nodes" + ); + assert_eq!( + hybrid_cdcl.propagation_calls, + hybrid_stats.visited + 1, + "hybrid performs one root query and one query per committed branch" + ); + } + + #[test] + fn cdcl_only_emits_after_cutoff_and_never_starts_a_full_search() { + const CNF: &str = "p cnf 3 4\n1 2 0\n-1 -2 0\n2 3 0\n-2 -3 0\n"; + let mut reader = Cursor::new(CNF.as_bytes()); + let cdcl = CdclPropagator::from_dimacs(&mut reader, vec![0, 1, 2]) + .expect("create CaDiCaL companion"); + let mut problem = xor_chain(); + let mut cubes = Vec::new(); + let mut nodes = Vec::new(); + let stats = generate_cubes_with_cutoff_trace_cdcl_policy( + &mut problem, + Selector::MostOccurrence { max_rows: 1 }, + Measure::NumUnfixedVars, + &BranchSolver::Greedy(GreedyMerge), + CubeCutoff::RemainingVars(n(3)), + cdcl.clone(), + CdclIntegrationMode::HybridCtCandidates, + CncSatPolicy::StopDecision, + None, + |cube| { + cubes.push(cube); + Ok::<(), Infallible>(()) + }, + |node| { + nodes.push(node); + Ok::<(), Infallible>(()) + }, + ) + .expect("infallible callbacks"); + + assert!(!stats.stopped_early); + assert!(!cubes.is_empty()); + assert!(cubes.iter().all(|cube| cube.refuted || cube.sat || { + let freevars = 3 - cube.sigma_all; + freevars < 3 && !cube.decisions.is_empty() + })); + assert!(nodes.iter().any(|node| node.kind == CubeNodeKind::Branch)); + assert!(nodes.iter().any(|node| node.kind == CubeNodeKind::Cutoff)); + assert_eq!(cdcl.stats().full_search_calls, 0); + } + + #[test] + fn decision_policy_honors_a_conquer_stop_without_cdcl() { + let signal = TerminationSignal::new(); + signal.request(); + let mut problem = xor_chain(); + let mut cubes = Vec::new(); + + let stats = generate_cubes_with_cutoff_policy( + &mut problem, + Selector::MostOccurrence { max_rows: 1 }, + Measure::NumUnfixedVars, + &BranchSolver::Greedy(GreedyMerge), + CubeCutoff::RemainingVars(n(3)), + CncSatPolicy::StopDecision, + Some(signal), + |cube| { + cubes.push(cube); + Ok::<(), Infallible>(()) + }, + ) + .expect("infallible callback"); + + assert!(stats.stopped_early); + assert!(cubes.is_empty()); + } + #[test] fn cc_difficulty_cutoff_is_evaluated_online() { let mut problem = xor_chain(); diff --git a/src/lib.rs b/src/lib.rs index 542e365..4fd38fa 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,6 +1,7 @@ pub mod adapter; pub mod api; pub mod canonicalize; +pub mod cdcl; pub mod circuit; pub mod conquer; pub mod contract; @@ -19,5 +20,6 @@ pub mod selector; pub mod solver; pub mod table; pub mod tail_greedy; +pub mod termination; pub mod trail; pub mod util; diff --git a/src/selector.rs b/src/selector.rs index fcdf571..4955dc8 100644 --- a/src/selector.rs +++ b/src/selector.rs @@ -3,12 +3,13 @@ use std::sync::Arc; use optimal_branching_core::Clause; use crate::adapter::BranchSolver; +use crate::cdcl::CdclPropagator; use crate::ct::{RSparseBitSet, TableMasks}; use crate::domain::DomainMask; use crate::measure::Measure; use crate::network::ConstraintNetwork; use crate::problem::SolverBuffer; -use crate::table::{compute_branching_result, BranchingResult}; +use crate::table::BranchingResult; use crate::trail::Trail; use crate::util::{active_tensors, is_entailed}; @@ -148,6 +149,8 @@ impl Selector { tables: &mut Vec, trail: &mut Trail, scope: &[usize], + cdcl: Option<&CdclPropagator>, + cdcl_decisions: &[(usize, bool)], collect_diagnostics: bool, ) -> BranchingResult { let var_id = select_var_most_occurrence(cn, doms, buffer, scope, masks); @@ -195,7 +198,7 @@ impl Selector { diagnostics: None, }; } - compute_branching_result( + crate::table::compute_branching_result_with_cdcl( cn, doms, buffer, @@ -206,6 +209,8 @@ impl Selector { masks, tables, trail, + cdcl, + cdcl_decisions, collect_diagnostics || self.replays_same_state(), self.replays_same_state(), ) @@ -295,6 +300,8 @@ mod tests { &mut tables, &mut trail, &[0, 1], + None, + &[], false, ); assert_eq!(result.variables, vec![0, 1]); @@ -328,6 +335,8 @@ mod tests { &mut tables, &mut trail, &[0, 1, 2, 3], + None, + &[], false, ); assert!(result.clauses.is_some()); @@ -344,6 +353,8 @@ mod tests { &mut tables, &mut trail, &[0, 1, 2, 3], + None, + &[], true, ); assert_eq!(traced.clauses, result.clauses); diff --git a/src/solver.rs b/src/solver.rs index 9fe9667..08ad747 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -104,6 +104,8 @@ fn bbsat_rec( tables, trail, scope, + None, + &[], false, ); let clauses = match selection.clauses { diff --git a/src/table.rs b/src/table.rs index 2bcc18c..4b47534 100644 --- a/src/table.rs +++ b/src/table.rs @@ -4,6 +4,7 @@ use std::time::Instant; use optimal_branching_core::{BranchingTable, Clause, NaiveBranch, OptimalBranchingResult, DNF}; use crate::adapter::{with_measure_scratch, BranchSolver, MeasureAdapter, RuleProblem}; +use crate::cdcl::CdclPropagator; use crate::ct::{RSparseBitSet, TableMasks}; use crate::domain::DomainMask; use crate::measure::Measure; @@ -160,6 +161,44 @@ pub fn compute_branching_result( trail: &mut Trail, collect_diagnostics: bool, replay_diagnostics: bool, +) -> BranchingResult { + compute_branching_result_with_cdcl( + cn, + doms, + buffer, + var_id, + max_rows, + measure, + solver, + masks, + tables, + trail, + None, + &[], + collect_diagnostics, + replay_diagnostics, + ) +} + +/// CDCL-scored form of [`compute_branching_result`]. Region growth and global +/// feasibility remain native/CT; only the many hypothetical `apply_branch` +/// probes performed by the rule optimizer use assumption-only CDCL BCP. +#[allow(clippy::too_many_arguments)] +pub fn compute_branching_result_with_cdcl( + cn: &Arc, + doms: &mut [DomainMask], + buffer: &mut SolverBuffer, + var_id: usize, + max_rows: usize, + measure: Measure, + solver: &BranchSolver, + masks: &Arc>, + tables: &mut Vec, + trail: &mut Trail, + cdcl: Option<&CdclPropagator>, + cdcl_decisions: &[(usize, bool)], + collect_diagnostics: bool, + replay_diagnostics: bool, ) -> BranchingResult { debug_assert!(!replay_diagnostics || collect_diagnostics); // 1. Grow the region and keep only its GAC-feasible configs, decided with @@ -170,9 +209,11 @@ pub fn compute_branching_result( // Growth already knows whether the live frontier is empty. Enumerate the // exact boundary only for trace diagnostics; production search pays no // second incidence scan and allocates no boundary vector. - let boundary_variables = collect_diagnostics - .then(|| boundary_vars(cn, ®ion, doms, masks).len()) - .unwrap_or(0); + let boundary_variables = if collect_diagnostics { + boundary_vars(cn, ®ion, doms, masks).len() + } else { + 0 + }; debug_assert!(!collect_diagnostics || closed == (boundary_variables == 0)); let region_tensors = region.tensors.len(); let region_vars = region.vars; @@ -235,7 +276,7 @@ pub fn compute_branching_result( let same_state_replay = if replay_diagnostics { let groups: Vec> = feasible.iter().map(|&c| vec![c]).collect(); let table = BranchingTable::new(region_vars.len(), groups); - let problem = RuleProblem::new(Arc::clone(cn), Arc::clone(masks), doms.to_vec()); + let problem = rule_problem(cn, masks, doms, cdcl, cdcl_decisions); Some(with_measure_scratch(doms, tables, buffer, trail, || { replay_same_state(&problem, &table, ®ion_vars, var_id, measure) })) @@ -273,12 +314,11 @@ pub fn compute_branching_result( // framework computes each candidate's measure reduction itself // (apply_branch + measure) and applies the literal-count fallback when the // measure is degenerate, so IPSolver/LPSolver/GreedyMerge/NaiveBranch all - // produce the rule through this one call. `apply_branch` uses CT via the - // thread-local measure scratch primed here. - let problem = RuleProblem::new(Arc::clone(cn), Arc::clone(masks), doms.to_vec()); - // Lend the live CT state to the measure scratch so apply_branch propagates - // with CT instead of the linear rescan. apply_branch restores it to base - // after every candidate, so `doms`/`tables`/`buffer`/`trail` are unchanged here. + // produce the rule through this one call. `apply_branch` uses the selected + // CDCL or CT propagation backend. + let problem = rule_problem(cn, masks, doms, cdcl, cdcl_decisions); + // Keep CT scratch primed for the CT backend and replay path. CDCL candidate + // calls ignore it. Either way, `doms`/`tables`/`buffer`/`trail` are unchanged. let (result, rule_solver_ns, same_state_replay) = with_measure_scratch(doms, tables, buffer, trail, || { let rule_start = collect_diagnostics.then(Instant::now); @@ -301,9 +341,8 @@ pub fn compute_branching_result( ); true }); - BranchingResult { - clauses: Some(result.optimal_rule.clauses), - diagnostics: collect_diagnostics.then(|| RegionRuleDiagnostics { + let diagnostics = if collect_diagnostics { + Some(RegionRuleDiagnostics { focus_var: var_id, region_tensors, region_variables: region_vars.len(), @@ -319,11 +358,31 @@ pub fn compute_branching_result( feasibility_probe_ns, rule_solver_ns, same_state_replay, - }), + }) + } else { + None + }; + BranchingResult { + clauses: Some(result.optimal_rule.clauses), + diagnostics, variables: region_vars, } } +fn rule_problem( + cn: &Arc, + masks: &Arc>, + doms: &[DomainMask], + cdcl: Option<&CdclPropagator>, + cdcl_decisions: &[(usize, bool)], +) -> RuleProblem { + let problem = RuleProblem::new(Arc::clone(cn), Arc::clone(masks), doms.to_vec()); + match cdcl { + Some(cdcl) => problem.with_cdcl(cdcl.clone(), cdcl_decisions.to_vec()), + None => problem, + } +} + #[cfg(test)] mod tests { use super::*; diff --git a/src/termination.rs b/src/termination.rs new file mode 100644 index 0000000..fb72a62 --- /dev/null +++ b/src/termination.rs @@ -0,0 +1,27 @@ +//! Shared first-answer termination for Cube-and-Conquer components. + +use std::sync::atomic::{AtomicBool, Ordering}; +use std::sync::Arc; + +/// A clone-cheap stop signal shared by the cuber, its CDCL companion, and all +/// conquer workers. +#[derive(Clone, Debug, Default)] +pub struct TerminationSignal { + requested: Arc, +} + +impl TerminationSignal { + pub fn new() -> Self { + Self::default() + } + + /// Publish that one sound component has decided the instance. + pub fn request(&self) { + self.requested.store(true, Ordering::Release); + } + + /// Observe a previously published terminal result. + pub fn is_requested(&self) -> bool { + self.requested.load(Ordering::Acquire) + } +} diff --git a/tests/cnc_cuber_trace.rs b/tests/cnc_cuber_trace.rs index ee058fd..ba8ee23 100644 --- a/tests/cnc_cuber_trace.rs +++ b/tests/cnc_cuber_trace.rs @@ -115,7 +115,9 @@ fn trace_flag_preserves_cubes_and_writes_original_variable_ids() { .map(|line| serde_json::from_str(line).expect("valid trace JSON")) .collect(); assert!(!records.is_empty()); - assert!(records.iter().all(|record| record["schema_version"] == 2)); + assert!(records + .iter() + .all(|record| record.get("schema_version").is_none())); assert!(records .iter() .all(|record| record["search_semantics"] == "sat-decision")); @@ -124,6 +126,8 @@ fn trace_flag_preserves_cubes_and_writes_original_variable_ids() { .iter() .all(|record| record["branch_solver"] == "greedy")); assert!(records.iter().all(|record| record["measure"] == "vars")); + assert!(records.iter().all(|record| record["propagation"] == "ct")); + assert!(records.iter().all(|record| record["cdcl_mode"] == "off")); assert!(records .iter() .all(|record| record["input_kind"] == "dimacs")); @@ -207,6 +211,242 @@ fn trace_flag_preserves_cubes_and_writes_original_variable_ids() { fs::remove_dir_all(dir).expect("remove temp directory"); } +#[test] +fn cdcl_propagation_matches_ct_on_a_clause_network() { + let dir = temp_dir(); + fs::create_dir_all(&dir).expect("create temp directory"); + let input = dir.join("input.cnf"); + let ct_cubes = dir.join("ct.cubes"); + let cdcl_cubes = dir.join("cdcl.cubes"); + let cdcl_trace = dir.join("cdcl.jsonl"); + fs::write( + &input, + "p cnf 6 8\n\ + 1 2 0\n-1 -2 0\n2 3 0\n-2 -3 0\n\ + 4 5 0\n-4 -5 0\n5 6 0\n-5 -6 0\n", + ) + .expect("write CNF"); + + let binary = env!("CARGO_BIN_EXE_cnc_cuber"); + let common = [ + "-n", + "4", + "--branch-solver", + "greedy", + "--measure", + "vars", + "--max-rows", + "1", + ]; + let ct = Command::new(binary) + .arg(&input) + .args(["-o"]) + .arg(&ct_cubes) + .args(common) + .output() + .expect("run CT cuber"); + assert!(ct.status.success(), "{ct:?}"); + + let cdcl = Command::new(binary) + .arg(&input) + .args(["-o"]) + .arg(&cdcl_cubes) + .args(common) + .args(["--propagation", "cdcl", "--trace"]) + .arg(&cdcl_trace) + .output() + .expect("run CDCL cuber"); + assert!(cdcl.status.success(), "{cdcl:?}"); + assert_eq!(fs::read(&ct_cubes).unwrap(), fs::read(&cdcl_cubes).unwrap()); + assert!( + String::from_utf8_lossy(&cdcl.stderr).contains("propagation=cdcl"), + "{cdcl:?}" + ); + let records: Vec = fs::read_to_string(&cdcl_trace) + .unwrap() + .lines() + .map(|line| serde_json::from_str(line).expect("valid trace JSON")) + .collect(); + assert!(!records.is_empty()); + assert!(records.iter().all(|record| record["propagation"] == "cdcl")); + assert!(records + .iter() + .all(|record| record["cdcl_mode"] == "branch-learning")); + + fs::remove_dir_all(dir).expect("remove temp directory"); +} + +#[test] +fn branch_learning_handles_a_non_bcp_unsat_formula_without_full_search() { + let dir = temp_dir(); + fs::create_dir_all(&dir).expect("create temp directory"); + let input = dir.join("learning-unsat.cnf"); + let cubes = dir.join("learning-unsat.cubes"); + let trace = dir.join("learning-unsat.jsonl"); + // PHP(4,3): root BCP stays open. Repeated branch propagation retains + // conflict clauses, but the cuber-side CaDiCaL never starts a full solve. + fs::write( + &input, + "p cnf 12 22\n\ + 1 2 3 0\n4 5 6 0\n7 8 9 0\n10 11 12 0\n\ + -1 -4 0\n-1 -7 0\n-1 -10 0\n-4 -7 0\n-4 -10 0\n-7 -10 0\n\ + -2 -5 0\n-2 -8 0\n-2 -11 0\n-5 -8 0\n-5 -11 0\n-8 -11 0\n\ + -3 -6 0\n-3 -9 0\n-3 -12 0\n-6 -9 0\n-6 -12 0\n-9 -12 0\n", + ) + .expect("write non-BCP UNSAT CNF"); + + let run = Command::new(env!("CARGO_BIN_EXE_cnc_cuber")) + .arg(&input) + .args(["-n", "1", "-o"]) + .arg(&cubes) + .args([ + "--branch-solver", + "greedy", + "--measure", + "vars", + "--propagation", + "cdcl", + "--trace", + ]) + .arg(&trace) + .output() + .expect("run learning CDCL cuber"); + assert!(run.status.success(), "{run:?}"); + assert!(fs::read_to_string(&cubes).unwrap().is_empty()); + let records: Vec = fs::read_to_string(&trace) + .unwrap() + .lines() + .map(|line| serde_json::from_str(line).expect("valid trace JSON")) + .collect(); + assert!(!records.is_empty()); + assert!(records + .iter() + .all(|record| record["cdcl_mode"] == "branch-learning")); + let stderr = String::from_utf8_lossy(&run.stderr); + assert!(stderr.contains("cdcl_mode=branch-learning"), "{stderr}"); + assert!(stderr.contains("full_search_calls=0"), "{stderr}"); + assert!(stderr.contains("learned_total="), "{stderr}"); + + fs::remove_dir_all(dir).expect("remove temp directory"); +} + +#[test] +fn hybrid_uses_ct_candidates_and_committed_branch_cdcl_learning() { + let dir = temp_dir(); + fs::create_dir_all(&dir).expect("create temp directory"); + let input = dir.join("learning-unsat.cnf"); + let cubes = dir.join("hybrid.cubes"); + let trace = dir.join("hybrid.jsonl"); + fs::write( + &input, + "p cnf 12 22\n\ + 1 2 3 0\n4 5 6 0\n7 8 9 0\n10 11 12 0\n\ + -1 -4 0\n-1 -7 0\n-1 -10 0\n-4 -7 0\n-4 -10 0\n-7 -10 0\n\ + -2 -5 0\n-2 -8 0\n-2 -11 0\n-5 -8 0\n-5 -11 0\n-8 -11 0\n\ + -3 -6 0\n-3 -9 0\n-3 -12 0\n-6 -9 0\n-6 -12 0\n-9 -12 0\n", + ) + .expect("write non-BCP UNSAT CNF"); + + let binary = env!("CARGO_BIN_EXE_cnc_cuber"); + let run = Command::new(binary) + .arg(&input) + .args(["-n", "1", "-o"]) + .arg(&cubes) + .args([ + "--branch-solver", + "greedy", + "--measure", + "vars", + "--propagation", + "hybrid", + "--trace", + ]) + .arg(&trace) + .output() + .expect("run hybrid cuber"); + assert!(run.status.success(), "{run:?}"); + assert!(fs::read_to_string(&cubes).unwrap().is_empty()); + let records: Vec = fs::read_to_string(&trace) + .unwrap() + .lines() + .map(|line| serde_json::from_str(line).expect("valid trace JSON")) + .collect(); + assert!(!records.is_empty()); + assert!(records + .iter() + .all(|record| record["propagation"] == "hybrid")); + assert!(records + .iter() + .all(|record| record["cdcl_mode"] == "branch-learning")); + let stderr = String::from_utf8_lossy(&run.stderr); + assert!(stderr.contains("propagation=hybrid"), "{stderr}"); + assert!(stderr.contains("full_search_calls=0"), "{stderr}"); + assert!(stderr.contains("learned_total="), "{stderr}"); + + fs::remove_dir_all(dir).expect("remove temp directory"); +} + +#[test] +fn native_regions_can_use_a_matching_flattened_cnf_for_cdcl_propagation() { + let dir = temp_dir(); + fs::create_dir_all(&dir).expect("create temp directory"); + let input = dir.join("xor.json"); + let cnf = dir.join("xor.cnf"); + let ct_cubes = dir.join("ct.cubes"); + let cdcl_cubes = dir.join("cdcl.cubes"); + fs::write( + &input, + r#"{ + "variables": ["a", "b", "c"], + "circuit": {"assignments": [ + {"outputs": ["c"], "expr": {"op": {"Xor": [ + {"op": {"Var": "a"}}, {"op": {"Var": "b"}} + ]}}} + ]} + }"#, + ) + .expect("write CircuitSAT"); + fs::write( + &cnf, + "p cnf 3 4\n-1 -2 -3 0\n1 2 -3 0\n1 -2 3 0\n-1 2 3 0\n", + ) + .expect("write matching Tseitin CNF"); + + let binary = env!("CARGO_BIN_EXE_cnc_cuber"); + let common = [ + "-n", + "3", + "--branch-solver", + "greedy", + "--measure", + "vars", + "--max-rows", + "1", + ]; + let ct = Command::new(binary) + .arg(&input) + .args(["-o"]) + .arg(&ct_cubes) + .args(common) + .output() + .expect("run native CT cuber"); + assert!(ct.status.success(), "{ct:?}"); + + let cdcl = Command::new(binary) + .arg(&input) + .args(["-o"]) + .arg(&cdcl_cubes) + .args(common) + .args(["--propagation", "cdcl", "--propagate-cnf"]) + .arg(&cnf) + .output() + .expect("run native/CDCL cuber"); + assert!(cdcl.status.success(), "{cdcl:?}"); + assert_eq!(fs::read(&ct_cubes).unwrap(), fs::read(&cdcl_cubes).unwrap()); + + fs::remove_dir_all(dir).expect("remove temp directory"); +} + #[test] fn structure_blind_selector_is_auditable_binary_control() { let dir = temp_dir(); @@ -347,7 +587,7 @@ fn root_refutation_trace_records_a_semantic_closure_reason() { let record: serde_json::Value = serde_json::from_str(fs::read_to_string(&trace).unwrap().trim()).unwrap(); assert_eq!(record["kind"], "refuted"); - assert_eq!(record["schema_version"], 2); + assert!(record.get("schema_version").is_none()); assert!(record["rule_diagnostics"].is_null()); assert_eq!( record["refutation_reason"], diff --git a/tests/cnc_streaming.rs b/tests/cnc_streaming.rs index ed08b21..e17e4fa 100644 --- a/tests/cnc_streaming.rs +++ b/tests/cnc_streaming.rs @@ -4,17 +4,21 @@ use std::fs; use std::os::unix::fs::PermissionsExt; use std::path::{Path, PathBuf}; use std::process::Command; +use std::sync::atomic::{AtomicU64, Ordering}; use std::time::{Duration, Instant, SystemTime, UNIX_EPOCH}; use boolean_inference::conquer::{ConquerResult, StreamingConquer}; +static NEXT_TEMP_ID: AtomicU64 = AtomicU64::new(0); + fn temp_dir() -> PathBuf { let nonce = SystemTime::now() .duration_since(UNIX_EPOCH) .expect("clock after epoch") .as_nanos(); + let sequence = NEXT_TEMP_ID.fetch_add(1, Ordering::Relaxed); std::env::temp_dir().join(format!( - "boolean-inference-streaming-{}-{nonce}", + "boolean-inference-streaming-{}-{nonce}-{sequence}", std::process::id() )) } @@ -96,6 +100,150 @@ fn streaming_mode_stops_after_a_sat_cube() { fs::remove_dir_all(dir).unwrap(); } +#[test] +fn conquer_first_answer_interrupts_the_ct_cuber() { + let dir = temp_dir(); + fs::create_dir_all(&dir).unwrap(); + let cnf = dir.join("many-cubes.cnf"); + let mut formula = String::from("p cnf 12 12\n"); + for pair in 0..6 { + let left = pair * 2 + 1; + let right = left + 1; + formula.push_str(&format!("{left} {right} 0\n-{left} -{right} 0\n")); + } + fs::write(&cnf, formula).unwrap(); + + let kissat = dir.join("kissat-first-answer"); + fs::write( + &kissat, + "#!/bin/sh\n\ + [ \"$#\" -eq 1 ] && [ \"$1\" = --relaxed ] || exit 3\n\ + cat >/dev/null\n\ + echo 's SATISFIABLE'\n\ + exit 10\n", + ) + .unwrap(); + let mut permissions = fs::metadata(&kissat).unwrap().permissions(); + permissions.set_mode(0o755); + fs::set_permissions(&kissat, permissions).unwrap(); + + let output = Command::new(env!("CARGO_BIN_EXE_cnc_cuber")) + .arg(&cnf) + .args(["-n", "1", "--solve-cnf"]) + .arg(&cnf) + .args([ + "--kissat", + kissat.to_str().unwrap(), + "--workers", + "1", + "--selector", + "structure-blind", + "--branch-solver", + "greedy", + "--measure", + "vars", + ]) + .output() + .expect("run first-answer CnC"); + + assert_eq!(output.status.code(), Some(10), "{output:?}"); + let stderr = String::from_utf8_lossy(&output.stderr); + assert!( + stderr.contains("status=SAT_EARLY cubes_submitted="), + "{stderr}" + ); + assert!(stderr.contains("sat=1"), "{stderr}"); + fs::remove_dir_all(dir).unwrap(); +} + +#[test] +fn cuber_cdcl_does_not_solve_sat_before_a_cutoff_cube_reaches_conquer() { + let dir = temp_dir(); + fs::create_dir_all(&dir).unwrap(); + let cnf = dir.join("sat.cnf"); + // PHP(3,4) is SAT without a root unit. The cuber-side CaDiCaL may only + // propagate selected branches; a cutoff cube must reach the conquer solver. + fs::write( + &cnf, + "p cnf 12 33\n\ + 1 2 3 4 0\n5 6 7 8 0\n9 10 11 12 0\n\ + -1 -2 0\n-1 -3 0\n-1 -4 0\n-2 -3 0\n-2 -4 0\n-3 -4 0\n\ + -5 -6 0\n-5 -7 0\n-5 -8 0\n-6 -7 0\n-6 -8 0\n-7 -8 0\n\ + -9 -10 0\n-9 -11 0\n-9 -12 0\n-10 -11 0\n-10 -12 0\n-11 -12 0\n\ + -1 -5 0\n-1 -9 0\n-5 -9 0\n-2 -6 0\n-2 -10 0\n-6 -10 0\n\ + -3 -7 0\n-3 -11 0\n-7 -11 0\n-4 -8 0\n-4 -12 0\n-8 -12 0\n", + ) + .unwrap(); + let kissat = dir.join("kissat-sat"); + fs::write( + &kissat, + "#!/bin/sh\n\ + [ \"$#\" -eq 1 ] && [ \"$1\" = --relaxed ] || exit 3\n\ + cat >/dev/null\n\ + echo 's SATISFIABLE'\n\ + exit 10\n", + ) + .unwrap(); + let mut permissions = fs::metadata(&kissat).unwrap().permissions(); + permissions.set_mode(0o755); + fs::set_permissions(&kissat, permissions).unwrap(); + + let output = Command::new(env!("CARGO_BIN_EXE_cnc_cuber")) + .arg(&cnf) + .args(["-n", "1", "--solve-cnf"]) + .arg(&cnf) + .args([ + "--kissat", + kissat.to_str().unwrap(), + "--workers", + "1", + "--branch-solver", + "tail-greedy", + "--measure", + "vars", + "--propagation", + "hybrid", + ]) + .output() + .expect("run branch-learning CnC solver"); + + assert_eq!(output.status.code(), Some(10), "{output:?}"); + let stdout = String::from_utf8_lossy(&output.stdout); + assert!(stdout.contains("s SATISFIABLE"), "{stdout}"); + let stderr = String::from_utf8_lossy(&output.stderr); + assert!( + stderr.contains("status=OK cubes=1") + || (stderr.contains("status=SAT_EARLY cubes_submitted=") + && !stderr.contains("status=SAT_EARLY cubes_submitted=0")), + "{stderr}" + ); + assert!(stderr.contains("full_search_calls=0"), "{stderr}"); + assert!( + stderr.contains("streaming submitted=1 sat=1 unsat=0 errors=0"), + "{stderr}" + ); + fs::remove_dir_all(dir).unwrap(); +} + +#[test] +fn externally_reported_sat_model_stops_workers_and_preserves_the_witness() { + let dir = temp_dir(); + fs::create_dir_all(&dir).unwrap(); + let cnf = dir.join("input.cnf"); + fs::write(&cnf, "p cnf 2 1\n1 2 0\n").unwrap(); + let conquer = StreamingConquer::start(&cnf, &dir.join("must-not-run"), 2).unwrap(); + let witness = "s SATISFIABLE\nv 1 -2 0\n".to_string(); + + conquer.mark_sat_with_witness(witness.clone()); + let summary = conquer.finish(false).unwrap(); + + assert_eq!(summary.result, ConquerResult::Sat); + assert_eq!(summary.sat, 1); + assert_eq!(summary.submitted, 0); + assert_eq!(summary.witness.as_deref(), Some(witness.as_str())); + fs::remove_dir_all(dir).unwrap(); +} + #[test] fn streaming_mode_kills_an_inflight_solver_after_sat() { let dir = temp_dir(); diff --git a/tests/test_cnc_trace_mechanism.py b/tests/test_cnc_trace_mechanism.py index 7e4ab0d..7599fe9 100644 --- a/tests/test_cnc_trace_mechanism.py +++ b/tests/test_cnc_trace_mechanism.py @@ -43,14 +43,17 @@ def rule_record( vector = [] gamma = 1.0 return { - "schema_version": 2, "search_semantics": "sat-decision", + "propagation": "ct", + "cdcl_mode": "off", "node_id": node_id, "parent_id": parent_id, "child_index": child_index, "depth": depth, "kind": "branch", + "optimized_rule_clauses": [{"mask": 0b0011, "value": 0}] * branches, "rule_clauses": [{"mask": 0b0011, "value": 0}] * branches, + "rule_partition_sources": list(range(branches)), "rule_diagnostics": { "rule_semantics": semantics, "region_tensors": 3, @@ -298,18 +301,32 @@ def test_rejects_semantic_contract_corruption(self): with self.assertRaisesRegex(TraceError, "sat-decision"): summarize([record]) + def test_accepts_only_branch_learning_cdcl_for_hybrid_provenance(self): + record = rule_record(0, replay_value=replay()) + record["propagation"] = "hybrid" + record["cdcl_mode"] = "branch-learning" + self.assertEqual(summarize([record])["rule_nodes"], 1) + + record["cdcl_mode"] = "off" + with self.assertRaisesRegex(TraceError, "invalid CDCL search provenance"): + summarize([record]) + def test_links_cutoff_paths_without_treating_cubes_as_instances(self): root = rule_record(0, replay_value=replay()) leaves = [ { - "schema_version": 2, "search_semantics": "sat-decision", + "propagation": "ct", + "cdcl_mode": "off", "node_id": index + 1, "parent_id": 0, "child_index": index, "depth": 1, "kind": "cutoff", "literals": [-1, index + 2], + "optimized_rule_clauses": [], + "rule_clauses": [], + "rule_partition_sources": [], "rule_diagnostics": None, } for index in range(2)