Fix #447: [Model] BoyceCoddNormalFormViolation (#685)

* Add plan for #447: [Model] BoyceCoddNormalFormViolation

* Implement #447: [Model] BoyceCoddNormalFormViolation

Add the Boyce-Codd Normal Form Violation satisfaction problem model
(Garey & Johnson A4 SR29). Given attributes, functional dependencies,
and a target subset, determines whether a BCNF violation exists.

- Model: src/models/misc/boyce_codd_normal_form_violation.rs
- Tests: 20 unit tests covering evaluation, solver, serialization, edge cases
- CLI: create support with --n, --sets (lhs:rhs format), --target
- Paper: problem-def entry in docs/paper/reductions.typ
- Example-db: canonical example with violation witness X={2}

* chore: remove plan file after implementation

* fix: address PR #685 review comments

* fix: update BCNF canonical example spec to new ModelExampleSpec API

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Xiwei Pan <xiwei.pan@connect.hkust-gz.edu.cn>
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Xiwei Pan <90967972+isPANN@users.noreply.github.com>

Author: 3 people

docs/paper/reductions.typ

@@ -103,6 +103,7 @@
   "BalancedCompleteBipartiteSubgraph": [Balanced Complete Bipartite Subgraph],
   "BoundedComponentSpanningForest": [Bounded Component Spanning Forest],
   "BinPacking": [Bin Packing],
+  "BoyceCoddNormalFormViolation": [Boyce-Codd Normal Form Violation],
   "ClosestVectorProblem": [Closest Vector Problem],
   "ConsecutiveSets": [Consecutive Sets],
   "MinimumMultiwayCut": [Minimum Multiway Cut],
@@ -2884,6 +2885,14 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76],
   *Example.* Let $n = 6$ tasks, $m = 3$ processors, $r = 1$ resource with $B_1 = 20$, and deadline $D = 2$. Resource requirements: $R_1(t_1) = 6$, $R_1(t_2) = 7$, $R_1(t_3) = 7$, $R_1(t_4) = 6$, $R_1(t_5) = 8$, $R_1(t_6) = 6$. Schedule: slot 0 $arrow.l {t_1, t_2, t_3}$ (3 tasks, resource $= 20$), slot 1 $arrow.l {t_4, t_5, t_6}$ (3 tasks, resource $= 20$). Both constraints satisfied; answer: YES.
 ]
 
