From f36f0794dc0db24c99793ee047658ce0a6daf621 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Wed, 4 Nov 2026 00:50:36 -0800 Subject: [PATCH] Fix #1202: BoyceCoddNormalFormViolation to Satisfiability Co-Authored-By: Claude Sonnet 5.5 --- docs/paper/reductions.typ | 108 ++++ ...ecoddnormalformviolation_satisfiability.rs | 218 +++++++ src/rules/mod.rs | 2 + ...ecoddnormalformviolation_satisfiability.rs | 532 ++++++++++++++++++ 4 files changed, 860 insertions(+) create mode 100644 src/rules/boycecoddnormalformviolation_satisfiability.rs create mode 100644 src/unit_tests/rules/boycecoddnormalformviolation_satisfiability.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 8e0462b7a..7513afc47 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -20306,6 +20306,114 @@ The following table shows concrete target-variable counts for example instances, _Boundary cases._ When $k=0$, the target has only terminal $r$; the edge-free tree maps to the empty source forest of cost zero. The same construction works when $beta=0$ or $omega=0$. Gadget costs use checked integer arithmetic. ] +// BoyceCoddNormalFormViolation → Satisfiability (#1202) +#let bcnf_sat = load-example("BoyceCoddNormalFormViolation", "Satisfiability") +#let bcnf_sat_sol = bcnf_sat.solutions.at(0) +#reduction-rule("BoyceCoddNormalFormViolation", "Satisfiability", + example: true, + example-caption: [$N = #bcnf_sat.source.instance.num_attributes$ attributes, $r = #bcnf_sat.source.instance.target_subset.len()$ target attributes], + extra: [ + #pred-commands( + "pred create --example " + rule-spec(bcnf_sat) + " -o bcnf.json", + "pred reduce bcnf.json --via route.json -o bundle.json", + "pred solve bundle.json", + "pred evaluate bcnf.json --config " + cli-config(bcnf_sat_sol.source_config), + ) + + #{ + // Everything below is computed from the loaded fixture. + let closure-of(fds, start) = { + let cur = start + let changed = true + while changed { + changed = false + for fd in fds { + if fd.at(0).all(a => cur.contains(a)) { + for a in fd.at(1) { + if not cur.contains(a) { + cur.push(a) + changed = true + } + } + } + } + } + cur.sorted() + } + let inst = bcnf_sat.source.instance + let n = inst.num_attributes + let fds = inst.functional_deps + let rset = inst.target_subset + let r = rset.len() + let d = fds.len() + let sel = bcnf_sat_sol.source_config + let X = range(r).filter(i => sel.at(i)).map(i => rset.at(i)) + let cl = closure-of(fds, X) + let gained = rset.filter(a => not X.contains(a) and cl.contains(a)) + let missing = rset.filter(a => not cl.contains(a)) + let big-l = fds.map(fd => fd.at(0).len()).sum() + let big-b = fds.map(fd => fd.at(1).len()).sum() + let tgt = bcnf_sat.target.instance + let tcfg = bcnf_sat_sol.target_config + assert(tgt.num_vars == n * (n + 1) + n * d + 2 * r) + assert(tgt.clauses.len() == n + 4 * r + n * (big-l + big-b + d + 2 * n) + 2) + assert(tcfg.len() == tgt.num_vars) + assert(gained.len() > 0 and missing.len() > 0) + let layer(t) = range(n).map(a => if tcfg.at(r + t * n + a) { "1" } else { "0" }).join() + let trig(t) = range(d).map(k => if tcfg.at(r + (n + 1) * n + t * d + k) { "1" } else { "0" }).join() + let outside = range(n).filter(a => not rset.contains(a)) + let first-layer = if outside.len() > 0 { range(n + 1).position(t => tcfg.at(r + t * n + outside.at(0))) } else { none } + assert(outside.len() == 0 or first-layer != none) + let gains = range(r).map(i => if tcfg.at(r + (n + 1) * n + n * d + i) { "1" } else { "0" }).join() + // The NO example: a dependency cycle over three target attributes. + let no-fds = ((range(1), range(1, 2)), (range(1, 2), range(2, 3)), (range(2, 3), range(1))) + let no-n = 3 + let no-sets = range(8).map(m => range(no-n).filter(a => calc.rem(calc.quo(m, calc.pow(2, a)), 2) == 1)) + let no-gain-and-miss(x) = { + let c = closure-of(no-fds, x) + range(no-n).any(a => not x.contains(a) and c.contains(a)) and range(no-n).any(a => not c.contains(a)) + } + let no-d = no-fds.len() + let no-r = no-n + let no-l = no-fds.map(fd => fd.at(0).len()).sum() + let no-b = no-fds.map(fd => fd.at(1).len()).sum() + let no-vars = no-n * (no-n + 1) + no-n * no-d + 2 * no-r + let no-clauses = no-n + 4 * no-r + no-n * (no-l + no-b + no-d + 2 * no-n) + 2 + let no-lits = no-n + 12 * no-r + no-n * (3 * no-l + 3 * no-b + no-d + 4 * no-n) + assert((no-vars, no-clauses, no-lits) == (27, 62, 138)) + assert(no-sets.all(x => not no-gain-and-miss(x))) + // Each selection: either no attribute is gained (empty selection) or none is missing (closure is R). + assert(no-sets.all(x => if x.len() == 0 { closure-of(no-fds, x).len() == 0 } else { closure-of(no-fds, x).len() == no-n })) + assert(closure-of(no-fds, ()).len() == 0) + assert(no-sets.filter(x => x.len() > 0).all(x => closure-of(no-fds, x).len() == no-n)) + [ + *Step 1 -- Source.* $N = #n$ attributes, $F = {#fds.map(fd => $#fd.at(0).map(a => $a_#a$).join(",") arrow.r #fd.at(1).map(a => $a_#a$).join(",")$).join(", ")}$, and $R = {#rset.map(a => $a_#a$).join(", ")}$, so $r = #r$, $D = #d$, $L = #big-l$, $B = #big-b$. The canonical witness selects $X = {#X.map(a => $a_#a$).join(", ")}$. + + *Step 2 -- Target size.* The CNF has $N(N+1) + N D + 2 r = #tgt.num_vars$ variables (#r selection, #((n + 1) * n) closure, #(n * d) trigger, #r gain bits), $N + 4 r + N (L + B + D + 2 N) + 2 = #tgt.clauses.len()$ clauses, and $N + 12 r + N (3 L + 3 B + D + 4 N) = #tgt.clauses.map(c => c.literals.len()).sum()$ literal occurrences. + + *Step 3 -- Closure layers.* Over $a_0, dots, a_#(n - 1)$ the layers $c_0, dots, c_#n$ are #(range(n + 1).map(layer).join(", "))\; the trigger vectors for rounds $0, dots, #(n - 1)$ are #(range(n).map(trig).join(", ")). The last layer is $X^+ = {#cl.map(a => $a_#a$).join(", ")}$. #if outside.len() > 0 [Attribute #outside.map(a => $a_#a$).join(", ") lies outside $R$: it keeps a closure bit in every layer, enters at layer #first-layer, and no gain bit reads it.] + + *Step 4 -- Gain and missing attributes.* The gain bits over $R$ are #gains: the gained attribute is #gained.map(a => $a_#a$).join(", ") and the missing one is #missing.map(a => $a_#a$).join(", "). Both final clauses hold, and the complete vector #fmt-values(tcfg) satisfies the CNF; extraction returns its first $r$ bits #fmt-values(sel). + + *NO example.* Take $N = 3$, $F = {a_0 arrow.r a_1, a_1 arrow.r a_2, a_2 arrow.r a_0}$, $R = {a_0, a_1, a_2}$. The empty selection has empty closure (every left side is nonempty), so no attribute is gained; each of the other #(no-sets.len() - 1) selections has closure $R$, so no attribute is missing. Hence the source has no solution. The target has $N(N+1) + N D + 2 r = #no-vars$ variables, $N + 4 r + N (L + B + D + 2 N) + 2 = #no-clauses$ clauses, and $N + 12 r + N (3 L + 3 B + D + 4 N) = #no-lits$ literal occurrences. Every selection fixes all auxiliary bits, and the corresponding assignment violates a final clause, so the CNF is unsatisfiable. + ] + } + ], +)[ + Unroll the least functional-dependency closure of the selected attributes into $N$ layers of a Boolean circuit and require, with two final clauses, a gained target attribute and a missing one. The target has $N(N+1) + N D + 2 r$ variables and at most $N + 4 r + N(2 N D + D + 2 N) + 2$ clauses, where $N$ is the number of attributes, $D$ the number of dependencies and $r = |R|$. Layered closure circuits are a standard technique#footnote[The construction is derived directly from the closure predicate of the source problem; it is not taken from a published reduction.]. +][ + _Construction._ Let $A = {0, dots, N-1}$, $F = ((L_d, R_d))_(d=0)^(D-1)$, $R subset.eq A$ nonempty with $r = |R|$, and let $L = sum_d |L_d|$, $B = sum_d |R_d|$ after normalization. Number the variables: selection bits $x_a$ ($a in R$, in sorted order); closure bits $c_(t,a)$ for $t = 0, dots, N$ and every $a in A$ (round-major); trigger bits $g_(t,d)$ for $t < N$; gain bits $w_a$ ($a in R$). Emit: + 1. $c_(0,a) <-> x_a$ for $a in R$ (two binary clauses) and the unit $not c_(0,a)$ for $a in.not R$. + 2. For each round $t < N$: $g_(t,d) <-> and.big_(a in L_d) c_(t,a)$ (one binary clause per $a in L_d$ and one long clause), and $c_(t+1,a) <-> c_(t,a) or or.big_(d : a in R_d) g_(t,d)$ (one binary clause per disjunct and one long clause); the previous-round bit is always a disjunct. + 3. $w_a <-> (not x_a and c_(N,a))$ for $a in R$ (three clauses). + 4. The clauses $(or.big_(a in R) w_a)$ and $(or.big_(a in R) not c_(N,a))$. + Attributes outside $R$ keep their layer bits, since a derivation may pass through them. Variables: $N(N+1) + N D + 2r$ (exact); clauses $N + 4r + N(L + B + D + 2N) + 2$ and literals $N + 12 r + N(3L + 3B + D + 4N)$, bounded using $L + B <= 2 N D$. + + _Correctness._ Fix $X = {a in R : x_a}$. The initial clauses force $c_0 = X$; given layer $t$, the equivalence gates force $g_(t,d)$ to hold exactly when $L_d$ lies in layer $t$ and layer $t+1$ to be layer $t$ together with every right side of a firing dependency. This iteration is increasing, each changing round adds at least one of the $N$ attributes, and an unchanged layer is a closed set containing $X$ reachable by derivations from $X$, so layer $N$ is exactly the least closure $X^+$. ($arrow.r.double$) For a solution $X$, assign the selection bits, the successive layers, the trigger truths, and $w_a = [a in.not X and a in X^+]$; every gate holds, a gained attribute $a in (X^+ without X) inter R$ makes $w_a$ true, and a missing attribute $b in R without X^+$ makes $not c_(N,b)$ true. ($arrow.l.double$) For a satisfying assignment, $X$ is read from the selection bits and layer $N$ equals $X^+$ by the argument above. A true gain bit gives $a in (X^+ without X) inter R$; the second final clause gives $b in R$ with $b in.not X^+$, and $b in.not X$ because $X subset.eq X^+$. So $X$ is a solution. All auxiliary bits are determined by $X$, so satisfying assignments correspond one-to-one with source solutions. Empty dependency lists, empty right sides, and $X = emptyset$ (every left side is nonempty, so the closure is empty and no attribute is gained) are covered by the same argument. + + _Solution extraction._ Evaluate the target witness once; if it does not satisfy the CNF, reject it. Otherwise return the first $r$ bits, which are already in the source's sorted order of $R$. +] + #pagebreak() #if export-details { detail-article("references")[#bibliography("references.bib", style: "ieee")] diff --git a/src/rules/boycecoddnormalformviolation_satisfiability.rs b/src/rules/boycecoddnormalformviolation_satisfiability.rs new file mode 100644 index 000000000..034522586 --- /dev/null +++ b/src/rules/boycecoddnormalformviolation_satisfiability.rs @@ -0,0 +1,218 @@ +//! Reduction from Boyce-Codd Normal Form Violation to Satisfiability. +//! +//! The target unrolls the least functional-dependency closure of the selected +//! attribute set into `N` synchronous layers. Every gate is a full equivalence, +//! so the final layer is exactly the closure `X⁺` of the selection `X`. +//! Two final clauses demand a gained target attribute and a missing one. +//! +//! Variables, in order (one-based): selection bits `x_a` for `a ∈ R`; closure +//! bits `c[t][a]` for `t = 0..=N` and every attribute `a` (round-major); +//! dependency triggers `g[t][d]` for `t < N` (round-major); gain bits `w_a`. + +use crate::models::formula::{CNFClause, Satisfiability}; +use crate::models::misc::BoyceCoddNormalFormViolation; +use crate::reduction; +use crate::registry::ConstructionError; +use crate::rules::ReductionError; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +/// Result of reducing a Boyce-Codd normal form violation instance to SAT. +#[derive(Debug, Clone)] +pub struct ReductionBCNFViolationToSAT { + target: Satisfiability, + num_selection_bits: usize, +} + +impl ReductionResult for ReductionBCNFViolationToSAT { + type Source = BoyceCoddNormalFormViolation; + type Target = Satisfiability; + + fn target_problem(&self) -> &Satisfiability { + &self.target + } + + fn extract_solution( + &self, + target_solution: &Vec, + ) -> crate::rules::ExtractionResult> { + crate::rules::traits::validate_target_witness( + &self.target, + target_solution, + |value| value.0, + "target assignment does not satisfy the closure encoding", + )?; + Ok(target_solution[..self.num_selection_bits].to_vec()) + } +} + +#[crate::aggregate_reduction(identity)] +impl crate::rules::AggregateReductionResult for ReductionBCNFViolationToSAT {} + +/// Number of SAT variables `N(N+1) + N·D + 2r`, checked against the signed +/// literal range (`i64::MAX`). +fn variable_count(n: usize, d: usize, r: usize) -> Result { + let total = n + .checked_add(1) + .and_then(|n1| n.checked_mul(n1)) + .and_then(|layers| layers.checked_add(n.checked_mul(d)?)) + .and_then(|sum| sum.checked_add(r.checked_mul(2)?)) + .ok_or_else(|| { + ConstructionError::from( + "BoyceCoddNormalFormViolation -> Satisfiability variable count overflows", + ) + })?; + if u64::try_from(total).map_or(true, |t| t > i64::MAX as u64) { + return Err(format!( + "BoyceCoddNormalFormViolation -> Satisfiability needs {total} variables; SAT variable numbers are limited to {}", + i64::MAX + ) + .into()); + } + Ok(total) +} + +/// Number of clauses `N + 4r + N(L + B + D + 2N) + 2`, checked. +fn clause_count(n: usize, d: usize, r: usize, l: usize, b: usize) -> Option { + let per_round = l + .checked_add(b)? + .checked_add(d)? + .checked_add(n.checked_mul(2)?)?; + n.checked_add(r.checked_mul(4)?)? + .checked_add(n.checked_mul(per_round)?)? + .checked_add(2) +} + +#[reduction(transform = { + exact { + num_vars = "num_attributes * (num_attributes + 1) + num_attributes * num_functional_deps + 2 * num_target_attributes", + }, + upper_bound { + num_clauses = "num_attributes + 4 * num_target_attributes + num_attributes * (2 * num_attributes * num_functional_deps + num_functional_deps + 2 * num_attributes) + 2", + num_literals = "num_attributes + 12 * num_target_attributes + num_attributes * (6 * num_attributes * num_functional_deps + num_functional_deps + 4 * num_attributes)", + }, +})] +impl ReduceTo for BoyceCoddNormalFormViolation { + type Result = ReductionBCNFViolationToSAT; + + fn reduce_to(&self) -> Result { + let construction = >::target_construction; + let n = self.num_attributes(); + let fds = self.functional_deps(); + let d = fds.len(); + let target_set = self.target_subset(); + let r = target_set.len(); + let num_vars = variable_count(n, d, r).map_err(construction)?; + let lhs_total = fds.iter().map(|(l, _)| l.len()).sum::(); + let rhs_total = fds.iter().map(|(_, rr)| rr.len()).sum::(); + let num_clauses = clause_count(n, d, r, lhs_total, rhs_total).ok_or_else(|| { + construction( + "BoyceCoddNormalFormViolation -> Satisfiability clause count overflows".into(), + ) + })?; + let mut clauses: Vec = Vec::new(); + clauses + .try_reserve_exact(num_clauses) + .map_err(|_| construction(format!("cannot allocate {num_clauses} clauses").into()))?; + + // All numbers below are at most `num_vars <= i64::MAX`. + let lit = |v: usize| -> i64 { i64::try_from(v).expect("variable number fits i64") }; + let mut position = vec![None; n]; + for (i, &a) in target_set.iter().enumerate() { + position[a] = Some(i); + } + let x = |pos: usize| lit(1 + pos); + let c = |t: usize, a: usize| lit(1 + r + t * n + a); + let g_base = r + (n + 1) * n; + let g = |t: usize, dep: usize| lit(1 + g_base + t * d + dep); + let w_base = g_base + n * d; + let w = |pos: usize| lit(1 + w_base + pos); + + // Dependencies concluding each attribute. + let mut concluding: Vec> = vec![Vec::new(); n]; + for (dep, (_, rhs)) in fds.iter().enumerate() { + for &a in rhs { + concluding[a].push(dep); + } + } + + for (a, slot) in position.iter().enumerate() { + match *slot { + Some(pos) => { + clauses.push(CNFClause::new(vec![-c(0, a), x(pos)])); + clauses.push(CNFClause::new(vec![c(0, a), -x(pos)])); + } + None => clauses.push(CNFClause::new(vec![-c(0, a)])), + } + } + for t in 0..n { + for (dep, (lhs, _)) in fds.iter().enumerate() { + let trigger = g(t, dep); + for &a in lhs { + clauses.push(CNFClause::new(vec![-trigger, c(t, a)])); + } + let mut all = vec![trigger]; + all.extend(lhs.iter().map(|&a| -c(t, a))); + clauses.push(CNFClause::new(all)); + } + for (a, deps) in concluding.iter().enumerate() { + let mut inputs = vec![c(t, a)]; + inputs.extend(deps.iter().map(|&dep| g(t, dep))); + for &h in &inputs { + clauses.push(CNFClause::new(vec![-h, c(t + 1, a)])); + } + let mut rev = vec![-c(t + 1, a)]; + rev.extend(inputs); + clauses.push(CNFClause::new(rev)); + } + } + for (pos, &a) in target_set.iter().enumerate() { + clauses.push(CNFClause::new(vec![-w(pos), -x(pos)])); + clauses.push(CNFClause::new(vec![-w(pos), c(n, a)])); + clauses.push(CNFClause::new(vec![w(pos), x(pos), -c(n, a)])); + } + clauses.push(CNFClause::new((0..r).map(w).collect())); + clauses.push(CNFClause::new( + target_set.iter().map(|&a| -c(n, a)).collect(), + )); + + let target = Satisfiability::try_new(num_vars, clauses).map_err(construction)?; + Ok(ReductionBCNFViolationToSAT { + target, + num_selection_bits: r, + }) + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "boycecoddnormalformviolation_to_satisfiability", + build: || { + let source = BoyceCoddNormalFormViolation::new( + 4, + vec![(vec![0], vec![1]), (vec![1], vec![2])], + vec![0, 1, 3], + ); + // X = {0}; layers 1000 1100 1110 1110 1110; triggers 10 11 11 11; gains 010. + let bits = "100\ + 1000110011101110\ + 1110\ + 10111111\ + 010"; + let target_config: Vec = bits.chars().map(|ch| ch == '1').collect(); + crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>( + source, + SolutionPair { + source_config: serde_json::json!(vec![true, false, false]), + target_config: serde_json::json!(target_config), + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/boycecoddnormalformviolation_satisfiability.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 7606f4923..ef684a910 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -1,5 +1,6 @@ //! Reduction rules between NP-hard problems. +pub(crate) mod boycecoddnormalformviolation_satisfiability; pub(crate) mod decisionilp_sat; pub mod analysis; @@ -460,6 +461,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec ReductionBCNFViolationToSAT { + ReduceTo::::reduce_to(source).expect("reduction should succeed") +} + +fn bcnf(n: usize, fds: &[(&[usize], &[usize])], r: &[usize]) -> BoyceCoddNormalFormViolation { + BoyceCoddNormalFormViolation::new( + n, + fds.iter() + .map(|(l, rr)| (l.to_vec(), rr.to_vec())) + .collect(), + r.to_vec(), + ) +} + +fn closure(source: &BoyceCoddNormalFormViolation, selected: &BTreeSet) -> BTreeSet { + let mut closed = selected.clone(); + loop { + let before = closed.len(); + for (lhs, rhs) in source.functional_deps() { + if lhs.iter().all(|a| closed.contains(a)) { + closed.extend(rhs.iter().copied()); + } + } + if closed.len() == before { + return closed; + } + } +} + +/// Forced assignment of the target for a selection: the layers of the closure +/// iteration, the triggers and the gain bits, in the documented variable order. +fn forced_assignment(source: &BoyceCoddNormalFormViolation, bits: &[bool]) -> Vec { + let n = source.num_attributes(); + let target_set = source.target_subset(); + let mut layer: BTreeSet = target_set + .iter() + .zip(bits) + .filter(|&(_, &b)| b) + .map(|(&a, _)| a) + .collect(); + let selected = layer.clone(); + let mut out = bits.to_vec(); + let mut triggers = Vec::new(); + for _ in 0..n { + out.extend((0..n).map(|a| layer.contains(&a))); + let mut next = layer.clone(); + for (lhs, rhs) in source.functional_deps() { + let on = lhs.iter().all(|a| layer.contains(a)); + triggers.push(on); + if on { + next.extend(rhs.iter().copied()); + } + } + layer = next; + } + out.extend((0..n).map(|a| layer.contains(&a))); + out.extend(triggers); + out.extend( + target_set + .iter() + .map(|a| !selected.contains(a) && layer.contains(a)), + ); + out +} + +fn selections(r: usize) -> impl Iterator> { + (0..1usize << r).map(move |mask| (0..r).map(|i| (mask >> i) & 1 == 1).collect()) +} + +/// For every selection: the forced assignment satisfies the target exactly when +/// the selection is a source solution, its final layer is the closure, and +/// extraction agrees. +fn assert_selection_equivalence(source: &BoyceCoddNormalFormViolation) { + let reduction = reduce(source); + let target = reduction.target_problem(); + let n = source.num_attributes(); + let r = source.num_target_attributes(); + for bits in selections(r) { + let assignment = forced_assignment(source, &bits); + assert_eq!(assignment.len(), target.num_vars()); + let source_ok = source.evaluate(&bits).unwrap().0; + assert_eq!( + target.evaluate(&assignment).unwrap().0, + source_ok, + "disagreement on {bits:?}" + ); + let selected: BTreeSet = source + .target_subset() + .iter() + .zip(&bits) + .filter(|&(_, &b)| b) + .map(|(&a, _)| a) + .collect(); + let layers_end = r + (n + 1) * n; + let last: BTreeSet = (0..n).filter(|&a| assignment[layers_end - n + a]).collect(); + assert_eq!(last, closure(source, &selected)); + match reduction.extract_solution(&assignment) { + Ok(extracted) => { + assert!(source_ok); + assert_eq!(extracted, bits); + } + Err(_) => assert!(!source_ok), + } + } +} + +/// Solve the target with an exact solver (not a re-simulation of the construction). +fn solve_target(target: &Satisfiability) -> Option> { + match ILPSolver::new().solve(target) { + Err(ILPSolveError::Infeasible) => None, + result => Some(result.expect("target solve")), + } +} + +/// With the selection pinned, the only model is the forced assignment: pin the +/// selection bits, forbid the forced assignment, and require infeasibility. +fn assert_auxiliaries_unique(source: &BoyceCoddNormalFormViolation, bits: &[bool]) { + let reduction = reduce(source); + let target = reduction.target_problem(); + let forced = forced_assignment(source, bits); + let mut clauses = target.clauses().to_vec(); + clauses.extend((0..bits.len()).map(|i| { + let v = i64::try_from(i + 1).unwrap(); + CNFClause::new(vec![if bits[i] { v } else { -v }]) + })); + clauses.push(CNFClause::new( + forced + .iter() + .enumerate() + .map(|(i, &b)| { + let v = i64::try_from(i + 1).unwrap(); + if b { -v } else { v } + }) + .collect(), + )); + let pinned = Satisfiability::new(target.num_vars(), clauses); + assert!( + solve_target(&pinned).is_none(), + "auxiliaries not determined for {bits:?}" + ); +} + +fn yes_source() -> BoyceCoddNormalFormViolation { + bcnf(4, &[(&[0], &[1]), (&[1], &[2])], &[0, 1, 3]) +} + +fn no_source() -> BoyceCoddNormalFormViolation { + bcnf(3, &[(&[0], &[1]), (&[1], &[2]), (&[2], &[0])], &[0, 1, 2]) +} + +fn yes_target_bits() -> Vec { + // selection | layers 1000 1100 1110 1110 1110 | triggers 10 11 11 11 | gains + ["100", "10001100111011101110", "10111111", "010"] + .concat() + .chars() + .map(|ch| ch == '1') + .collect() +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_closed_loop() { + // N = 3, one dependency, R = A: 21 target variables, enumerable by brute force. + let source = bcnf(3, &[(&[0], &[1])], &[0, 1, 2]); + let reduction = reduce(&source); + assert_eq!(reduction.target_problem().num_vars(), 21); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "BCNF violation -> SAT closed loop", + ); + // One target model per source solution. + let models = BruteForce::new() + .find_all_witnesses(reduction.target_problem()) + .unwrap(); + let solutions = BruteForce::new().find_all_witnesses(&source).unwrap(); + assert_eq!(models.len(), solutions.len()); + assert!(!solutions.is_empty()); +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_yes_example() { + let source = yes_source(); + let reduction = reduce(&source); + let target = reduction.target_problem(); + assert_eq!( + ( + target.num_vars(), + target.num_clauses(), + target.num_literals() + ), + (34, 74, 160) + ); + let bits = yes_target_bits(); + assert_eq!(bits.len(), 34); + assert!(target.evaluate(&bits).unwrap().0); + assert_eq!(forced_assignment(&source, &[true, false, false]), bits); + assert_eq!( + reduction.extract_solution(&bits).unwrap(), + vec![true, false, false] + ); + assert_selection_equivalence(&source); + for bits in selections(3) { + assert_auxiliaries_unique(&source, &bits); + } + let model = solve_target(target).expect("YES target is satisfiable"); + let extracted = reduction.extract_solution(&model).unwrap(); + assert!(source.evaluate(&extracted).unwrap().0); + let solutions: Vec> = selections(3) + .filter(|b| source.evaluate(b).unwrap().0) + .collect(); + assert!(solutions.contains(&vec![true, false, false])); +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_no_example_infeasible() { + let source = no_source(); + let reduction = reduce(&source); + let target = reduction.target_problem(); + assert_eq!( + ( + target.num_vars(), + target.num_clauses(), + target.num_literals() + ), + (27, 62, 138) + ); + assert!(BruteForce::new().solve(&source).unwrap().is_none()); + // The exact solver finds no model of the 27-variable target. + assert!(solve_target(target).is_none()); + assert_selection_equivalence(&source); + // Each selection determines all auxiliaries, and its forced assignment violates a final clause. + for bits in selections(3) { + assert_auxiliaries_unique(&source, &bits); + assert!( + !target + .evaluate(&forced_assignment(&source, &bits)) + .unwrap() + .0 + ); + } +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_variable_layout_and_clauses() { + let source = yes_source(); + let target = reduce(&source).target_problem().clone(); + let clauses: Vec> = target + .clauses() + .iter() + .map(|c| c.literals.clone()) + .collect(); + // selection bits 1..=3; c[0][0] = 4, c[0][3] = 7; c[1][0] = 8; triggers start at 24; gains at 32 + assert_eq!(&clauses[0], &vec![-4, 1]); + assert_eq!(&clauses[1], &vec![4, -1]); + assert_eq!(&clauses[2], &vec![-5, 2]); + assert_eq!(&clauses[4], &vec![-6]); + // trigger g[0][0] = 24 for FD {0} -> {1} + assert!(clauses.contains(&vec![-24, 4])); + assert!(clauses.contains(&vec![24, -4])); + // c[1][1] (= 9) is fed by its predecessor c[0][1] (= 5) and by g[0][0] (= 24) + assert!(clauses.contains(&vec![-5, 9])); + assert!(clauses.contains(&vec![-24, 9])); + assert!(clauses.contains(&vec![-9, 5, 24])); + // gain gate for the first target attribute and the final clauses + assert!(clauses.contains(&vec![-32, -1])); + assert!(clauses.contains(&vec![-32, 20])); + assert!(clauses.contains(&vec![32, 1, -20])); + assert_eq!(clauses[clauses.len() - 2], vec![32, 33, 34]); + assert_eq!(clauses[clauses.len() - 1], vec![-20, -21, -23]); +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_parameter_formulas() { + let sources = vec![ + yes_source(), + no_source(), + bcnf(3, &[], &[0, 1, 2]), + bcnf(1, &[(&[0], &[0])], &[0]), + bcnf( + 4, + &[(&[0, 1], &[1, 2]), (&[0, 1], &[1, 2]), (&[2], &[])], + &[0, 1, 2, 3], + ), + bcnf(5, &[(&[0], &[1, 2, 3, 4]), (&[1, 2, 3, 4], &[0])], &[1, 4]), + ]; + for source in sources { + let reduction = reduce(&source); + assert_parameter_predictions(&source, &reduction); + let (n, d, r) = ( + source.num_attributes(), + source.num_functional_deps(), + source.num_target_attributes(), + ); + let l: usize = source.functional_deps().iter().map(|(a, _)| a.len()).sum(); + let b: usize = source.functional_deps().iter().map(|(_, a)| a.len()).sum(); + let target = reduction.target_problem(); + assert_eq!(target.num_vars(), n * (n + 1) + n * d + 2 * r); + assert_eq!( + target.num_clauses(), + n + 4 * r + n * (l + b + d + 2 * n) + 2 + ); + assert_eq!( + target.num_literals(), + n + 12 * r + n * (3 * l + 3 * b + d + 4 * n) + ); + } +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_special_cases() { + // empty dependency list: no gain is ever possible + let empty = bcnf(3, &[], &[0, 1, 2]); + assert_selection_equivalence(&empty); + assert!(selections(3).all(|b| !empty.evaluate(&b).unwrap().0)); + // empty right sides only conclude nothing + let empty_rhs = bcnf(3, &[(&[0], &[]), (&[1], &[])], &[0, 1, 2]); + assert_selection_equivalence(&empty_rhs); + assert!(selections(3).all(|b| !empty_rhs.evaluate(&b).unwrap().0)); + // derivation 0 -> 2 -> 1 passes through attribute 2 outside R = {0, 1, 3} + let through = bcnf(4, &[(&[0], &[2]), (&[2], &[1])], &[0, 1, 3]); + assert_selection_equivalence(&through); + let reduction = reduce(&through); + let witness = forced_assignment(&through, &[true, false, false]); + assert!(reduction.target_problem().evaluate(&witness).unwrap().0); + assert_eq!( + reduction.extract_solution(&witness).unwrap(), + vec![true, false, false] + ); + // X = empty is never a solution: every left side is nonempty + let reduction = reduce(&yes_source()); + let zero = forced_assignment(&yes_source(), &[false; 3]); + assert!(!reduction.target_problem().evaluate(&zero).unwrap().0); + assert!(reduction.extract_solution(&zero).is_err()); + // single target attribute, duplicates, left side contained in right side + assert_selection_equivalence(&bcnf(3, &[(&[0], &[1])], &[0])); + assert_selection_equivalence(&bcnf(3, &[(&[0], &[1]), (&[0, 0], &[1, 1])], &[0, 1, 2])); + assert_selection_equivalence(&bcnf(4, &[(&[0, 1], &[1, 2])], &[0, 1, 2, 3])); + assert_selection_equivalence(&bcnf(1, &[(&[0], &[0])], &[0])); +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_exhaustive_small_instances() { + // Every instance with N <= 3 and at most two dependencies, over every target set. + for n in 1..=3usize { + let sides: Vec> = (0..1usize << n) + .map(|m| (0..n).filter(|a| (m >> a) & 1 == 1).collect()) + .collect(); + let mut deps: Vec<(Vec, Vec)> = Vec::new(); + for lhs in sides.iter().filter(|s| !s.is_empty()) { + for rhs in &sides { + deps.push((lhs.clone(), rhs.clone())); + } + } + let mut lists: Vec, Vec)>> = vec![vec![]]; + lists.extend(deps.iter().map(|f| vec![f.clone()])); + if n <= 2 { + for f in &deps { + for g in &deps { + lists.push(vec![f.clone(), g.clone()]); + } + } + } + for list in lists { + for target_set in sides.iter().filter(|s| !s.is_empty()) { + let source = BoyceCoddNormalFormViolation::new(n, list.clone(), target_set.clone()); + assert_selection_equivalence(&source); + } + } + } +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_long_chain_needs_all_rounds() { + // 0 -> 1 -> 2 -> 3 -> 4: gaining attribute 4 from {0} takes four rounds. + let source = bcnf( + 5, + &[(&[0], &[1]), (&[1], &[2]), (&[2], &[3]), (&[3], &[4])], + &[0, 4, 3], + ); + assert_selection_equivalence(&source); + assert!(!source.evaluate(&vec![true, false, false]).unwrap().0); +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_extraction_rejects_invalid_witnesses() { + let source = yes_source(); + let reduction = reduce(&source); + let good = yes_target_bits(); + assert_eq!( + reduction.extract_solution(&good).unwrap(), + vec![true, false, false] + ); + // wrong lengths + assert!(reduction.extract_solution(&good[..33].to_vec()).is_err()); + let mut long = good.clone(); + long.push(false); + assert!(reduction.extract_solution(&long).is_err()); + assert!(reduction.extract_solution(&vec![]).is_err()); + // every single-bit flip violates the encoding (all bits are functionally determined) + for i in 0..good.len() { + let mut bad = good.clone(); + bad[i] = !bad[i]; + assert!( + reduction.extract_solution(&bad).is_err(), + "flip of bit {i} accepted" + ); + } + // a consistent assignment of a non-solution selection + let non_solution = forced_assignment(&source, &[true, true, false]); + assert!(!source.evaluate(&vec![true, true, false]).unwrap().0); + assert!(reduction.extract_solution(&non_solution).is_err()); + // all-false is rejected + assert!(reduction.extract_solution(&vec![false; 34]).is_err()); +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_aggregate_value_matches_both_solvers() { + use crate::rules::AggregateReductionResult; + use crate::types::Or; + for source in [yes_source(), no_source()] { + let reduction = reduce(&source); + let target = ReductionResult::target_problem(&reduction); + let source_value = Or(BruteForce::new().solve(&source).unwrap().is_some()); + let target_value = Or(solve_target(target).is_some()); + assert_eq!(target_value, source_value); + assert_eq!(reduction.extract_value(target_value), source_value); + } +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_size_boundaries() { + // variable numbers must fit i64: N(N+1) + N*D + 2r <= i64::MAX + let limit = i64::MAX as u128; + let fits = |n: u128, r: u128| n * (n + 1) + 2 * r <= limit; + let mut n = 3_037_000_499u128; + while !fits(n, 1) { + n -= 1; + } + while fits(n + 1, 1) { + n += 1; + } + let n = usize::try_from(n).unwrap(); + assert_eq!( + variable_count(n, 0, 1).unwrap() as u128, + (n as u128) * (n as u128 + 1) + 2 + ); + assert!(variable_count(n + 1, 0, 1).is_err()); + // usize overflow in the products is reported, not wrapped + assert!(variable_count(usize::MAX, 0, 1).is_err()); + assert!(variable_count(2, usize::MAX, 1).is_err()); + assert!(variable_count(1, 0, usize::MAX).is_err()); + // the dependency term is part of the bound + assert!(variable_count(3_037_000_000, 5_000_000, 1).is_err()); + assert_eq!(variable_count(3, 2, 3).unwrap(), 12 + 6 + 6); + // clause counts are checked as well + assert_eq!(clause_count(4, 2, 3, 2, 2), Some(74)); + assert_eq!(clause_count(usize::MAX, 0, 1, 0, 0), None); + assert_eq!(clause_count(2, 1, usize::MAX / 4 + 1, 1, 1), None); + assert_eq!(clause_count(1, 0, 1, usize::MAX, 1), None); + assert_eq!(clause_count(1, usize::MAX, 1, 0, 0), None); + // largest representable clause count and its successor + let r = (usize::MAX - 2) / 4; + assert_eq!(clause_count(0, 0, r, 0, 0), Some(4 * r + 2)); + assert_eq!(clause_count(0, 0, r + 1, 0, 0), None); + // N = 2: 2l + 12 clauses for l left-side attributes + let l = (usize::MAX - 12) / 2; + assert_eq!(clause_count(2, 0, 0, l, 0), Some(2 * l + 12)); + assert_eq!(clause_count(2, 0, 0, l + 1, 0), None); +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_huge_universe_is_an_error() { + // An implicit universe of 2^32 attributes needs more than 2^63 variables. + let source = + BoyceCoddNormalFormViolation::new(1usize << 32, vec![(vec![0], vec![1])], vec![0, 1]); + let error = ReduceTo::::reduce_to(&source).unwrap_err(); + assert!( + matches!(error, ReductionError::Construction { .. }), + "{error}" + ); +} + +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_unallocatable_universe_is_an_error() { + // Variable numbers still fit i64 but the clause list cannot be allocated. + let source = BoyceCoddNormalFormViolation::new(3_000_000_000, vec![], vec![0, 1]); + let error = ReduceTo::::reduce_to(&source).unwrap_err(); + assert!( + matches!(error, ReductionError::Construction { .. }), + "{error}" + ); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_boycecoddnormalformviolation_to_satisfiability_canonical_example() { + let specs = canonical_rule_example_specs(); + assert_eq!(specs.len(), 1); + let example = (specs[0].build)(); + assert_eq!(example.source.problem, "BoyceCoddNormalFormViolation"); + assert_eq!(example.target.problem, "Satisfiability"); + let target: Satisfiability = serde_json::from_value(example.target.instance.clone()).unwrap(); + assert_eq!( + ( + target.num_vars(), + target.num_clauses(), + target.num_literals() + ), + (34, 74, 160) + ); + assert_eq!(example.solutions.len(), 1); + let pair = &example.solutions[0]; + let target_config: Vec = serde_json::from_value(pair.target_config.clone()).unwrap(); + let source_config: Vec = serde_json::from_value(pair.source_config.clone()).unwrap(); + assert!(target.evaluate(&target_config).unwrap().0); + assert_eq!(target_config, yes_target_bits()); + let reduction = reduce(&yes_source()); + assert_eq!( + reduction.extract_solution(&target_config).unwrap(), + source_config + ); + assert!(yes_source().evaluate(&source_config).unwrap().0); +}