[Critical] Remove KSatisfiability KN variant and short-clause constructors

problemreductions-cli/src/cli.rs

@@ -507,17 +507,17 @@ mod tests {
         let cli = Cli::try_parse_from([
             "pred",
             "create",
-            "3SAT",
+            "2SAT",
             "--num-vars",
             "3",
             "--clauses",
-            "1,2,3",
+            "1,2",
         ])
         .expect("variant alias parses");
         let Commands::Create(args) = cli.command else {
             panic!("expected create command");
         };
-        assert_eq!(args.problem.as_deref(), Some("KSatisfiability/K3"));
+        assert_eq!(args.problem.as_deref(), Some("KSatisfiability/K2"));
         assert_eq!(args.raw("num-vars"), Some("3"));
     }
 

src/models/formula/ksat.rs

@@ -7,7 +7,7 @@
 
 use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension};
 use crate::traits::Problem;
-use crate::variant::{KValue, K2, K3, KN};
+use crate::variant::{KValue, K2, K3};
 use serde::{de::Error as _, Deserialize, Deserializer, Serialize};
 
 use super::{sat::validate_cnf_literals, CNFClause};
@@ -53,7 +53,7 @@ inventory::submit! {
         name: "KSatisfiability",
         display_name: "K-Satisfiability",
         aliases: &["KSAT"],
-        dimensions: &[VariantDimension::new("k", "KN", &["KN", "K2", "K3"])],
+        dimensions: &[VariantDimension::new("k", "K3", &["K3", "K2"])],
         category: crate::registry::ProblemCategory::Formula,
         module_path: module_path!(),
         description: "SAT with exactly k literals per clause",
@@ -124,63 +124,24 @@ impl<K: KValue> KSatisfiability<K> {
     /// Create a new K-SAT problem.
     ///
     /// # Panics
-    /// Panics if any clause does not have exactly K literals (when K is a
-    /// concrete value like K2, K3). When K is KN (arbitrary), no clause-length
-    /// validation is performed.
+    /// Panics if any clause does not have exactly K literals.
     pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
         Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
     }
 
-    /// Create a K-SAT problem after validating its clauses.
+    /// Create a K-SAT problem after validating that every clause has exactly
+    /// K literals.
     pub fn try_new(
         num_vars: usize,
         clauses: Vec<CNFClause>,
     ) -> Result<Self, crate::registry::ConstructionError> {
         validate_cnf_literals(num_vars, &clauses)?;
-        if let Some(k) = K::K {
-            for (i, clause) in clauses.iter().enumerate() {
-                if clause.len() != k {
-                    return Err(
-                        format!("Clause {i} has {} literals, expected {k}", clause.len()).into(),
-                    );
-                }
-            }
-        }
-        Ok(Self {
-            num_vars,
-            clauses,
-            _phantom: std::marker::PhantomData,
-        })
-    }
-
-    /// Create a new K-SAT problem allowing clauses with fewer than K literals.
-    ///
-    /// This is useful when the reduction algorithm produces clauses with
-    /// fewer literals (e.g., when allow_less is true in the Julia implementation).
-    ///
-    /// # Panics
-    /// Panics if any clause has more than K literals (when K is a concrete
-    /// value like K2, K3). When K is KN (arbitrary), no clause-length
-    /// validation is performed.
-    pub fn new_allow_less(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
-        Self::try_new_allow_less(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
-    }
-
-    /// Create a K-SAT problem with shorter clauses after validation.
-    pub fn try_new_allow_less(
-        num_vars: usize,
-        clauses: Vec<CNFClause>,
-    ) -> Result<Self, crate::registry::ConstructionError> {
-        validate_cnf_literals(num_vars, &clauses)?;
-        if let Some(k) = K::K {
-            for (i, clause) in clauses.iter().enumerate() {
-                if clause.len() > k {
-                    return Err(format!(
-                        "Clause {i} has {} literals, expected at most {k}",
-                        clause.len()
-                    )
-                    .into());
-                }
+        let k = K::K.ok_or("KSatisfiability requires a fixed clause width K")?;
+        for (i, clause) in clauses.iter().enumerate() {
+            if clause.len() != k {
+                return Err(
+                    format!("Clause {i} has {} literals, expected {k}", clause.len()).into(),
+                );
             }
         }
         Ok(Self {
@@ -273,13 +234,11 @@ impl<K: KValue> crate::solvers::BruteForceProblem for KSatisfiability<K> {
 }
 
 crate::declare_variants! {
-    default KSatisfiability<KN> => "2^num_vars",
+    default KSatisfiability<K3> => "1.307^num_vars" aliases ["3SAT"],
     KSatisfiability<K2> => "num_vars + num_clauses" aliases ["2SAT"],
-    KSatisfiability<K3> => "1.307^num_vars" aliases ["3SAT"],
 }
 
 crate::register_brute_force! {
-    KSatisfiability<KN> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
     KSatisfiability<K2> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
     KSatisfiability<K3> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
 }

src/rules/ksatisfiability_bicliquecover.rs

@@ -5,8 +5,7 @@
 //!
 //! 1. **Normalize** the source 3-CNF formula:
 //!    - Compact the variables appearing in clauses, retaining the inverse map.
-//!      Repeat literals to pad nonempty short clauses to three positions.
-//!      Empty formulas and empty clauses map to fixed YES and NO targets.
+//!      The empty formula maps to a fixed YES target.
 //!    - For each appearing variable `x_i`, create two normalized variables
 //!      `t_i` and `f_i`. Replace literal `x_i` by `t_i`, replace literal
 //!      `¬x_i` by `f_i`. Add exactly-one clauses
@@ -205,9 +204,6 @@ fn normalize(
                 translated.push(f_lit(compact)?);
             }
         }
-        // Nonempty short clauses are equivalent after repeating a literal.
-        // Empty clauses are handled by the fixed NO construction before here.
-        translated.resize(3, translated[0]);
         clauses.push(translated);
     }
 
@@ -233,7 +229,7 @@ fn free_edge_budget(ell: usize, m: usize) -> Option<usize> {
 // With s source variables and m source clauses, the normalized counts
 // satisfy n <= 4(s+1), M <= m+4(s+1), ell <= s+1, ceil(log2 M) <= M.
 // Hence each partition is <= 31s+5m+39 and rank <= 14s+2m+22.
-// The declared coarser bounds also cover the fixed YES and NO targets.
+// The declared coarser bounds also cover the fixed YES target.
 #[crate::aggregate_reduction]
 impl crate::rules::AggregateReductionResult for ReductionKSatisfiabilityToBicliqueCover {
     type Source = KSatisfiability<K3>;
@@ -261,21 +257,10 @@ impl ReduceTo<BicliqueCover> for KSatisfiability<K3> {
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
         // ---------------- Stage 1: normalize ----------------
         let source_num_vars = self.num_vars();
-        let has_empty_clause = self
-            .clauses()
-            .iter()
-            .any(|clause| clause.literals.is_empty());
-        if has_empty_clause || self.clauses().is_empty() {
-            // The empty conjunction is YES; a conjunction with an empty
-            // disjunction is NO. Zero bicliques cover only the empty graph.
-            let size = usize::from(has_empty_clause);
-            let edges = if has_empty_clause {
-                vec![(0, 0)]
-            } else {
-                vec![]
-            };
+        if self.clauses().is_empty() {
+            // The empty conjunction is YES: zero bicliques cover the empty graph.
             return Ok(ReductionKSatisfiabilityToBicliqueCover {
-                target: BicliqueCover::new(BipartiteGraph::new(size, size, edges), 0),
+                target: BicliqueCover::new(BipartiteGraph::new(0, 0, vec![]), 0),
                 source_num_vars,
                 normalized_n: 0,
                 s1_left_offset: 0,

src/rules/ksatisfiability_cyclicordering.rs

@@ -9,10 +9,11 @@
 //! "true" one.
 //!
 //! Before applying the gadget, remove tautologies and repeated literals,
-//! compact occurring variables, and expand short clauses with fresh variables.
-//! Each resulting clause has three distinct variables in global index order.
-//! This is the hypothesis needed to combine the paper's local cyclic orders.
-//! Empty clauses and empty conjunctions map to fixed NO and YES targets.
+//! compact occurring variables, and expand clauses left with fewer than three
+//! distinct literals using fresh variables. Each resulting clause has three
+//! distinct variables in global index order. This is the hypothesis needed to
+//! combine the paper's local cyclic orders. The empty conjunction maps to a
+//! fixed YES target.
 //!
 //! Reference: Galil and Megiddo, "Cyclic ordering is NP-complete", 1977.
 
@@ -135,21 +136,17 @@ fn normalize(
                 }
             })
             .collect();
-        match *literals.as_slice() {
-            [a, b, c] => normalized.push([a, b, c]),
-            [a, b] => {
-                let u = variables.allocate()
-                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
-                normalized.extend([[a, b, u], [a, b, -u]]);
-            }
-            [a] => {
-                let u = variables.allocate()
-                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
-                let v = variables.allocate()
-                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
+        // Deduplication leaves one to three literals; fill the rest with fresh variables.
+        let fresh = variables
+            .allocate_many(3 - literals.len())
+            .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
+        match (literals.as_slice(), fresh.as_slice()) {
+            (&[a, b, c], []) => normalized.push([a, b, c]),
+            (&[a, b], &[u]) => normalized.extend([[a, b, u], [a, b, -u]]),
+            (&[a], &[u, v]) => {
                 normalized.extend([[a, u, v], [a, u, -v], [a, -u, v], [a, -u, -v]]);
             }
-            _ => unreachable!("empty clauses are handled before normalization; native clauses have at most three literals"),
+            _ => unreachable!("deduplicated three-literal clauses keep one to three literals"),
         }
     }
     // Original compact indices precede all fresh indices. Every emitted
@@ -174,18 +171,6 @@ impl ReduceTo<CyclicOrdering> for KSatisfiability<K3> {
     type Result = Reduction3SATToCyclicOrdering;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        if self
-            .clauses()
-            .iter()
-            .any(|clause| clause.literals.is_empty())
-        {
-            return Ok(Reduction3SATToCyclicOrdering {
-                target: CyclicOrdering::try_new(3, vec![(0, 1, 2), (0, 2, 1)])
-                    .map_err(<Self as ReduceTo<CyclicOrdering>>::target_construction)?,
-                source_num_vars: self.num_vars(),
-                source_variables: Vec::new(),
-            });
-        }
         let normalized = normalize(self)?;
         let num_vars = normalized.num_vars;
         let num_clauses = normalized.clauses.len();

src/rules/ksatisfiability_decisionminimumvertexcover.rs

@@ -68,10 +68,9 @@ impl ReductionResult for Reduction3SATToDecisionMVC {
 impl crate::rules::AggregateReductionResult for Reduction3SATToDecisionMVC {}
 
 #[reduction(
-    transform = {
-        exact { num_vertices = "2 * num_vars + 3 * num_clauses" },
-        // A clause with fewer than three literals links fewer triangle corners.
-        upper_bound { num_edges = "num_vars + 6 * num_clauses" },
+    transform = exact {
+        num_vertices = "2 * num_vars + 3 * num_clauses",
+        num_edges = "num_vars + 6 * num_clauses",
     }
 )]
 impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>> for KSatisfiability<K3> {
@@ -100,12 +99,7 @@ impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>> for KSatisfiabilit
             edges.push((base, base + 2));
 
             // Communication edges: connect triangle vertex k to the literal vertex
-            for k in 0..3 {
-                if clause.literals.is_empty() {
-                    continue;
-                }
-                // Repeating a literal pads a short clause without changing it.
-                let lit = clause.literals[k % clause.literals.len()];
+            for (k, &lit) in clause.literals.iter().enumerate() {
                 let var_idx = lit.unsigned_abs() as usize - 1; // 0-indexed variable
                 let literal_vertex = if lit > 0 {
                     2 * var_idx // positive literal vertex
@@ -123,18 +117,10 @@ impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>> for KSatisfiabilit
         Ok(Reduction3SATToDecisionMVC {
             target: Decision::new(
                 target,
-                if self
-                    .clauses()
-                    .iter()
-                    .any(|clause| clause.literals.is_empty())
-                {
-                    -1 // No nonnegative vertex-cover size can satisfy an empty clause.
-                } else {
-                    <Self as ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>>>::exact_i64(
-                        n + 2 * m,
-                        "computing the cover bound",
-                    )?
-                },
+                <Self as ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>>>::exact_i64(
+                    n + 2 * m,
+                    "computing the cover bound",
+                )?,
             ),
             source_num_vars: n,
         })

src/rules/ksatisfiability_feasibleregisterassignment.rs

@@ -1,9 +1,8 @@
 //! Reduction from KSatisfiability (3-SAT) to Feasible Register Assignment.
 //!
 //! This follows Sethi's Reduction 3 / Theorem 5.11 (STOC 1973):
-//! Nonempty short clauses are padded by literal repetition, an empty clause
-//! maps to a fixed infeasible DAG, and appearing variables are compacted with
-//! an inverse map. No ordering or distinct-variable hypothesis is needed.
+//! Appearing variables are compacted with an inverse map. No ordering or
+//! distinct-variable hypothesis is needed.
 //! - Variable leaf pairs `s_pos[k], s_neg[k]` share register `S[k]`
 //! - Each literal occurrence adds `p[i,j], q[i,j], r[i,j], rbar[i,j]`
 //! - `r[i,j]` and `rbar[i,j]` share register `R[i,j]`
@@ -109,19 +108,6 @@ impl ReduceTo<FeasibleRegisterAssignment> for KSatisfiability<K3> {
     type Result = Reduction3SATToFeasibleRegisterAssignment;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        if self
-            .clauses()
-            .iter()
-            .any(|clause| clause.literals.is_empty())
-        {
-            // Both predecessors must remain live until vertex 2, but they
-            // share a register. This acyclic target has no realization.
-            return Ok(Reduction3SATToFeasibleRegisterAssignment {
-                target: FeasibleRegisterAssignment::new(3, vec![(2, 0), (2, 1)], 2, vec![0, 0, 1]),
-                num_vars: self.num_vars(),
-                source_variables: Vec::new(),
-            });
-        }
         let source_variables: Vec<_> = self
             .clauses()
             .iter()
@@ -166,10 +152,9 @@ impl ReduceTo<FeasibleRegisterAssignment> for KSatisfiability<K3> {
         }
 
         for (clause_idx, clause) in self.clauses().iter().enumerate() {
-            // Repetition preserves a nonempty disjunction. Every occurrence
-            // keeps its own gadget and register pair, even for repeated literals.
-            let mut literals = clause.literals.clone();
-            literals.resize(3, literals[0]);
+            // Every occurrence keeps its own gadget and register pair, even
+            // for repeated literals.
+            let literals = &clause.literals;
             for literal_pos in 0..3 {
                 assignment[p_idx(num_vars, clause_idx, literal_pos)] =
                     p_register(num_vars, clause_idx, literal_pos);