+#problem-def("BoyceCoddNormalFormViolation")[
+  *Instance:* A set $A$ of attribute names, a collection $F$ of functional dependencies on $A$, and a subset $A' subset.eq A$.
+
+  *Question:* Is there a subset $X subset.eq A'$ and two attributes $y, z in A' backslash X$ such that $y in X^+$ but $z in.not X^+$, where $X^+$ is the closure of $X$ under $F$?
+][
+  A relation satisfies _Boyce-Codd Normal Form_ (BCNF) if every non-trivial functional dependency $X arrow.r Y$ has $X$ as a superkey --- that is, $X^+$ = $A'$. This classical NP-complete problem from database theory asks whether the given attribute subset $A'$ violates BCNF. The NP-completeness was established by Beeri and Bernstein (1979) via reduction from Hitting Set. It appears as problem SR29 in Garey and Johnson's compendium (category A4: Storage and Retrieval).
+]
+
 #problem-def("SumOfSquaresPartition")[
   Given a finite set $A = {a_0, dots, a_(n-1)}$ with sizes $s(a_i) in ZZ^+$, a positive integer $K lt.eq |A|$ (number of groups), and a positive integer $J$ (bound), determine whether $A$ can be partitioned into $K$ disjoint sets $A_1, dots, A_K$ such that $sum_(i=1)^K (sum_(a in A_i) s(a))^2 lt.eq J$.
 ][

problemreductions-cli/src/commands/create.rs

@@ -14,9 +14,10 @@ use problemreductions::models::graph::{
     MultipleChoiceBranching, SteinerTree, StrongConnectivityAugmentation,
 };
 use problemreductions::models::misc::{
-    BinPacking, CbqRelation, ConjunctiveBooleanQuery, FlowShopScheduling, LongestCommonSubsequence,
-    MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, PartiallyOrderedKnapsack,
-    QueryArg, RectilinearPictureCompression, ResourceConstrainedScheduling,
+    BinPacking, BoyceCoddNormalFormViolation, CbqRelation, ConjunctiveBooleanQuery,
+    FlowShopScheduling, LongestCommonSubsequence, MinimumTardinessSequencing,
+    MultiprocessorScheduling, PaintShop, PartiallyOrderedKnapsack, QueryArg,
+    RectilinearPictureCompression, ResourceConstrainedScheduling,
     SequencingToMinimizeMaximumCumulativeCost, SequencingWithReleaseTimesAndDeadlines,
     SequencingWithinIntervals, ShortestCommonSupersequence, StringToStringCorrection, SubsetSum,
     SumOfSquaresPartition,
@@ -154,6 +155,20 @@ fn format_problem_ref(problem: &ProblemRef) -> String {
     format!("{}/{}", problem.name, values)
 }
 
+fn ensure_attribute_indices_in_range(
+    indices: &[usize],
+    num_attributes: usize,
+    context: &str,
+) -> Result<()> {
+    for &attr in indices {
+        anyhow::ensure!(
+            attr < num_attributes,
+            "{context} contains attribute index {attr}, which is out of range for --n {num_attributes}"
+        );
+    }
+    Ok(())
+}
+
 fn resolve_example_problem_ref(
     input: &str,
     rgraph: &problemreductions::rules::ReductionGraph,
@@ -402,6 +417,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str {
             "--matrix \"1,1,0,0;1,1,0,0;0,0,1,1;0,0,1,1\" --k 2"
         }
         "SubsetSum" => "--sizes 3,7,1,8,2,4 --target 11",
+        "BoyceCoddNormalFormViolation" => {
+            "--n 6 --sets \"0,1:2;2:3;3,4:5\" --target 0,1,2,3,4,5"
+        }
         "SumOfSquaresPartition" => "--sizes 5,3,8,2,7,1 --num-groups 3 --bound 240",
         "ComparativeContainment" => {
             "--universe 4 --r-sets \"0,1,2,3;0,1\" --s-sets \"0,1,2,3;2,3\" --r-weights 2,5 --s-weights 3,6"
@@ -1301,6 +1319,58 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> {
             create_vertex_weight_problem(args, canonical, graph_type, &resolved_variant)?
         }
 
+        // BoyceCoddNormalFormViolation
+        "BoyceCoddNormalFormViolation" => {
+            let n = args.n.ok_or_else(|| {
+                anyhow::anyhow!(
+                    "BoyceCoddNormalFormViolation requires --n, --sets, and --target\n\n\
+                     Usage: pred create BoyceCoddNormalFormViolation --n 6 --sets \"0,1:2;2:3;3,4:5\" --target 0,1,2,3,4,5"
+                )
+            })?;
+            let sets_str = args.sets.as_deref().ok_or_else(|| {
+                anyhow::anyhow!(
+                    "BoyceCoddNormalFormViolation requires --sets (functional deps as lhs:rhs;...)\n\n\
+                     Usage: pred create BoyceCoddNormalFormViolation --n 6 --sets \"0,1:2;2:3;3,4:5\" --target 0,1,2,3,4,5"
+                )
+            })?;
+            let target_str = args.target.as_deref().ok_or_else(|| {
+                anyhow::anyhow!(
+                    "BoyceCoddNormalFormViolation requires --target (comma-separated attribute indices)\n\n\
+                     Usage: pred create BoyceCoddNormalFormViolation --n 6 --sets \"0,1:2;2:3;3,4:5\" --target 0,1,2,3,4,5"
+                )
+            })?;
+            let fds: Vec<(Vec<usize>, Vec<usize>)> = sets_str
+                .split(';')
+                .map(|fd_str| {
+                    let parts: Vec<&str> = fd_str.split(':').collect();
+                    anyhow::ensure!(
+                        parts.len() == 2,
+                        "Each FD must be lhs:rhs, got '{}'",
+                        fd_str
+                    );
+                    let lhs: Vec<usize> = util::parse_comma_list(parts[0])?;
+                    let rhs: Vec<usize> = util::parse_comma_list(parts[1])?;
+                    ensure_attribute_indices_in_range(
+                        &lhs,
+                        n,
+                        &format!("Functional dependency '{fd_str}' lhs"),
+                    )?;
+                    ensure_attribute_indices_in_range(
+                        &rhs,
+                        n,
+                        &format!("Functional dependency '{fd_str}' rhs"),
+                    )?;
+                    Ok((lhs, rhs))
+                })
+                .collect::<Result<_>>()?;
+            let target: Vec<usize> = util::parse_comma_list(target_str)?;
+            ensure_attribute_indices_in_range(&target, n, "Target subset")?;
+            (
+                ser(BoyceCoddNormalFormViolation::new(n, fds, target))?,
+                resolved_variant.clone(),
+            )
+        }
+
         // BinPacking
         "BinPacking" => {
             let sizes_str = args.sizes.as_deref().ok_or_else(|| {
@@ -4007,6 +4077,7 @@ mod tests {
     use super::help_flag_name;
     use super::parse_bool_rows;
     use super::*;
+    use super::{ensure_attribute_indices_in_range, problem_help_flag_name};
     use crate::cli::{Cli, Commands};
     use crate::output::OutputConfig;
 
@@ -4039,6 +4110,16 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_ensure_attribute_indices_in_range_rejects_out_of_range_index() {
+        let err = ensure_attribute_indices_in_range(&[0, 4], 3, "Functional dependency '0:4' rhs")
+            .unwrap_err();
+        assert!(
+            err.to_string().contains("out of range"),
+            "unexpected error: {err}"
+        );
+    }
+
     #[test]
     fn test_problem_help_uses_prime_attribute_name_cli_overrides() {
         assert_eq!(

problemreductions-cli/tests/cli_tests.rs

@@ -4988,6 +4988,88 @@ fn test_create_factoring_missing_bits() {
     );
 }
 
+#[test]
+fn test_create_bcnf_rejects_out_of_range_attribute_indices() {
+    let output = pred()
+        .args([
+            "create",
+            "BoyceCoddNormalFormViolation",
+            "--n",
+            "3",
+            "--sets",
+            "0:4",
+            "--target",
+            "0,1,2",
+        ])
+        .output()
+        .unwrap();
+    assert!(
+        !output.status.success(),
+        "expected invalid indices to be rejected"
+    );
+    let stderr = String::from_utf8_lossy(&output.stderr);
+    assert!(
+        !stderr.contains("panicked at"),
+        "CLI should return a user-facing error, got: {stderr}"
+    );
+    assert!(
+        stderr.contains("out of range"),
+        "expected out-of-range error, got: {stderr}"
+    );
+}
+
+#[test]
+fn test_create_bcnf_rejects_out_of_range_lhs_attribute_indices() {
+    let output = pred()
+        .args([
+            "create",
+            "BoyceCoddNormalFormViolation",
+            "--n",
+            "3",
+            "--sets",
+            "4:0",
+            "--target",
+            "0,1,2",
+        ])
+        .output()
+        .unwrap();
+    assert!(
+        !output.status.success(),
+        "expected invalid lhs indices to be rejected"
+    );
+    let stderr = String::from_utf8_lossy(&output.stderr);
+    assert!(
+        stderr.contains("lhs contains attribute index 4"),
+        "expected lhs-specific out-of-range error, got: {stderr}"
+    );
+}
+
+#[test]
+fn test_create_bcnf_rejects_out_of_range_target_attribute_indices() {
+    let output = pred()
+        .args([
+            "create",
+            "BoyceCoddNormalFormViolation",
+            "--n",
+            "3",
+            "--sets",
+            "0:1",
+            "--target",
+            "0,1,4",
+        ])
+        .output()
+        .unwrap();
+    assert!(
+        !output.status.success(),
+        "expected invalid target indices to be rejected"
+    );
+    let stderr = String::from_utf8_lossy(&output.stderr);
+    assert!(
+        stderr.contains("Target subset contains attribute index 4"),
+        "expected target-specific out-of-range error, got: {stderr}"
+    );
+}
+
 #[test]
 fn test_create_sequencing_to_minimize_maximum_cumulative_cost() {
     let output = pred()

src/lib.rs

@@ -60,13 +60,13 @@ pub mod prelude {
         UndirectedTwoCommodityIntegralFlow,
     };
     pub use crate::models::misc::{
-        BinPacking, CbqRelation, ConjunctiveBooleanQuery, ConjunctiveQueryFoldability, Factoring,
-        FlowShopScheduling, Knapsack, LongestCommonSubsequence, MinimumTardinessSequencing,
-        MultiprocessorScheduling, PaintShop, Partition, QueryArg, RectilinearPictureCompression,
-        ResourceConstrainedScheduling, SequencingToMinimizeMaximumCumulativeCost,
-        SequencingWithReleaseTimesAndDeadlines, SequencingWithinIntervals,
-        ShortestCommonSupersequence, StaffScheduling, StringToStringCorrection, SubsetSum,
-        SumOfSquaresPartition, Term,
+        BinPacking, BoyceCoddNormalFormViolation, CbqRelation, ConjunctiveBooleanQuery,
+        ConjunctiveQueryFoldability, Factoring, FlowShopScheduling, Knapsack,
+        LongestCommonSubsequence, MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop,
+        Partition, QueryArg, RectilinearPictureCompression, ResourceConstrainedScheduling,
+        SequencingToMinimizeMaximumCumulativeCost, SequencingWithReleaseTimesAndDeadlines,
+        SequencingWithinIntervals, ShortestCommonSupersequence, StaffScheduling,
+        StringToStringCorrection, SubsetSum, SumOfSquaresPartition, Term,
     };
     pub use crate::models::set::{
         ComparativeContainment, ConsecutiveSets, ExactCoverBy3Sets, MaximumSetPacking,