problemreductions/models/satisfiability/
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).
5
6use crate::graph_types::SimpleGraph;
7use crate::traits::{ConstraintSatisfactionProblem, Problem};
8use crate::types::{EnergyMode, LocalConstraint, LocalSolutionSize, ProblemSize, SolutionSize};
9use serde::{Deserialize, Serialize};
10
11use super::CNFClause;
12
13/// K-Satisfiability problem where each clause has exactly K literals.
14///
15/// This is a restricted form of SAT where every clause must contain
16/// exactly K literals. The most famous variant is 3-SAT (K=3), which
17/// is NP-complete, while 2-SAT (K=2) is solvable in polynomial time.
18///
19/// # Type Parameters
20/// * `K` - The number of literals per clause (compile-time constant)
21/// * `W` - The weight type for MAX-K-SAT
22///
23/// # Example
24///
25/// ```
26/// use problemreductions::models::satisfiability::{KSatisfiability, CNFClause};
27/// use problemreductions::{Problem, Solver, BruteForce};
28///
29/// // 3-SAT formula: (x1 OR x2 OR x3) AND (NOT x1 OR x2 OR NOT x3)
30/// let problem = KSatisfiability::<3, i32>::new(
31///     3,
32///     vec![
33///         CNFClause::new(vec![1, 2, 3]),       // x1 OR x2 OR x3
34///         CNFClause::new(vec![-1, 2, -3]),     // NOT x1 OR x2 OR NOT x3
35///     ],
36/// );
37///
38/// let solver = BruteForce::new();
39/// let solutions = solver.find_best(&problem);
40/// assert!(!solutions.is_empty());
41/// ```
42#[derive(Debug, Clone, Serialize, Deserialize)]
43pub struct KSatisfiability<const K: usize, W = i32> {
44    /// Number of variables.
45    num_vars: usize,
46    /// Clauses in CNF, each with exactly K literals.
47    clauses: Vec<CNFClause>,
48    /// Weights for each clause (for MAX-K-SAT).
49    weights: Vec<W>,
50}
51
52impl<const K: usize, W: Clone + Default> KSatisfiability<K, W> {
53    /// Create a new K-SAT problem with unit weights.
54    ///
55    /// # Panics
56    /// Panics if any clause does not have exactly K literals.
57    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self
58    where
59        W: From<i32>,
60    {
61        for (i, clause) in clauses.iter().enumerate() {
62            assert!(
63                clause.len() == K,
64                "Clause {} has {} literals, expected {}",
65                i,
66                clause.len(),
67                K
68            );
69        }
70        let num_clauses = clauses.len();
71        let weights = vec![W::from(1); num_clauses];
72        Self {
73            num_vars,
74            clauses,
75            weights,
76        }
77    }
78
79    /// Create a new K-SAT problem allowing clauses with fewer than K literals.
80    ///
81    /// This is useful when the reduction algorithm produces clauses with
82    /// fewer literals (e.g., when allow_less is true in the Julia implementation).
83    ///
84    /// # Panics
85    /// Panics if any clause has more than K literals.
86    pub fn new_allow_less(num_vars: usize, clauses: Vec<CNFClause>) -> Self
87    where
88        W: From<i32>,
89    {
90        for (i, clause) in clauses.iter().enumerate() {
91            assert!(
92                clause.len() <= K,
93                "Clause {} has {} literals, expected at most {}",
94                i,
95                clause.len(),
96                K
97            );
98        }
99        let num_clauses = clauses.len();
100        let weights = vec![W::from(1); num_clauses];
101        Self {
102            num_vars,
103            clauses,
104            weights,
105        }
106    }
107
108    /// Create a new weighted K-SAT problem (MAX-K-SAT).
109    ///
110    /// # Panics
111    /// Panics if any clause does not have exactly K literals,
112    /// or if the number of weights doesn't match the number of clauses.
113    pub fn with_weights(num_vars: usize, clauses: Vec<CNFClause>, weights: Vec<W>) -> Self {
114        for (i, clause) in clauses.iter().enumerate() {
115            assert!(
116                clause.len() == K,
117                "Clause {} has {} literals, expected {}",
118                i,
119                clause.len(),
120                K
121            );
122        }
123        assert_eq!(clauses.len(), weights.len());
124        Self {
125            num_vars,
126            clauses,
127            weights,
128        }
129    }
130
131    /// Get the number of variables.
132    pub fn num_vars(&self) -> usize {
133        self.num_vars
134    }
135
136    /// Get the number of clauses.
137    pub fn num_clauses(&self) -> usize {
138        self.clauses.len()
139    }
140
141    /// Get the clauses.
142    pub fn clauses(&self) -> &[CNFClause] {
143        &self.clauses
144    }
145
146    /// Get a specific clause.
147    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
148        self.clauses.get(index)
149    }
150
151    /// Count satisfied clauses for an assignment.
152    pub fn count_satisfied(&self, assignment: &[bool]) -> usize {
153        self.clauses
154            .iter()
155            .filter(|c| c.is_satisfied(assignment))
156            .count()
157    }
158
159    /// Check if an assignment satisfies all clauses.
160    pub fn is_satisfying(&self, assignment: &[bool]) -> bool {
161        self.clauses.iter().all(|c| c.is_satisfied(assignment))
162    }
163
164    /// Convert a usize config to boolean assignment.
165    fn config_to_assignment(config: &[usize]) -> Vec<bool> {
166        config.iter().map(|&v| v == 1).collect()
167    }
168}
169
170impl<const K: usize, W> Problem for KSatisfiability<K, W>
171where
172    W: Clone + Default + PartialOrd + num_traits::Num + num_traits::Zero + std::ops::AddAssign + 'static,
173{
174    const NAME: &'static str = "KSatisfiability";
175    type GraphType = SimpleGraph;
176    type Weight = W;
177    type Size = W;
178
179    fn num_variables(&self) -> usize {
180        self.num_vars
181    }
182
183    fn num_flavors(&self) -> usize {
184        2 // Boolean
185    }
186
187    fn problem_size(&self) -> ProblemSize {
188        ProblemSize::new(vec![
189            ("k", K),
190            ("num_vars", self.num_vars),
191            ("num_clauses", self.clauses.len()),
192        ])
193    }
194
195    fn energy_mode(&self) -> EnergyMode {
196        EnergyMode::LargerSizeIsBetter
197    }
198
199    fn solution_size(&self, config: &[usize]) -> SolutionSize<Self::Size> {
200        let assignment = Self::config_to_assignment(config);
201        let is_valid = self.is_satisfying(&assignment);
202
203        let mut total = W::zero();
204        for (clause, weight) in self.clauses.iter().zip(&self.weights) {
205            if clause.is_satisfied(&assignment) {
206                total += weight.clone();
207            }
208        }
209
210        SolutionSize::new(total, is_valid)
211    }
212}
213
214impl<const K: usize, W> ConstraintSatisfactionProblem for KSatisfiability<K, W>
215where
216    W: Clone + Default + PartialOrd + num_traits::Num + num_traits::Zero + std::ops::AddAssign + 'static,
217{
218    fn constraints(&self) -> Vec<LocalConstraint> {
219        self.clauses
220            .iter()
221            .map(|clause| {
222                let vars = clause.variables();
223                let num_configs = 2usize.pow(vars.len() as u32);
224
225                let spec: Vec<bool> = (0..num_configs)
226                    .map(|config_idx| {
227                        let local_assignment: Vec<bool> = (0..vars.len())
228                            .map(|i| (config_idx >> (vars.len() - 1 - i)) & 1 == 1)
229                            .collect();
230
231                        let mut full_assignment = vec![false; self.num_vars];
232                        for (i, &var) in vars.iter().enumerate() {
233                            full_assignment[var] = local_assignment[i];
234                        }
235
236                        clause.is_satisfied(&full_assignment)
237                    })
238                    .collect();
239
240                LocalConstraint::new(2, vars, spec)
241            })
242            .collect()
243    }
244
245    fn objectives(&self) -> Vec<LocalSolutionSize<Self::Size>> {
246        self.clauses
247            .iter()
248            .zip(&self.weights)
249            .map(|(clause, weight)| {
250                let vars = clause.variables();
251                let num_configs = 2usize.pow(vars.len() as u32);
252
253                let spec: Vec<W> = (0..num_configs)
254                    .map(|config_idx| {
255                        let local_assignment: Vec<bool> = (0..vars.len())
256                            .map(|i| (config_idx >> (vars.len() - 1 - i)) & 1 == 1)
257                            .collect();
258
259                        let mut full_assignment = vec![false; self.num_vars];
260                        for (i, &var) in vars.iter().enumerate() {
261                            full_assignment[var] = local_assignment[i];
262                        }
263
264                        if clause.is_satisfied(&full_assignment) {
265                            weight.clone()
266                        } else {
267                            W::zero()
268                        }
269                    })
270                    .collect();
271
272                LocalSolutionSize::new(2, vars, spec)
273            })
274            .collect()
275    }
276
277    fn weights(&self) -> Vec<Self::Size> {
278        self.weights.clone()
279    }
280
281    fn set_weights(&mut self, weights: Vec<Self::Size>) {
282        assert_eq!(weights.len(), self.clauses.len());
283        self.weights = weights;
284    }
285
286    fn is_weighted(&self) -> bool {
287        if self.weights.is_empty() {
288            return false;
289        }
290        let first = &self.weights[0];
291        !self.weights.iter().all(|w| w == first)
292    }
293}
294
295#[cfg(test)]
296mod tests {
297    use super::*;
298    use crate::solvers::{BruteForce, Solver};
299
300    #[test]
301    fn test_3sat_creation() {
302        let problem = KSatisfiability::<3, i32>::new(
303            3,
304            vec![
305                CNFClause::new(vec![1, 2, 3]),
306                CNFClause::new(vec![-1, -2, 3]),
307            ],
308        );
309        assert_eq!(problem.num_vars(), 3);
310        assert_eq!(problem.num_clauses(), 2);
311    }
312
313    #[test]
314    #[should_panic(expected = "Clause 0 has 2 literals, expected 3")]
315    fn test_3sat_wrong_clause_size() {
316        let _ = KSatisfiability::<3, i32>::new(3, vec![CNFClause::new(vec![1, 2])]);
317    }
318
319    #[test]
320    fn test_2sat_creation() {
321        let problem = KSatisfiability::<2, i32>::new(
322            2,
323            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, -2])],
324        );
325        assert_eq!(problem.num_vars(), 2);
326        assert_eq!(problem.num_clauses(), 2);
327    }
328
329    #[test]
330    fn test_3sat_is_satisfying() {
331        // (x1 OR x2 OR x3) AND (NOT x1 OR NOT x2 OR NOT x3)
332        let problem = KSatisfiability::<3, i32>::new(
333            3,
334            vec![
335                CNFClause::new(vec![1, 2, 3]),
336                CNFClause::new(vec![-1, -2, -3]),
337            ],
338        );
339
340        // x1=T, x2=F, x3=F satisfies both
341        assert!(problem.is_satisfying(&[true, false, false]));
342        // x1=T, x2=T, x3=T fails second clause
343        assert!(!problem.is_satisfying(&[true, true, true]));
344    }
345
346    #[test]
347    fn test_3sat_brute_force() {
348        let problem = KSatisfiability::<3, i32>::new(
349            3,
350            vec![
351                CNFClause::new(vec![1, 2, 3]),
352                CNFClause::new(vec![-1, -2, 3]),
353            ],
354        );
355        let solver = BruteForce::new();
356        let solutions = solver.find_best(&problem);
357
358        assert!(!solutions.is_empty());
359        for sol in &solutions {
360            assert!(problem.solution_size(sol).is_valid);
361        }
362    }
363
364    #[test]
365    fn test_ksat_problem_size() {
366        let problem = KSatisfiability::<3, i32>::new(4, vec![CNFClause::new(vec![1, 2, 3])]);
367        let size = problem.problem_size();
368        assert_eq!(size.get("k"), Some(3));
369        assert_eq!(size.get("num_vars"), Some(4));
370        assert_eq!(size.get("num_clauses"), Some(1));
371    }
372
373    #[test]
374    fn test_ksat_with_weights() {
375        let problem = KSatisfiability::<3>::with_weights(
376            3,
377            vec![
378                CNFClause::new(vec![1, 2, 3]),
379                CNFClause::new(vec![-1, -2, -3]),
380            ],
381            vec![5, 10],
382        );
383        assert_eq!(problem.weights(), vec![5, 10]);
384        assert!(problem.is_weighted());
385    }
386
387    #[test]
388    fn test_ksat_allow_less() {
389        // This should work - clause has 2 literals which is <= 3
390        let problem = KSatisfiability::<3, i32>::new_allow_less(2, vec![CNFClause::new(vec![1, 2])]);
391        assert_eq!(problem.num_clauses(), 1);
392    }
393
394    #[test]
395    #[should_panic(expected = "Clause 0 has 4 literals, expected at most 3")]
396    fn test_ksat_allow_less_too_many() {
397        let _ =
398            KSatisfiability::<3, i32>::new_allow_less(4, vec![CNFClause::new(vec![1, 2, 3, 4])]);
399    }
400
401    #[test]
402    fn test_ksat_constraints() {
403        let problem = KSatisfiability::<3, i32>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
404        let constraints = problem.constraints();
405        assert_eq!(constraints.len(), 1);
406    }
407
408    #[test]
409    fn test_ksat_objectives() {
410        let problem =
411            KSatisfiability::<3>::with_weights(3, vec![CNFClause::new(vec![1, 2, 3])], vec![5]);
412        let objectives = problem.objectives();
413        assert_eq!(objectives.len(), 1);
414    }
415
416    #[test]
417    fn test_ksat_energy_mode() {
418        let problem = KSatisfiability::<3, i32>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
419        assert!(problem.energy_mode().is_maximization());
420    }
421
422    #[test]
423    fn test_ksat_get_clause() {
424        let problem = KSatisfiability::<3, i32>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
425        assert_eq!(problem.get_clause(0), Some(&CNFClause::new(vec![1, 2, 3])));
426        assert_eq!(problem.get_clause(1), None);
427    }
428
429    #[test]
430    fn test_ksat_count_satisfied() {
431        let problem = KSatisfiability::<3, i32>::new(
432            3,
433            vec![
434                CNFClause::new(vec![1, 2, 3]),
435                CNFClause::new(vec![-1, -2, -3]),
436            ],
437        );
438        // x1=T, x2=T, x3=T: first satisfied, second not
439        assert_eq!(problem.count_satisfied(&[true, true, true]), 1);
440        // x1=T, x2=F, x3=F: both satisfied
441        assert_eq!(problem.count_satisfied(&[true, false, false]), 2);
442    }
443
444    #[test]
445    fn test_ksat_set_weights() {
446        let mut problem = KSatisfiability::<3, i32>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
447        assert!(!problem.is_weighted());
448        problem.set_weights(vec![10]);
449        assert_eq!(problem.weights(), vec![10]);
450    }
451
452    #[test]
453    fn test_ksat_is_satisfied_csp() {
454        let problem = KSatisfiability::<3, i32>::new(
455            3,
456            vec![
457                CNFClause::new(vec![1, 2, 3]),
458                CNFClause::new(vec![-1, -2, -3]),
459            ],
460        );
461        assert!(problem.is_satisfied(&[1, 0, 0])); // x1=T, x2=F, x3=F
462        assert!(!problem.is_satisfied(&[1, 1, 1])); // x1=T, x2=T, x3=T
463    }
464}
problemreductions/models/satisfiability/ksat.rs

problemreductions/models/satisfiability/
ksat.rs
