problemreductions/models/satisfiability/
sat.rs

1//! Boolean Satisfiability (SAT) problem implementation.
2//!
3//! SAT is the problem of determining if there exists an assignment of
4//! Boolean variables that makes a given Boolean formula true.
5
6use crate::graph_types::SimpleGraph;
7use crate::traits::{ConstraintSatisfactionProblem, Problem};
8use crate::types::{EnergyMode, LocalConstraint, LocalSolutionSize, ProblemSize, SolutionSize};
9use serde::{Deserialize, Serialize};
10
11/// A clause in conjunctive normal form (CNF).
12///
13/// A clause is a disjunction (OR) of literals.
14/// Literals are represented as signed integers:
15/// - Positive i means variable i
16/// - Negative -i means NOT variable i
17///
18/// Variables are 1-indexed in the external representation but
19/// 0-indexed internally.
20#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
21pub struct CNFClause {
22    /// Literals in this clause (signed integers, 1-indexed).
23    pub literals: Vec<i32>,
24}
25
26impl CNFClause {
27    /// Create a new clause from literals.
28    ///
29    /// Literals are signed integers where positive means the variable
30    /// and negative means its negation. Variables are 1-indexed.
31    pub fn new(literals: Vec<i32>) -> Self {
32        Self { literals }
33    }
34
35    /// Check if the clause is satisfied by an assignment.
36    ///
37    /// # Arguments
38    /// * `assignment` - Boolean assignment, 0-indexed
39    pub fn is_satisfied(&self, assignment: &[bool]) -> bool {
40        self.literals.iter().any(|&lit| {
41            let var = lit.unsigned_abs() as usize - 1; // Convert to 0-indexed
42            let value = assignment.get(var).copied().unwrap_or(false);
43            if lit > 0 {
44                value
45            } else {
46                !value
47            }
48        })
49    }
50
51    /// Get the variables involved in this clause (0-indexed).
52    pub fn variables(&self) -> Vec<usize> {
53        self.literals
54            .iter()
55            .map(|&lit| lit.unsigned_abs() as usize - 1)
56            .collect()
57    }
58
59    /// Get the number of literals.
60    pub fn len(&self) -> usize {
61        self.literals.len()
62    }
63
64    /// Check if the clause is empty.
65    pub fn is_empty(&self) -> bool {
66        self.literals.is_empty()
67    }
68}
69
70/// Boolean Satisfiability (SAT) problem in CNF form.
71///
72/// Given a Boolean formula in conjunctive normal form (CNF),
73/// determine if there exists an assignment that satisfies all clauses.
74///
75/// The problem can be weighted, where the goal is to maximize the
76/// total weight of satisfied clauses (MAX-SAT).
77///
78/// # Example
79///
80/// ```
81/// use problemreductions::models::satisfiability::{Satisfiability, CNFClause};
82/// use problemreductions::{Problem, Solver, BruteForce};
83///
84/// // Formula: (x1 OR x2) AND (NOT x1 OR x3) AND (NOT x2 OR NOT x3)
85/// let problem = Satisfiability::<i32>::new(
86///     3,
87///     vec![
88///         CNFClause::new(vec![1, 2]),      // x1 OR x2
89///         CNFClause::new(vec![-1, 3]),     // NOT x1 OR x3
90///         CNFClause::new(vec![-2, -3]),    // NOT x2 OR NOT x3
91///     ],
92/// );
93///
94/// let solver = BruteForce::new();
95/// let solutions = solver.find_best(&problem);
96///
97/// // Verify solutions satisfy all clauses
98/// for sol in solutions {
99///     assert!(problem.solution_size(&sol).is_valid);
100/// }
101/// ```
102#[derive(Debug, Clone, Serialize, Deserialize)]
103pub struct Satisfiability<W = i32> {
104    /// Number of variables.
105    num_vars: usize,
106    /// Clauses in CNF.
107    clauses: Vec<CNFClause>,
108    /// Weights for each clause (for MAX-SAT).
109    weights: Vec<W>,
110}
111
112impl<W: Clone + Default> Satisfiability<W> {
113    /// Create a new SAT problem with unit weights.
114    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self
115    where
116        W: From<i32>,
117    {
118        let num_clauses = clauses.len();
119        let weights = vec![W::from(1); num_clauses];
120        Self {
121            num_vars,
122            clauses,
123            weights,
124        }
125    }
126
127    /// Create a new weighted SAT problem (MAX-SAT).
128    pub fn with_weights(num_vars: usize, clauses: Vec<CNFClause>, weights: Vec<W>) -> Self {
129        assert_eq!(clauses.len(), weights.len());
130        Self {
131            num_vars,
132            clauses,
133            weights,
134        }
135    }
136
137    /// Get the number of variables.
138    pub fn num_vars(&self) -> usize {
139        self.num_vars
140    }
141
142    /// Get the number of clauses.
143    pub fn num_clauses(&self) -> usize {
144        self.clauses.len()
145    }
146
147    /// Get the clauses.
148    pub fn clauses(&self) -> &[CNFClause] {
149        &self.clauses
150    }
151
152    /// Get a specific clause.
153    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
154        self.clauses.get(index)
155    }
156
157    /// Count satisfied clauses for an assignment.
158    pub fn count_satisfied(&self, assignment: &[bool]) -> usize {
159        self.clauses
160            .iter()
161            .filter(|c| c.is_satisfied(assignment))
162            .count()
163    }
164
165    /// Check if an assignment satisfies all clauses.
166    pub fn is_satisfying(&self, assignment: &[bool]) -> bool {
167        self.clauses.iter().all(|c| c.is_satisfied(assignment))
168    }
169
170    /// Convert a usize config to boolean assignment.
171    fn config_to_assignment(config: &[usize]) -> Vec<bool> {
172        config.iter().map(|&v| v == 1).collect()
173    }
174}
175
176impl<W> Problem for Satisfiability<W>
177where
178    W: Clone + Default + PartialOrd + num_traits::Num + num_traits::Zero + std::ops::AddAssign + 'static,
179{
180    const NAME: &'static str = "Satisfiability";
181    type GraphType = SimpleGraph;
182    type Weight = W;
183    type Size = W;
184
185    fn num_variables(&self) -> usize {
186        self.num_vars
187    }
188
189    fn num_flavors(&self) -> usize {
190        2 // Boolean
191    }
192
193    fn problem_size(&self) -> ProblemSize {
194        ProblemSize::new(vec![
195            ("num_vars", self.num_vars),
196            ("num_clauses", self.clauses.len()),
197        ])
198    }
199
200    fn energy_mode(&self) -> EnergyMode {
201        // For standard SAT, we maximize satisfied clauses (all must be satisfied)
202        // For MAX-SAT, we maximize weighted sum of satisfied clauses
203        EnergyMode::LargerSizeIsBetter
204    }
205
206    fn solution_size(&self, config: &[usize]) -> SolutionSize<Self::Size> {
207        let assignment = Self::config_to_assignment(config);
208        let is_valid = self.is_satisfying(&assignment);
209
210        // Compute weighted sum of satisfied clauses
211        let mut total = W::zero();
212        for (clause, weight) in self.clauses.iter().zip(&self.weights) {
213            if clause.is_satisfied(&assignment) {
214                total += weight.clone();
215            }
216        }
217
218        SolutionSize::new(total, is_valid)
219    }
220}
221
222impl<W> ConstraintSatisfactionProblem for Satisfiability<W>
223where
224    W: Clone + Default + PartialOrd + num_traits::Num + num_traits::Zero + std::ops::AddAssign + 'static,
225{
226    fn constraints(&self) -> Vec<LocalConstraint> {
227        // Each clause is a constraint
228        self.clauses
229            .iter()
230            .map(|clause| {
231                let vars = clause.variables();
232                let num_configs = 2usize.pow(vars.len() as u32);
233
234                // Build spec: config is valid if clause is satisfied
235                let spec: Vec<bool> = (0..num_configs)
236                    .map(|config_idx| {
237                        // Convert config index to local assignment
238                        let local_assignment: Vec<bool> = (0..vars.len())
239                            .map(|i| (config_idx >> (vars.len() - 1 - i)) & 1 == 1)
240                            .collect();
241
242                        // Build full assignment for clause evaluation
243                        let mut full_assignment = vec![false; self.num_vars];
244                        for (i, &var) in vars.iter().enumerate() {
245                            full_assignment[var] = local_assignment[i];
246                        }
247
248                        clause.is_satisfied(&full_assignment)
249                    })
250                    .collect();
251
252                LocalConstraint::new(2, vars, spec)
253            })
254            .collect()
255    }
256
257    fn objectives(&self) -> Vec<LocalSolutionSize<Self::Size>> {
258        // For MAX-SAT, each clause contributes its weight if satisfied
259        self.clauses
260            .iter()
261            .zip(&self.weights)
262            .map(|(clause, weight)| {
263                let vars = clause.variables();
264                let num_configs = 2usize.pow(vars.len() as u32);
265
266                let spec: Vec<W> = (0..num_configs)
267                    .map(|config_idx| {
268                        let local_assignment: Vec<bool> = (0..vars.len())
269                            .map(|i| (config_idx >> (vars.len() - 1 - i)) & 1 == 1)
270                            .collect();
271
272                        let mut full_assignment = vec![false; self.num_vars];
273                        for (i, &var) in vars.iter().enumerate() {
274                            full_assignment[var] = local_assignment[i];
275                        }
276
277                        if clause.is_satisfied(&full_assignment) {
278                            weight.clone()
279                        } else {
280                            W::zero()
281                        }
282                    })
283                    .collect();
284
285                LocalSolutionSize::new(2, vars, spec)
286            })
287            .collect()
288    }
289
290    fn weights(&self) -> Vec<Self::Size> {
291        self.weights.clone()
292    }
293
294    fn set_weights(&mut self, weights: Vec<Self::Size>) {
295        assert_eq!(weights.len(), self.clauses.len());
296        self.weights = weights;
297    }
298
299    fn is_weighted(&self) -> bool {
300        if self.weights.is_empty() {
301            return false;
302        }
303        let first = &self.weights[0];
304        !self.weights.iter().all(|w| w == first)
305    }
306}
307
308/// Check if an assignment satisfies a SAT formula.
309///
310/// # Arguments
311/// * `num_vars` - Number of variables
312/// * `clauses` - Clauses as vectors of literals (1-indexed, signed)
313/// * `assignment` - Boolean assignment (0-indexed)
314pub fn is_satisfying_assignment(
315    _num_vars: usize,
316    clauses: &[Vec<i32>],
317    assignment: &[bool],
318) -> bool {
319    clauses.iter().all(|clause| {
320        clause.iter().any(|&lit| {
321            let var = lit.unsigned_abs() as usize - 1;
322            let value = assignment.get(var).copied().unwrap_or(false);
323            if lit > 0 {
324                value
325            } else {
326                !value
327            }
328        })
329    })
330}
331
332#[cfg(test)]
333mod tests {
334    use super::*;
335    use crate::solvers::{BruteForce, Solver};
336
337    #[test]
338    fn test_cnf_clause_creation() {
339        let clause = CNFClause::new(vec![1, -2, 3]);
340        assert_eq!(clause.len(), 3);
341        assert!(!clause.is_empty());
342        assert_eq!(clause.variables(), vec![0, 1, 2]);
343    }
344
345    #[test]
346    fn test_cnf_clause_satisfaction() {
347        let clause = CNFClause::new(vec![1, 2]); // x1 OR x2
348
349        assert!(clause.is_satisfied(&[true, false])); // x1 = T
350        assert!(clause.is_satisfied(&[false, true])); // x2 = T
351        assert!(clause.is_satisfied(&[true, true])); // Both T
352        assert!(!clause.is_satisfied(&[false, false])); // Both F
353    }
354
355    #[test]
356    fn test_cnf_clause_negation() {
357        let clause = CNFClause::new(vec![-1, 2]); // NOT x1 OR x2
358
359        assert!(clause.is_satisfied(&[false, false])); // NOT x1 = T
360        assert!(clause.is_satisfied(&[false, true])); // Both true
361        assert!(clause.is_satisfied(&[true, true])); // x2 = T
362        assert!(!clause.is_satisfied(&[true, false])); // Both false
363    }
364
365    #[test]
366    fn test_sat_creation() {
367        let problem = Satisfiability::<i32>::new(
368            3,
369            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 3])],
370        );
371        assert_eq!(problem.num_vars(), 3);
372        assert_eq!(problem.num_clauses(), 2);
373        assert_eq!(problem.num_variables(), 3);
374    }
375
376    #[test]
377    fn test_sat_with_weights() {
378        let problem = Satisfiability::with_weights(
379            2,
380            vec![CNFClause::new(vec![1]), CNFClause::new(vec![2])],
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_is_satisfying() {
389        // (x1 OR x2) AND (NOT x1 OR NOT x2)
390        let problem = Satisfiability::<i32>::new(
391            2,
392            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, -2])],
393        );
394
395        assert!(problem.is_satisfying(&[true, false])); // Satisfies both
396        assert!(problem.is_satisfying(&[false, true])); // Satisfies both
397        assert!(!problem.is_satisfying(&[true, true])); // Fails second clause
398        assert!(!problem.is_satisfying(&[false, false])); // Fails first clause
399    }
400
401    #[test]
402    fn test_count_satisfied() {
403        let problem = Satisfiability::<i32>::new(
404            2,
405            vec![CNFClause::new(vec![1]), CNFClause::new(vec![2]), CNFClause::new(vec![-1, -2])],
406        );
407
408        assert_eq!(problem.count_satisfied(&[true, true]), 2); // x1, x2 satisfied
409        assert_eq!(problem.count_satisfied(&[false, false]), 1); // Only last
410        assert_eq!(problem.count_satisfied(&[true, false]), 2); // x1 and last
411    }
412
413    #[test]
414    fn test_solution_size() {
415        let problem = Satisfiability::<i32>::new(
416            2,
417            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, -2])],
418        );
419
420        let sol = problem.solution_size(&[1, 0]); // true, false
421        assert!(sol.is_valid);
422        assert_eq!(sol.size, 2); // Both clauses satisfied
423
424        let sol = problem.solution_size(&[1, 1]); // true, true
425        assert!(!sol.is_valid);
426        assert_eq!(sol.size, 1); // Only first clause satisfied
427    }
428
429    #[test]
430    fn test_brute_force_satisfiable() {
431        // (x1) AND (x2) AND (NOT x1 OR NOT x2) - UNSAT
432        let problem = Satisfiability::<i32>::new(
433            2,
434            vec![
435                CNFClause::new(vec![1]),
436                CNFClause::new(vec![2]),
437                CNFClause::new(vec![-1, -2]),
438            ],
439        );
440        let solver = BruteForce::new();
441
442        let solutions = solver.find_best(&problem);
443        // This is unsatisfiable, so no valid solutions
444        // BruteForce will return configs with max satisfied clauses
445        for sol in &solutions {
446            // Best we can do is satisfy 2 out of 3 clauses
447            assert!(!problem.solution_size(sol).is_valid);
448            assert_eq!(problem.solution_size(sol).size, 2);
449        }
450    }
451
452    #[test]
453    fn test_brute_force_simple_sat() {
454        // (x1 OR x2) - many solutions
455        let problem = Satisfiability::<i32>::new(2, vec![CNFClause::new(vec![1, 2])]);
456        let solver = BruteForce::new();
457
458        let solutions = solver.find_best(&problem);
459        // 3 satisfying assignments
460        assert_eq!(solutions.len(), 3);
461        for sol in &solutions {
462            assert!(problem.solution_size(sol).is_valid);
463        }
464    }
465
466    #[test]
467    fn test_max_sat() {
468        // Weighted: clause 1 has weight 10, clause 2 has weight 1
469        // They conflict, so we prefer satisfying clause 1
470        let problem = Satisfiability::with_weights(
471            1,
472            vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
473            vec![10, 1],
474        );
475        let solver = BruteForce::new().valid_only(false); // Allow invalid (partial) solutions
476
477        let solutions = solver.find_best(&problem);
478        // Should select x1 = true (weight 10)
479        assert_eq!(solutions.len(), 1);
480        assert_eq!(solutions[0], vec![1]);
481    }
482
483    #[test]
484    fn test_is_satisfying_assignment() {
485        let clauses = vec![vec![1, 2], vec![-1, 3]];
486
487        assert!(is_satisfying_assignment(3, &clauses, &[true, false, true]));
488        assert!(is_satisfying_assignment(3, &clauses, &[false, true, false]));
489        assert!(!is_satisfying_assignment(3, &clauses, &[true, false, false]));
490    }
491
492    #[test]
493    fn test_constraints() {
494        let problem = Satisfiability::<i32>::new(
495            2,
496            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1])],
497        );
498        let constraints = problem.constraints();
499        assert_eq!(constraints.len(), 2);
500    }
501
502    #[test]
503    fn test_energy_mode() {
504        let problem = Satisfiability::<i32>::new(2, vec![CNFClause::new(vec![1])]);
505        assert!(problem.energy_mode().is_maximization());
506    }
507
508    #[test]
509    fn test_empty_formula() {
510        let problem = Satisfiability::<i32>::new(2, vec![]);
511        let sol = problem.solution_size(&[0, 0]);
512        assert!(sol.is_valid); // Empty formula is trivially satisfied
513    }
514
515    #[test]
516    fn test_single_literal_clauses() {
517        // Unit propagation scenario: x1 AND NOT x2
518        let problem = Satisfiability::<i32>::new(
519            2,
520            vec![CNFClause::new(vec![1]), CNFClause::new(vec![-2])],
521        );
522        let solver = BruteForce::new();
523
524        let solutions = solver.find_best(&problem);
525        assert_eq!(solutions.len(), 1);
526        assert_eq!(solutions[0], vec![1, 0]); // x1=T, x2=F
527    }
528
529    #[test]
530    fn test_get_clause() {
531        let problem = Satisfiability::<i32>::new(
532            2,
533            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1])],
534        );
535        assert_eq!(problem.get_clause(0), Some(&CNFClause::new(vec![1, 2])));
536        assert_eq!(problem.get_clause(2), None);
537    }
538
539    #[test]
540    fn test_three_sat_example() {
541        // (x1 OR x2 OR x3) AND (NOT x1 OR NOT x2 OR x3) AND (x1 OR NOT x2 OR NOT x3)
542        let problem = Satisfiability::<i32>::new(
543            3,
544            vec![
545                CNFClause::new(vec![1, 2, 3]),
546                CNFClause::new(vec![-1, -2, 3]),
547                CNFClause::new(vec![1, -2, -3]),
548            ],
549        );
550        let solver = BruteForce::new();
551
552        let solutions = solver.find_best(&problem);
553        for sol in &solutions {
554            assert!(problem.solution_size(sol).is_valid);
555        }
556    }
557
558    #[test]
559    fn test_is_satisfied_csp() {
560        let problem = Satisfiability::<i32>::new(
561            2,
562            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, -2])],
563        );
564
565        assert!(problem.is_satisfied(&[1, 0]));
566        assert!(problem.is_satisfied(&[0, 1]));
567        assert!(!problem.is_satisfied(&[1, 1]));
568        assert!(!problem.is_satisfied(&[0, 0]));
569    }
570
571    #[test]
572    fn test_objectives() {
573        let problem = Satisfiability::with_weights(
574            2,
575            vec![CNFClause::new(vec![1, 2])],
576            vec![5],
577        );
578        let objectives = problem.objectives();
579        assert_eq!(objectives.len(), 1);
580    }
581
582    #[test]
583    fn test_set_weights() {
584        let mut problem = Satisfiability::<i32>::new(
585            2,
586            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1])],
587        );
588        assert!(!problem.is_weighted()); // Initially uniform
589        problem.set_weights(vec![1, 2]);
590        assert!(problem.is_weighted());
591        assert_eq!(problem.weights(), vec![1, 2]);
592    }
593
594    #[test]
595    fn test_is_weighted_empty() {
596        let problem = Satisfiability::<i32>::new(2, vec![]);
597        assert!(!problem.is_weighted());
598    }
599
600    #[test]
601    fn test_is_satisfying_assignment_defaults() {
602        // When assignment is shorter than needed, missing vars default to false
603        let clauses = vec![vec![1, 2]];
604        // assignment is [true], var 0 = true satisfies literal 1
605        assert!(is_satisfying_assignment(3, &clauses, &[true]));
606        // assignment is [false], var 0 = false, var 1 defaults to false
607        // Neither literal 1 (var0=false) nor literal 2 (var1=false) satisfied
608        assert!(!is_satisfying_assignment(3, &clauses, &[false]));
609    }
610
611    #[test]
612    fn test_problem_size() {
613        let problem = Satisfiability::<i32>::new(
614            3,
615            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 3])],
616        );
617        let size = problem.problem_size();
618        assert_eq!(size.get("num_vars"), Some(3));
619        assert_eq!(size.get("num_clauses"), Some(2));
620    }
621
622    #[test]
623    fn test_num_variables_flavors() {
624        let problem = Satisfiability::<i32>::new(5, vec![CNFClause::new(vec![1])]);
625        assert_eq!(problem.num_variables(), 5);
626        assert_eq!(problem.num_flavors(), 2);
627    }
628
629    #[test]
630    fn test_clause_variables() {
631        let clause = CNFClause::new(vec![1, -2, 3]);
632        let vars = clause.variables();
633        assert_eq!(vars, vec![0, 1, 2]); // 0-indexed
634    }
635
636    #[test]
637    fn test_clause_debug() {
638        let clause = CNFClause::new(vec![1, -2, 3]);
639        let debug = format!("{:?}", clause);
640        assert!(debug.contains("CNFClause"));
641    }
642}
problemreductions/models/satisfiability/sat.rs

problemreductions/models/satisfiability/
sat.rs
