diff --git a/.gitignore b/.gitignore index fadbd5b..be81e1b 100644 --- a/.gitignore +++ b/.gitignore @@ -12,8 +12,11 @@ # Local research and experiment state. /.knowledge/ +/.worktrees/ /experiments/ /artifacts/ +/research/ +/topics.md # Python caches. __pycache__/ diff --git a/Cargo.lock b/Cargo.lock index 64dcc57..3b79c4a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -20,15 +20,6 @@ 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" @@ -41,12 +32,6 @@ 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" @@ -62,7 +47,7 @@ dependencies = [ "bitflags", "cexpr", "clang-sys", - "itertools 0.13.0", + "itertools", "log", "prettyplease", "proc-macro2", @@ -87,8 +72,6 @@ dependencies = [ "optimal-branching", "rayon", "rustc-hash", - "rustsat", - "rustsat-cadical", "serde", "serde_json", "smallvec", @@ -121,8 +104,6 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e228eec9be7c17ccb640b59b36a5cd805ea2a564a4c5e162c2f659fea30d3b96" dependencies = [ "find-msvc-tools", - "jobserver", - "libc", "shlex 2.0.1", ] @@ -141,19 +122,6 @@ 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" @@ -226,22 +194,6 @@ 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" @@ -254,7 +206,7 @@ dependencies = [ "ciborium", "clap", "criterion-plot", - "itertools 0.13.0", + "itertools", "num-traits", "oorandom", "page_size", @@ -274,7 +226,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d8d80a2f4f5b554395e47b5d8305bc3d27813bacb73493eb1001e8f76dae29ea" dependencies = [ "cast", - "itertools 0.13.0", + "itertools", ] [[package]] @@ -314,22 +266,6 @@ 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" @@ -374,21 +310,10 @@ checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd" dependencies = [ "cfg-if", "libc", - "r-efi 5.3.0", + "r-efi", "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" @@ -436,30 +361,6 @@ 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" @@ -469,31 +370,12 @@ 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.99" @@ -522,12 +404,6 @@ 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" @@ -675,12 +551,6 @@ 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" @@ -707,7 +577,7 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" dependencies = [ - "getrandom 0.3.4", + "getrandom", ] [[package]] @@ -765,48 +635,6 @@ 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" @@ -909,19 +737,6 @@ 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" @@ -1032,16 +847,6 @@ dependencies = [ "wasm-bindgen", ] -[[package]] -name = "web-time" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a6580f308b1fad9207618087a65c04e7a10bc77e02c8e84e9b00dd4b12fa0bb" -dependencies = [ - "js-sys", - "wasm-bindgen", -] - [[package]] name = "wide" version = "1.5.0" @@ -1083,65 +888,12 @@ 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 7b934d3..db97513 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -18,10 +18,6 @@ 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 cb9ba27..8460fad 100644 --- a/benchmarks/cnc/README.md +++ b/benchmarks/cnc/README.md @@ -59,29 +59,10 @@ 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. +Cubing is entirely native. Region construction, feasibility probes, +OptimalBranching candidate evaluation, committed-branch propagation, +domination, and failed-literal reduction all operate on the Compact-Table +constraint network. The flattened CNF does not participate in cubing. Before descending, the cuber converts the optimizer's potentially overlapping DNF cover into an equivalent pairwise-disjoint DNF. Consequently the emitted @@ -90,18 +71,12 @@ 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 +A native 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. +for a root contradiction proved by native propagation). For CircuitSAT input, +`--solve-cnf` supplies the canonical flattened CNF used only by Kissat. Both `--branch-solver` and `--measure` are mandatory so an artifact cannot silently inherit a changed default. `--branch-solver tail-greedy` starts from @@ -109,8 +84,8 @@ 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`. -The trace records propagation/CDCL provenance, the selected `measure`, and -`rule_diagnostics` for every structure-aware branch: +The trace records 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 diff --git a/benchmarks/cnc/trace_mechanism.py b/benchmarks/cnc/trace_mechanism.py index 70f94d9..f17e8f3 100644 --- a/benchmarks/cnc/trace_mechanism.py +++ b/benchmarks/cnc/trace_mechanism.py @@ -171,16 +171,6 @@ 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("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"): diff --git a/src/adapter.rs b/src/adapter.rs index 1be8bf9..d18a503 100644 --- a/src/adapter.rs +++ b/src/adapter.rs @@ -23,7 +23,6 @@ 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}; @@ -82,20 +81,13 @@ 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`. Candidate propagation uses either the optional -/// shared CDCL engine or CT via the thread-local measure scratch. +/// deep-copies only `doms`. CT tables are shared via `masks` so `apply_branch` +/// can propagate with 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 { @@ -104,19 +96,7 @@ impl RuleProblem { masks: Arc>, doms: Vec, ) -> RuleProblem { - 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 + RuleProblem { cn, masks, doms } } } @@ -131,11 +111,11 @@ impl BranchAndReduceProblem for RuleProblem { self.doms.iter().all(|d| d.is_fixed()) } - /// 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`. + /// 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. 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, @@ -143,22 +123,15 @@ 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 = 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) - }), - }; + let snapshot = 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, ) @@ -168,9 +141,9 @@ impl BranchAndReduceProblem for RuleProblem { /// Propagate `clause` over `variables` on the measure scratch `s` from its base, /// returning the resulting domains and restoring `s` to base — exactly a /// `probe` with a domain-snapshot read (the adapter test pins the equality). -/// This is a PURE function of `(clause.mask, clause.val)` given the fixed node +/// This is a pure function of `(clause.mask, clause.val)` given the fixed node /// base (`s.doms`, `s.tables`), the constant `variables` slice, and immutable -/// `cn`/`masks` — the determinism the per-node `cache` relies on. +/// `cn`/`masks`. fn apply_branch_fresh( cn: &ConstraintNetwork, masks: &[TableMasks], @@ -251,10 +224,7 @@ 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; @@ -333,36 +303,6 @@ 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 60f0265..0290613 100644 --- a/src/bin/cnc_cuber.rs +++ b/src/bin/cnc_cuber.rs @@ -10,14 +10,12 @@ 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_configured, generate_cubes_configured_with_trace, CdclIntegrationMode, - CncSatPolicy, CubeCdclOptions, CubeCutoff, CubeGenerationOptions, CubeNodeKind, CubeNodeTrace, - CubeRefutationReason, + generate_cubes_configured, generate_cubes_configured_with_trace, CncSatPolicy, CubeCutoff, + CubeGenerationOptions, CubeNodeKind, CubeNodeTrace, CubeRefutationReason, }; use boolean_inference::dimacs::network_from_dimacs; use boolean_inference::measure::Measure; @@ -32,7 +30,6 @@ const USAGE: &str = (-o | --solve-cnf --kissat --workers ) \ --branch-solver \ --measure \ - [--propagation ] [--propagate-cnf ] \ [--selector ] \ [--max-rows ] [--trace ] [--trace-replay]"; @@ -42,41 +39,6 @@ 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 { @@ -128,14 +90,12 @@ 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, @@ -158,7 +118,6 @@ 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; @@ -167,7 +126,6 @@ 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; @@ -195,7 +153,6 @@ 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")?; @@ -222,9 +179,6 @@ 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 @@ -263,21 +217,10 @@ fn parse_args() -> Result { return Err("--trace-replay requires --selector region".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, @@ -288,7 +231,6 @@ 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, @@ -335,7 +277,6 @@ 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", } } @@ -347,8 +288,6 @@ 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 @@ -427,8 +366,6 @@ fn write_trace_node( "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, @@ -536,8 +473,6 @@ 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, )?; trace_writer @@ -547,14 +482,11 @@ 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={} propagation={} cdcl_mode={} \ - max_rows={}", + selector={} branch_solver={} measure={} 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() { @@ -567,21 +499,6 @@ 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 { @@ -660,10 +577,6 @@ fn run(args: Args) -> Result { }; let generation_options = CubeGenerationOptions { cutoff: args.cutoff, - cdcl: cdcl.as_ref().map(|cdcl| CubeCdclOptions { - propagator: cdcl.clone(), - integration: cdcl_integration, - }), sat_policy, termination, }; @@ -683,8 +596,6 @@ 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, ) }, @@ -699,7 +610,6 @@ fn run(args: Args) -> Result { ), }; 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, @@ -726,8 +636,7 @@ 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={} \ - propagation={} cdcl_mode={} max_rows={}", + root_unfixed={} remaining_range={} selector={} branch_solver={} measure={} max_rows={}", stats.cubes, stats.refuted, stats.sat_leaves, @@ -738,8 +647,6 @@ 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; @@ -751,31 +658,12 @@ fn run(args: Args) -> Result { } } else { eprintln!( - "status=SAT_EARLY cubes_submitted={} cutoff={:?} selector={} branch_solver={} \ - measure={} propagation={} cdcl_mode={}", + "status=SAT_EARLY cubes_submitted={} cutoff={:?} selector={} branch_solver={} measure={}", emitted, args.cutoff, args.selector.label(), args.branch_solver.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 + args.measure.label() ); } if let Some(conquer) = conquer.take() { diff --git a/src/cdcl.rs b/src/cdcl.rs deleted file mode 100644 index 3dfc253..0000000 --- a/src/cdcl.rs +++ /dev/null @@ -1,419 +0,0 @@ -//! 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/cube.rs b/src/cube.rs index 20b4147..1c43119 100644 --- a/src/cube.rs +++ b/src/cube.rs @@ -16,15 +16,11 @@ //! propagation itself. Each cube also carries `sigma_dec`/`sigma_all` so the //! emitted frontier can be audited. -use std::convert::Infallible; use std::num::NonZeroUsize; use std::sync::Arc; use crate::adapter::BranchSolver; -use crate::cdcl::CdclPropagator; -use crate::ct::{ - apply_masked_assignment, ct_propagate, enqueue_var_change, RSparseBitSet, TableMasks, -}; +use crate::ct::{apply_masked_assignment, ct_propagate, RSparseBitSet, TableMasks}; use crate::domain::DomainMask; use crate::measure::Measure; use crate::network::ConstraintNetwork; @@ -74,7 +70,6 @@ pub enum CubeRefutationReason { RootPropagation, SelectorNoFeasibleConfig, BranchPropagation, - CdclPropagationConflict, } /// One branching clause in the bit encoding over `CubeNodeTrace::variables`. @@ -118,20 +113,11 @@ 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; @@ -151,17 +137,6 @@ 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 { @@ -172,19 +147,10 @@ pub enum CncSatPolicy { 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. +/// Orthogonal generation policies collected in one value. #[derive(Clone)] pub struct CubeGenerationOptions { pub cutoff: CubeCutoff, - pub cdcl: Option, pub sat_policy: CncSatPolicy, pub termination: Option, } @@ -193,7 +159,6 @@ impl CubeGenerationOptions { pub fn new(cutoff: CubeCutoff) -> Self { Self { cutoff, - cdcl: None, sat_policy: CncSatPolicy::CompleteFrontier, termination: None, } @@ -213,62 +178,6 @@ impl CubeCutoff { } } -/// Generate a satisfiability-preserving cube frontier of `problem` using -/// march_cu's static `-n` cutoff: -/// emit the current decision path when fewer than `cutoff_vars` variables remain -/// unfixed. The comparison is strict, exactly as in march_cu's static mode; -/// `cutoff_vars` is nonzero because march_cu reserves zero for dynamic mode. -/// -/// The problem's root propagation must already have run (as after -/// `from_network`). Returns the open cubes (to hand to a conquer solver) and -/// generation stats. Refuted and SAT leaves are included in the returned -/// vector, flagged, so callers can audit SAT-equivalence and provenance. -/// -/// New experiments should call [`generate_cubes_with_cutoff`] with -/// [`CubeCutoff::CcDifficulty`]. This wrapper remains for compatibility and -/// remaining-variable ablations. -pub fn generate_cubes( - problem: &mut TnProblem, - selector: Selector, - measure: Measure, - solver: &BranchSolver, - cutoff_vars: NonZeroUsize, -) -> (Vec, CubeStats) { - let mut cubes = Vec::new(); - let stats = match generate_cubes_with(problem, selector, measure, solver, cutoff_vars, |cube| { - cubes.push(cube); - Ok::<(), Infallible>(()) - }) { - Ok(stats) => stats, - Err(error) => match error {}, - }; - (cubes, stats) -} - -/// Streaming form of [`generate_cubes`]. Each open, refuted, or SAT leaf is -/// passed to `emit` as soon as it is reached, so production cubers need not keep -/// the entire frontier and every cloned decision path in memory. -pub fn generate_cubes_with( - problem: &mut TnProblem, - selector: Selector, - measure: Measure, - solver: &BranchSolver, - cutoff_vars: NonZeroUsize, - emit: F, -) -> Result -where - F: FnMut(Cube) -> Result<(), E>, -{ - generate_cubes_with_cutoff( - problem, - selector, - measure, - solver, - CubeCutoff::RemainingVars(cutoff_vars), - emit, - ) -} - /// Streaming generation under either supported online stopping rule. pub fn generate_cubes_with_cutoff( problem: &mut TnProblem, @@ -291,8 +200,8 @@ where ) } -/// 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. +/// Primary streaming entry point. A conquer worker can stop native cubing +/// through the shared termination signal. pub fn generate_cubes_configured( problem: &mut TnProblem, selector: Selector, @@ -315,156 +224,6 @@ where ) } -/// 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. -pub fn generate_cubes_with_trace( - problem: &mut TnProblem, - selector: Selector, - measure: Measure, - solver: &BranchSolver, - cutoff_vars: NonZeroUsize, - emit: F, - trace: T, -) -> Result -where - F: FnMut(Cube) -> Result<(), E>, - T: FnMut(CubeNodeTrace) -> Result<(), E>, -{ - generate_cubes_with_cutoff_trace( - problem, - selector, - measure, - solver, - CubeCutoff::RemainingVars(cutoff_vars), - emit, - trace, - ) -} - /// Traced generation under either supported online stopping rule. pub fn generate_cubes_with_cutoff_trace( problem: &mut TnProblem, @@ -475,36 +234,6 @@ pub fn generate_cubes_with_cutoff_trace( 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>, @@ -514,117 +243,12 @@ where 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, + CubeGenerationOptions::new(cutoff), 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, @@ -664,10 +288,6 @@ 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, @@ -678,8 +298,6 @@ where measure, solver, cutoff: options.cutoff, - cdcl, - cdcl_integration, sat_policy: options.sat_policy, termination, }; @@ -694,8 +312,6 @@ 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 ctx.should_stop_for_sat() { @@ -708,11 +324,7 @@ where child_index: None, depth: 0, kind: CubeNodeKind::Refuted, - refutation_reason: Some(if root_cdcl_refuted { - CubeRefutationReason::CdclPropagationConflict - } else { - CubeRefutationReason::RootPropagation - }), + refutation_reason: Some(CubeRefutationReason::RootPropagation), decisions: Vec::new(), sigma_dec: 0, sigma_all: 0, @@ -895,8 +507,6 @@ where tables, trail, &scope, - ctx.candidate_cdcl(), - decisions, trace.is_some(), ); if ctx.should_stop_for_sat() { @@ -1006,11 +616,7 @@ where } } apply_masked_assignment(ctx.cn, doms, buffer, trail, &variables, cl.mask, cl.val); - // 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); + ct_propagate(ctx.cn, doms, masks, tables, buffer, trail); 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); @@ -1035,11 +641,7 @@ where child_index: Some(branch_index), depth: depth + 1, kind: CubeNodeKind::Refuted, - refutation_reason: Some(if cdcl_refuted { - CubeRefutationReason::CdclPropagationConflict - } else { - CubeRefutationReason::BranchPropagation - }), + refutation_reason: Some(CubeRefutationReason::BranchPropagation), decisions: decisions.clone(), sigma_dec: decisions.len(), sigma_all: doms.len() - branch_freevars, @@ -1155,73 +757,13 @@ fn subtract_clause( 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 std::convert::Infallible; + 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"; @@ -1261,148 +803,60 @@ mod tests { fn static_n_controls_the_emitted_frontier() { let mut root_cut = xor_chain(); assert_eq!(root_cut.count_unfixed(), 3); - let (root_cubes, root_stats) = generate_cubes( + let mut root_cubes = Vec::new(); + let root_stats = generate_cubes_with_cutoff( &mut root_cut, Selector::MostOccurrence { max_rows: 32 }, Measure::NumUnfixedVars, &BranchSolver::Greedy(GreedyMerge), - n(4), - ); + CubeCutoff::RemainingVars(n(4)), + |cube| { + root_cubes.push(cube); + Ok::<(), Infallible>(()) + }, + ) + .expect("infallible callback"); assert_eq!(root_stats.cubes, 1); assert!(root_cubes[0].decisions.is_empty()); let mut strict = xor_chain(); - let (strict_cubes, strict_stats) = generate_cubes( + let mut strict_cubes = Vec::new(); + let strict_stats = generate_cubes_with_cutoff( &mut strict, Selector::MostOccurrence { max_rows: 32 }, Measure::NumUnfixedVars, &BranchSolver::Greedy(GreedyMerge), - n(3), - ); - assert!(strict_stats.cubes >= 1); - assert!(strict_cubes - .iter() - .filter(|c| !c.refuted && !c.sat) - .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); + strict_cubes.push(cube); 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); + .expect("infallible callback"); + assert!(strict_stats.cubes >= 1); + assert!(strict_cubes + .iter() + .filter(|c| !c.refuted && !c.sat) + .all(|c| !c.decisions.is_empty())); } #[test] - fn decision_policy_honors_a_conquer_stop_without_cdcl() { + fn decision_policy_honors_a_conquer_stop() { let signal = TerminationSignal::new(); signal.request(); let mut problem = xor_chain(); let mut cubes = Vec::new(); - let stats = generate_cubes_with_cutoff_policy( + let stats = generate_cubes_configured( &mut problem, Selector::MostOccurrence { max_rows: 1 }, Measure::NumUnfixedVars, &BranchSolver::Greedy(GreedyMerge), - CubeCutoff::RemainingVars(n(3)), - CncSatPolicy::StopDecision, - Some(signal), + CubeGenerationOptions { + cutoff: CubeCutoff::RemainingVars(n(3)), + sat_policy: CncSatPolicy::StopDecision, + termination: Some(signal), + }, |cube| { cubes.push(cube); Ok::<(), Infallible>(()) @@ -1437,21 +891,26 @@ mod tests { .all(|cube| cube.sigma_dec * cube.sigma_all > 0)); } - /// march_cu checks its static cutoff before declaring a solved leaf. Lock - /// that compatibility behavior: a root-solved instance emits `a 0` at any - /// valid static `-n` rather than being counted as a SAT leaf. + /// march_cu checks its static cutoff before declaring a solved leaf, so a + /// root-solved instance emits `a 0` at any valid static `-n`. #[test] fn root_solved_instance_emits_the_empty_cube() { let cn = network_from_dimacs("p cnf 1 1\n1 0\n").expect("parse"); let mut p = TnProblem::from_network(cn).expect("root SAT"); assert_eq!(p.count_unfixed(), 0); - let (cubes, stats) = generate_cubes( + let mut cubes = Vec::new(); + let stats = generate_cubes_with_cutoff( &mut p, Selector::MostOccurrence { max_rows: 32 }, Measure::NumUnfixedVars, &BranchSolver::Greedy(GreedyMerge), - n(1), - ); + CubeCutoff::RemainingVars(n(1)), + |cube| { + cubes.push(cube); + Ok::<(), Infallible>(()) + }, + ) + .expect("infallible callback"); assert_eq!(stats.cubes, 1); assert_eq!(stats.sat_leaves, 0); assert!(cubes[0].decisions.is_empty()); @@ -1461,12 +920,12 @@ mod tests { fn streaming_callback_error_restores_the_search_state() { let mut p = xor_chain(); let root_doms = p.doms.clone(); - let result = generate_cubes_with( + let result = generate_cubes_with_cutoff( &mut p, Selector::MostOccurrence { max_rows: 32 }, Measure::NumUnfixedVars, &BranchSolver::Greedy(GreedyMerge), - n(3), + CubeCutoff::RemainingVars(n(3)), |_| Err("stop"), ); assert_eq!(result.unwrap_err(), "stop"); @@ -1476,24 +935,30 @@ mod tests { #[test] fn tracing_preserves_frontier_and_records_a_tree() { let mut plain = xor_chain(); - let (plain_cubes, plain_stats) = generate_cubes( + let mut plain_cubes = Vec::new(); + let plain_stats = generate_cubes_with_cutoff( &mut plain, Selector::MostOccurrence { max_rows: 32 }, Measure::NumUnfixedVars, &BranchSolver::Greedy(GreedyMerge), - n(3), - ); + CubeCutoff::RemainingVars(n(3)), + |cube| { + plain_cubes.push(cube); + Ok::<(), Infallible>(()) + }, + ) + .expect("infallible callback"); let mut traced = xor_chain(); let root_doms = traced.doms.clone(); let mut traced_cubes = Vec::new(); let mut nodes = Vec::new(); - let traced_stats = generate_cubes_with_trace( + let traced_stats = generate_cubes_with_cutoff_trace( &mut traced, Selector::MostOccurrence { max_rows: 32 }, Measure::NumUnfixedVars, &BranchSolver::Greedy(GreedyMerge), - n(3), + CubeCutoff::RemainingVars(n(3)), |cube| { traced_cubes.push(cube); Ok::<(), Infallible>(()) diff --git a/src/lib.rs b/src/lib.rs index 4fd38fa..c00c780 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,7 +1,6 @@ pub mod adapter; pub mod api; pub mod canonicalize; -pub mod cdcl; pub mod circuit; pub mod conquer; pub mod contract; diff --git a/src/selector.rs b/src/selector.rs index 4955dc8..fcdf571 100644 --- a/src/selector.rs +++ b/src/selector.rs @@ -3,13 +3,12 @@ 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::BranchingResult; +use crate::table::{compute_branching_result, BranchingResult}; use crate::trail::Trail; use crate::util::{active_tensors, is_entailed}; @@ -149,8 +148,6 @@ 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); @@ -198,7 +195,7 @@ impl Selector { diagnostics: None, }; } - crate::table::compute_branching_result_with_cdcl( + compute_branching_result( cn, doms, buffer, @@ -209,8 +206,6 @@ impl Selector { masks, tables, trail, - cdcl, - cdcl_decisions, collect_diagnostics || self.replays_same_state(), self.replays_same_state(), ) @@ -300,8 +295,6 @@ mod tests { &mut tables, &mut trail, &[0, 1], - None, - &[], false, ); assert_eq!(result.variables, vec![0, 1]); @@ -335,8 +328,6 @@ mod tests { &mut tables, &mut trail, &[0, 1, 2, 3], - None, - &[], false, ); assert!(result.clauses.is_some()); @@ -353,8 +344,6 @@ 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 08ad747..9fe9667 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -104,8 +104,6 @@ fn bbsat_rec( tables, trail, scope, - None, - &[], false, ); let clauses = match selection.clauses { diff --git a/src/table.rs b/src/table.rs index 4b47534..a7e0d1e 100644 --- a/src/table.rs +++ b/src/table.rs @@ -4,7 +4,6 @@ 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; @@ -161,44 +160,6 @@ 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 @@ -276,7 +237,7 @@ pub fn compute_branching_result_with_cdcl( 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 = rule_problem(cn, masks, doms, cdcl, cdcl_decisions); + let problem = RuleProblem::new(Arc::clone(cn), Arc::clone(masks), doms.to_vec()); Some(with_measure_scratch(doms, tables, buffer, trail, || { replay_same_state(&problem, &table, ®ion_vars, var_id, measure) })) @@ -314,11 +275,11 @@ pub fn compute_branching_result_with_cdcl( // 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 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. + // produce the rule through this one call. `apply_branch` always uses + // native CT propagation. + let problem = RuleProblem::new(Arc::clone(cn), Arc::clone(masks), doms.to_vec()); + // Keep CT scratch primed for candidate evaluation and replay. The live + // `doms`/`tables`/`buffer`/`trail` remain unchanged. let (result, rule_solver_ns, same_state_replay) = with_measure_scratch(doms, tables, buffer, trail, || { let rule_start = collect_diagnostics.then(Instant::now); @@ -369,20 +330,6 @@ pub fn compute_branching_result_with_cdcl( } } -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 index fb72a62..671b93f 100644 --- a/src/termination.rs +++ b/src/termination.rs @@ -3,8 +3,7 @@ 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. +/// A clone-cheap stop signal shared by the cuber and all conquer workers. #[derive(Clone, Debug, Default)] pub struct TerminationSignal { requested: Arc, diff --git a/tests/cnc_cuber_trace.rs b/tests/cnc_cuber_trace.rs index ba8ee23..d4bead1 100644 --- a/tests/cnc_cuber_trace.rs +++ b/tests/cnc_cuber_trace.rs @@ -126,8 +126,12 @@ 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.get("propagation").is_none())); + assert!(records + .iter() + .all(|record| record.get("cdcl_mode").is_none())); assert!(records .iter() .all(|record| record["input_kind"] == "dimacs")); @@ -211,242 +215,6 @@ 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(); diff --git a/tests/cnc_streaming.rs b/tests/cnc_streaming.rs index e17e4fa..a2f905e 100644 --- a/tests/cnc_streaming.rs +++ b/tests/cnc_streaming.rs @@ -156,75 +156,6 @@ fn conquer_first_answer_interrupts_the_ct_cuber() { 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(); diff --git a/tests/test_cnc_trace_mechanism.py b/tests/test_cnc_trace_mechanism.py index 7599fe9..dbc99d2 100644 --- a/tests/test_cnc_trace_mechanism.py +++ b/tests/test_cnc_trace_mechanism.py @@ -44,8 +44,6 @@ def rule_record( gamma = 1.0 return { "search_semantics": "sat-decision", - "propagation": "ct", - "cdcl_mode": "off", "node_id": node_id, "parent_id": parent_id, "child_index": child_index, @@ -301,23 +299,11 @@ 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 = [ { "search_semantics": "sat-decision", - "propagation": "ct", - "cdcl_mode": "off", "node_id": index + 1, "parent_id": 0, "child_index": index,