problemreductions/models/formula/
ksat.rs

1//! K-Satisfiability (K-SAT) problem implementation.
2//!
3//! K-SAT is a special case of SAT where each clause has exactly K literals.
4//! Common variants include 3-SAT (K=3) and 2-SAT (K=2). This is the decision
5//! version - for the optimization variant (MAX-K-SAT), see the separate
6//! MaxKSatisfiability type (if available).
7
8use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension};
9use crate::traits::Problem;
10use crate::variant::{KValue, K2, K3, KN};
11use serde::{de::Error as _, Deserialize, Deserializer, Serialize};
12
13use super::{sat::validate_cnf_literals, CNFClause};
14
15pub(crate) fn first_n_odd_primes(count: usize) -> Vec<u64> {
16    let mut primes = Vec::with_capacity(count);
17    let mut candidate = 3u64;
18
19    while primes.len() < count {
20        if is_prime(candidate) {
21            primes.push(candidate);
22        }
23        candidate += 2;
24    }
25
26    primes
27}
28
29fn is_prime(candidate: u64) -> bool {
30    if candidate < 2 {
31        return false;
32    }
33    if candidate == 2 {
34        return true;
35    }
36    if candidate.is_multiple_of(2) {
37        return false;
38    }
39
40    let mut divisor = 3u64;
41    while divisor * divisor <= candidate {
42        if candidate.is_multiple_of(divisor) {
43            return false;
44        }
45        divisor += 2;
46    }
47
48    true
49}
50
51inventory::submit! {
52    ProblemSchemaEntry {
53        name: "KSatisfiability",
54        display_name: "K-Satisfiability",
55        aliases: &["KSAT"],
56        dimensions: &[VariantDimension::new("k", "KN", &["KN", "K2", "K3"])],
57        category: crate::registry::ProblemCategory::Formula,
58        module_path: module_path!(),
59        description: "SAT with exactly k literals per clause",
60        fields: &[
61            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
62            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Clauses each with exactly K literals" },
63        ],
64    }
65}
66
67/// K-Satisfiability problem where each clause has exactly K literals.
68///
69/// This is a restricted form of SAT where every clause must contain
70/// exactly K literals. The most famous variant is 3-SAT (K=3), which
71/// is NP-complete, while 2-SAT (K=2) is solvable in polynomial time.
72/// This is the decision version of the problem.
73///
74/// # Type Parameters
75/// * `K` - A type implementing `KValue` that specifies the number of literals per clause
76///
77/// # Example
78///
79/// ```
80/// use problemreductions::models::formula::{KSatisfiability, CNFClause};
81/// use problemreductions::variant::K3;
82/// use problemreductions::{Problem, BruteForce};
83///
84/// // 3-SAT formula: (x1 OR x2 OR x3) AND (NOT x1 OR x2 OR NOT x3)
85/// let problem = KSatisfiability::<K3>::new(
86///     3,
87///     vec![
88///         CNFClause::new(vec![1, 2, 3]),       // x1 OR x2 OR x3
89///         CNFClause::new(vec![-1, 2, -3]),     // NOT x1 OR x2 OR NOT x3
90///     ],
91/// );
92///
93/// let solver = BruteForce::new();
94/// let solutions = solver.find_all_witnesses(&problem).unwrap();
95/// assert!(!solutions.is_empty());
96/// ```
97#[derive(Debug, Clone, Serialize)]
98pub struct KSatisfiability<K: KValue> {
99    /// Number of variables.
100    num_vars: usize,
101    /// Clauses in CNF, each with exactly K literals.
102    clauses: Vec<CNFClause>,
103    #[serde(skip)]
104    _phantom: std::marker::PhantomData<K>,
105}
106
107#[derive(Deserialize)]
108struct KSatisfiabilityDef {
109    num_vars: usize,
110    clauses: Vec<CNFClause>,
111}
112
113impl<'de, K: KValue> Deserialize<'de> for KSatisfiability<K> {
114    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
115    where
116        D: Deserializer<'de>,
117    {
118        let value = KSatisfiabilityDef::deserialize(deserializer)?;
119        Self::try_new(value.num_vars, value.clauses).map_err(D::Error::custom)
120    }
121}
122
123impl<K: KValue> KSatisfiability<K> {
124    /// Create a new K-SAT problem.
125    ///
126    /// # Panics
127    /// Panics if any clause does not have exactly K literals (when K is a
128    /// concrete value like K2, K3). When K is KN (arbitrary), no clause-length
129    /// validation is performed.
130    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
131        Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
132    }
133
134    /// Create a K-SAT problem after validating its clauses.
135    pub fn try_new(
136        num_vars: usize,
137        clauses: Vec<CNFClause>,
138    ) -> Result<Self, crate::registry::ConstructionError> {
139        validate_cnf_literals(num_vars, &clauses)?;
140        if let Some(k) = K::K {
141            for (i, clause) in clauses.iter().enumerate() {
142                if clause.len() != k {
143                    return Err(
144                        format!("Clause {i} has {} literals, expected {k}", clause.len()).into(),
145                    );
146                }
147            }
148        }
149        Ok(Self {
150            num_vars,
151            clauses,
152            _phantom: std::marker::PhantomData,
153        })
154    }
155
156    /// Create a new K-SAT problem allowing clauses with fewer than K literals.
157    ///
158    /// This is useful when the reduction algorithm produces clauses with
159    /// fewer literals (e.g., when allow_less is true in the Julia implementation).
160    ///
161    /// # Panics
162    /// Panics if any clause has more than K literals (when K is a concrete
163    /// value like K2, K3). When K is KN (arbitrary), no clause-length
164    /// validation is performed.
165    pub fn new_allow_less(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
166        Self::try_new_allow_less(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
167    }
168
169    /// Create a K-SAT problem with shorter clauses after validation.
170    pub fn try_new_allow_less(
171        num_vars: usize,
172        clauses: Vec<CNFClause>,
173    ) -> Result<Self, crate::registry::ConstructionError> {
174        validate_cnf_literals(num_vars, &clauses)?;
175        if let Some(k) = K::K {
176            for (i, clause) in clauses.iter().enumerate() {
177                if clause.len() > k {
178                    return Err(format!(
179                        "Clause {i} has {} literals, expected at most {k}",
180                        clause.len()
181                    )
182                    .into());
183                }
184            }
185        }
186        Ok(Self {
187            num_vars,
188            clauses,
189            _phantom: std::marker::PhantomData,
190        })
191    }
192
193    /// Get the number of variables.
194    pub fn num_vars(&self) -> usize {
195        self.num_vars
196    }
197
198    /// Get the number of clauses.
199    pub fn num_clauses(&self) -> usize {
200        self.clauses.len()
201    }
202
203    /// Get the clauses.
204    pub fn clauses(&self) -> &[CNFClause] {
205        &self.clauses
206    }
207
208    /// Get a specific clause.
209    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
210        self.clauses.get(index)
211    }
212
213    /// Get the total number of literals across all clauses.
214    pub fn num_literals(&self) -> usize {
215        self.clauses().iter().map(|c| c.len()).sum()
216    }
217
218    /// Count satisfied clauses for an assignment.
219    pub fn count_satisfied(
220        &self,
221        assignment: &[bool],
222    ) -> Result<i64, crate::traits::EvaluationError> {
223        let count = self
224            .clauses
225            .iter()
226            .filter(|c| c.is_satisfied(assignment))
227            .count();
228        i64::try_from(count).map_err(|_| {
229            crate::traits::EvaluationError::IntegerOverflow(
230                "converting satisfied-clause count to i64".into(),
231            )
232        })
233    }
234
235    /// Check if an assignment satisfies all clauses.
236    pub fn is_satisfying(&self, assignment: &[bool]) -> bool {
237        self.clauses.iter().all(|c| c.is_satisfied(assignment))
238    }
239}
240
241impl<K: KValue> Problem for KSatisfiability<K> {
242    const NAME: &'static str = "KSatisfiability";
243    type Solution = Vec<bool>;
244    type Value = crate::types::Or;
245
246    crate::problem_parameters![
247        ("num_clauses", num_clauses),
248        ("num_literals", num_literals),
249        ("num_vars", num_vars),
250    ];
251
252    fn evaluate(
253        &self,
254        config: &Self::Solution,
255    ) -> Result<crate::types::Or, crate::traits::EvaluationError> {
256        if config.len() != self.num_vars {
257            return Err(crate::traits::EvaluationError::InvalidConfiguration(
258                "assignment length does not match the formula variables".into(),
259            ));
260        }
261        Ok(crate::types::Or(self.is_satisfying(config)))
262    }
263
264    fn variant() -> Vec<(&'static str, &'static str)> {
265        crate::variant_params![K]
266    }
267}
268
269impl<K: KValue> crate::solvers::BruteForceProblem for KSatisfiability<K> {
270    fn dimensions(&self) -> Vec<usize> {
271        vec![2; self.num_vars]
272    }
273}
274
275crate::declare_variants! {
276    default KSatisfiability<KN> => "2^num_vars",
277    KSatisfiability<K2> => "num_vars + num_clauses" aliases ["2SAT"],
278    KSatisfiability<K3> => "1.307^num_vars" aliases ["3SAT"],
279}
280
281crate::register_brute_force! {
282    KSatisfiability<KN> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
283    KSatisfiability<K2> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
284    KSatisfiability<K3> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
285}
286
287#[cfg(feature = "example-db")]
288pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
289    use super::CNFClause;
290    vec![crate::example_db::specs::ModelExampleSpec {
291        id: "ksatisfiability_k3",
292        instance: Box::new(KSatisfiability::<K3>::new(
293            3,
294            vec![
295                CNFClause::new(vec![1, 2, 3]),
296                CNFClause::new(vec![-1, -2, 3]),
297                CNFClause::new(vec![1, -2, -3]),
298            ],
299        )),
300        optimal_config: serde_json::json!(vec![false, false, true]),
301        optimal_value: serde_json::json!(true),
302    }]
303}
304
305#[cfg(test)]
306#[path = "../../unit_tests/models/formula/ksat.rs"]
307mod tests;
problemreductions/models/formula/ksat.rs

problemreductions/models/formula/
ksat.rs
