Add persistent CDCL-assisted cube generation

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 = []

benchmarks/cnc/README.md

@@ -59,16 +59,65 @@ DIMACS. The `.csp` format retains each `<scope> : <allowed configurations>`
 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

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,23 +288,23 @@ 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":
         if (
             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
         ):
             raise TraceError(f"record {index}: inconsistent closed-witness semantics")
     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]

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<R>(
 
 /// 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<ConstraintNetwork>,
     pub masks: Arc<Vec<TableMasks>>,
     pub doms: Vec<DomainMask>,
+    /// 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<CdclPropagator>,
+    /// 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<Vec<TableMasks>>,
         doms: Vec<DomainMask>,
     ) -> 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,29 +131,34 @@ 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,
     /// upstream of this call and covering the measure too, so a downstream cache
     /// 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<DomainMask>) -> 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();