problemreductions/models/formula/
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. This is
5//! the decision version - for the optimization variant (MAX-SAT), see
6//! the separate MaxSatisfiability type (if available).
7
8use crate::registry::{FieldInfo, ProblemSchemaEntry};
9use crate::traits::Problem;
10use serde::{Deserialize, Serialize};
11
12inventory::submit! {
13    ProblemSchemaEntry {
14        name: "Satisfiability",
15        display_name: "Satisfiability",
16        aliases: &["SAT"],
17        dimensions: &[],
18        module_path: module_path!(),
19        description: "Find satisfying assignment for CNF formula",
20        fields: &[
21            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
22            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Clauses in conjunctive normal form" },
23        ],
24    }
25}
26
27/// A clause in conjunctive normal form (CNF).
28///
29/// A clause is a disjunction (OR) of literals.
30/// Literals are represented as signed integers:
31/// - Positive i means variable i
32/// - Negative -i means NOT variable i
33///
34/// Variables are 1-indexed in the external representation but
35/// 0-indexed internally.
36#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
37pub struct CNFClause {
38    /// Literals in this clause (signed integers, 1-indexed).
39    pub literals: Vec<i32>,
40}
41
42impl CNFClause {
43    /// Create a new clause from literals.
44    ///
45    /// Literals are signed integers where positive means the variable
46    /// and negative means its negation. Variables are 1-indexed.
47    pub fn new(literals: Vec<i32>) -> Self {
48        Self { literals }
49    }
50
51    /// Check if the clause is satisfied by an assignment.
52    ///
53    /// # Arguments
54    /// * `assignment` - Boolean assignment, 0-indexed
55    pub fn is_satisfied(&self, assignment: &[bool]) -> bool {
56        self.literals.iter().any(|&lit| {
57            let var = lit.unsigned_abs() as usize - 1; // Convert to 0-indexed
58            let value = assignment.get(var).copied().unwrap_or(false);
59            if lit > 0 {
60                value
61            } else {
62                !value
63            }
64        })
65    }
66
67    /// Get the variables involved in this clause (0-indexed).
68    pub fn variables(&self) -> Vec<usize> {
69        self.literals
70            .iter()
71            .map(|&lit| lit.unsigned_abs() as usize - 1)
72            .collect()
73    }
74
75    /// Get the number of literals.
76    pub fn len(&self) -> usize {
77        self.literals.len()
78    }
79
80    /// Check if the clause is empty.
81    pub fn is_empty(&self) -> bool {
82        self.literals.is_empty()
83    }
84}
85
86/// Boolean Satisfiability (SAT) problem in CNF form.
87///
88/// Given a Boolean formula in conjunctive normal form (CNF),
89/// determine if there exists an assignment that satisfies all clauses.
90/// This is the decision version of the problem.
91///
92/// # Example
93///
94/// ```
95/// use problemreductions::models::formula::{Satisfiability, CNFClause};
96/// use problemreductions::{Problem, Solver, BruteForce};
97///
98/// // Formula: (x1 OR x2) AND (NOT x1 OR x3) AND (NOT x2 OR NOT x3)
99/// let problem = Satisfiability::new(
100///     3,
101///     vec![
102///         CNFClause::new(vec![1, 2]),      // x1 OR x2
103///         CNFClause::new(vec![-1, 3]),     // NOT x1 OR x3
104///         CNFClause::new(vec![-2, -3]),    // NOT x2 OR NOT x3
105///     ],
106/// );
107///
108/// let solver = BruteForce::new();
109/// let solutions = solver.find_all_witnesses(&problem);
110///
111/// // Verify solutions satisfy all clauses
112/// for sol in solutions {
113///     assert!(problem.evaluate(&sol));
114/// }
115/// ```
116#[derive(Debug, Clone, Serialize, Deserialize)]
117pub struct Satisfiability {
118    /// Number of variables.
119    num_vars: usize,
120    /// Clauses in CNF.
121    clauses: Vec<CNFClause>,
122}
123
124impl Satisfiability {
125    /// Create a new SAT problem.
126    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
127        Self { num_vars, clauses }
128    }
129
130    /// Get the number of variables.
131    pub fn num_vars(&self) -> usize {
132        self.num_vars
133    }
134
135    /// Get the number of clauses.
136    pub fn num_clauses(&self) -> usize {
137        self.clauses.len()
138    }
139
140    /// Get the total number of literal occurrences across all clauses.
141    pub fn num_literals(&self) -> usize {
142        self.clauses.iter().map(|c| c.len()).sum()
143    }
144
145    /// Get the clauses.
146    pub fn clauses(&self) -> &[CNFClause] {
147        &self.clauses
148    }
149
150    /// Get a specific clause.
151    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
152        self.clauses.get(index)
153    }
154
155    /// Count satisfied clauses for an assignment.
156    pub fn count_satisfied(&self, assignment: &[bool]) -> usize {
157        self.clauses
158            .iter()
159            .filter(|c| c.is_satisfied(assignment))
160            .count()
161    }
162
163    /// Check if an assignment satisfies all clauses.
164    pub fn is_satisfying(&self, assignment: &[bool]) -> bool {
165        self.clauses.iter().all(|c| c.is_satisfied(assignment))
166    }
167
168    /// Check if a solution (config) is valid.
169    ///
170    /// For SAT, a valid solution is one that satisfies all clauses.
171    pub fn is_valid_solution(&self, config: &[usize]) -> bool {
172        self.evaluate(config).0
173    }
174}
175
176impl Problem for Satisfiability {
177    const NAME: &'static str = "Satisfiability";
178    type Value = crate::types::Or;
179
180    fn dims(&self) -> Vec<usize> {
181        vec![2; self.num_vars]
182    }
183
184    fn evaluate(&self, config: &[usize]) -> crate::types::Or {
185        crate::types::Or({
186            let assignment = super::config_to_assignment(config);
187            self.is_satisfying(&assignment)
188        })
189    }
190
191    fn variant() -> Vec<(&'static str, &'static str)> {
192        crate::variant_params![]
193    }
194}
195
196crate::declare_variants! {
197    default Satisfiability => "2^num_variables",
198}
199
200/// Check if an assignment satisfies a SAT formula.
201///
202/// # Arguments
203/// * `num_vars` - Number of variables
204/// * `clauses` - Clauses as vectors of literals (1-indexed, signed)
205/// * `assignment` - Boolean assignment (0-indexed)
206#[cfg(test)]
207pub(crate) fn is_satisfying_assignment(
208    _num_vars: usize,
209    clauses: &[Vec<i32>],
210    assignment: &[bool],
211) -> bool {
212    clauses.iter().all(|clause| {
213        clause.iter().any(|&lit| {
214            let var = lit.unsigned_abs() as usize - 1;
215            let value = assignment.get(var).copied().unwrap_or(false);
216            if lit > 0 {
217                value
218            } else {
219                !value
220            }
221        })
222    })
223}
224
225#[cfg(feature = "example-db")]
226pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
227    vec![crate::example_db::specs::ModelExampleSpec {
228        id: "satisfiability",
229        instance: Box::new(Satisfiability::new(
230            3,
231            vec![
232                CNFClause::new(vec![1, 2]),
233                CNFClause::new(vec![-1, 3]),
234                CNFClause::new(vec![-2, -3]),
235            ],
236        )),
237        optimal_config: vec![0, 1, 0],
238        optimal_value: serde_json::json!(true),
239    }]
240}
241
242#[cfg(test)]
243#[path = "../../unit_tests/models/formula/sat.rs"]
244mod tests;
problemreductions/models/formula/sat.rs

problemreductions/models/formula/
sat.rs
