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        category: crate::registry::ProblemCategory::Formula,
19        module_path: module_path!(),
20        description: "Find satisfying assignment for CNF formula",
21        fields: &[
22            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
23            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Clauses in conjunctive normal form" },
24        ],
25    }
26}
27
28/// A clause in conjunctive normal form (CNF).
29///
30/// A clause is a disjunction (OR) of literals.
31/// Literals are represented as signed integers:
32/// - Positive i means variable i
33/// - Negative -i means NOT variable i
34///
35/// Variables are 1-indexed in the external representation but
36/// 0-indexed internally.
37#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
38pub struct CNFClause {
39    /// Literals in this clause (signed integers, 1-indexed).
40    pub literals: Vec<i64>,
41}
42
43impl CNFClause {
44    /// Create a new clause from literals.
45    ///
46    /// Literals are signed integers where positive means the variable
47    /// and negative means its negation. Variables are 1-indexed.
48    pub fn new(literals: Vec<i64>) -> Self {
49        Self { literals }
50    }
51
52    /// Check if the clause is satisfied by an assignment.
53    ///
54    /// # Arguments
55    /// * `assignment` - Boolean assignment, 0-indexed
56    pub fn is_satisfied(&self, assignment: &[bool]) -> bool {
57        self.literals.iter().any(|&lit| {
58            let var = usize::try_from(lit.unsigned_abs())
59                .expect("i64 literal magnitude must fit usize")
60                .checked_sub(1)
61                .expect("CNF literal 0 is invalid");
62            let value = assignment.get(var).copied().unwrap_or(false);
63            if lit > 0 {
64                value
65            } else {
66                !value
67            }
68        })
69    }
70
71    /// Get the variables involved in this clause (0-indexed).
72    pub fn variables(&self) -> Vec<usize> {
73        self.literals
74            .iter()
75            .map(|&lit| {
76                usize::try_from(lit.unsigned_abs())
77                    .expect("i64 literal magnitude must fit usize")
78                    .checked_sub(1)
79                    .expect("CNF literal 0 is invalid")
80            })
81            .collect()
82    }
83
84    /// Get the number of literals.
85    pub fn len(&self) -> usize {
86        self.literals.len()
87    }
88
89    /// Check if the clause is empty.
90    pub fn is_empty(&self) -> bool {
91        self.literals.is_empty()
92    }
93}
94
95/// Boolean Satisfiability (SAT) problem in CNF form.
96///
97/// Given a Boolean formula in conjunctive normal form (CNF),
98/// determine if there exists an assignment that satisfies all clauses.
99/// This is the decision version of the problem.
100///
101/// # Example
102///
103/// ```
104/// use problemreductions::models::formula::{Satisfiability, CNFClause};
105/// use problemreductions::{Problem, BruteForce};
106///
107/// // Formula: (x1 OR x2) AND (NOT x1 OR x3) AND (NOT x2 OR NOT x3)
108/// let problem = Satisfiability::new(
109///     3,
110///     vec![
111///         CNFClause::new(vec![1, 2]),      // x1 OR x2
112///         CNFClause::new(vec![-1, 3]),     // NOT x1 OR x3
113///         CNFClause::new(vec![-2, -3]),    // NOT x2 OR NOT x3
114///     ],
115/// );
116///
117/// let solver = BruteForce::new();
118/// let solutions = solver.find_all_witnesses(&problem).unwrap();
119///
120/// // Verify solutions satisfy all clauses
121/// for sol in solutions {
122///     assert!(problem.evaluate(&sol).unwrap());
123/// }
124/// ```
125#[derive(Debug, Clone, Serialize, Deserialize)]
126#[serde(try_from = "SatisfiabilityDef")]
127pub struct Satisfiability {
128    /// Number of variables.
129    num_vars: usize,
130    /// Clauses in CNF.
131    clauses: Vec<CNFClause>,
132}
133
134impl Satisfiability {
135    /// Create a new SAT problem.
136    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
137        Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
138    }
139
140    /// Create a new SAT problem after validating its literal encoding.
141    pub fn try_new(
142        num_vars: usize,
143        clauses: Vec<CNFClause>,
144    ) -> Result<Self, crate::registry::ConstructionError> {
145        validate_cnf_literals(num_vars, &clauses)?;
146        Ok(Self { num_vars, clauses })
147    }
148
149    /// Get the number of variables.
150    pub fn num_vars(&self) -> usize {
151        self.num_vars
152    }
153
154    /// Get the number of clauses.
155    pub fn num_clauses(&self) -> usize {
156        self.clauses.len()
157    }
158
159    /// Get the total number of literal occurrences across all clauses.
160    pub fn num_literals(&self) -> usize {
161        self.clauses.iter().map(|c| c.len()).sum()
162    }
163
164    /// Get the clauses.
165    pub fn clauses(&self) -> &[CNFClause] {
166        &self.clauses
167    }
168
169    /// Get a specific clause.
170    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
171        self.clauses.get(index)
172    }
173
174    /// Count satisfied clauses for an assignment.
175    pub fn count_satisfied(
176        &self,
177        assignment: &[bool],
178    ) -> Result<i64, crate::traits::EvaluationError> {
179        let count = self
180            .clauses
181            .iter()
182            .filter(|c| c.is_satisfied(assignment))
183            .count();
184        i64::try_from(count).map_err(|_| {
185            crate::traits::EvaluationError::IntegerOverflow(
186                "converting satisfied-clause count to i64".into(),
187            )
188        })
189    }
190
191    /// Check if an assignment satisfies all clauses.
192    pub fn is_satisfying(&self, assignment: &[bool]) -> bool {
193        self.clauses.iter().all(|c| c.is_satisfied(assignment))
194    }
195
196    /// Check if a solution (config) is valid.
197    ///
198    /// For SAT, a valid solution is one that satisfies all clauses.
199    pub fn is_valid_solution(
200        &self,
201        config: &[bool],
202    ) -> Result<bool, crate::traits::EvaluationError> {
203        if config.len() != self.num_vars {
204            return Err(crate::traits::EvaluationError::InvalidConfiguration(
205                "assignment length does not match the formula variables".into(),
206            ));
207        }
208        Ok(self.is_satisfying(config))
209    }
210}
211
212impl Problem for Satisfiability {
213    const NAME: &'static str = "Satisfiability";
214    type Solution = Vec<bool>;
215    type Value = crate::types::Or;
216
217    crate::problem_parameters![
218        ("num_clauses", num_clauses),
219        ("num_literals", num_literals),
220        ("num_vars", num_vars),
221    ];
222
223    fn evaluate(
224        &self,
225        config: &Self::Solution,
226    ) -> Result<crate::types::Or, crate::traits::EvaluationError> {
227        Ok(crate::types::Or(self.is_valid_solution(config)?))
228    }
229
230    fn variant() -> Vec<(&'static str, &'static str)> {
231        crate::variant_params![]
232    }
233}
234
235impl crate::solvers::BruteForceProblem for Satisfiability {
236    fn dimensions(&self) -> Vec<usize> {
237        vec![2; self.num_vars]
238    }
239}
240
241crate::declare_variants! {
242    default Satisfiability => "2^num_vars",
243}
244
245crate::register_brute_force! {
246    Satisfiability decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
247}
248
249#[derive(Deserialize)]
250struct SatisfiabilityDef {
251    num_vars: usize,
252    clauses: Vec<CNFClause>,
253}
254
255impl TryFrom<SatisfiabilityDef> for Satisfiability {
256    type Error = crate::registry::ConstructionError;
257
258    fn try_from(value: SatisfiabilityDef) -> Result<Self, Self::Error> {
259        Self::try_new(value.num_vars, value.clauses)
260    }
261}
262
263pub(super) fn validate_cnf_literals(
264    num_vars: usize,
265    clauses: &[CNFClause],
266) -> Result<(), crate::registry::ConstructionError> {
267    if num_vars > i64::MAX as usize {
268        return Err(format!(
269            "num_vars {num_vars} exceeds the SAT literal limit {}",
270            i64::MAX
271        )
272        .into());
273    }
274
275    for (clause_index, clause) in clauses.iter().enumerate() {
276        for &literal in &clause.literals {
277            if literal == 0 || literal == i64::MIN {
278                return Err(format!(
279                    "clause {clause_index} contains invalid literal {literal}; allowed variable numbers are 1..={num_vars} with either sign"
280                ).into());
281            }
282            let magnitude = usize::try_from(literal.unsigned_abs()).map_err(|_| {
283                format!("clause {clause_index} literal {literal} magnitude does not fit usize")
284            })?;
285            if magnitude > num_vars {
286                return Err(format!(
287                    "clause {clause_index} contains invalid literal {literal}; allowed variable numbers are 1..={num_vars} with either sign"
288                ).into());
289            }
290        }
291    }
292
293    Ok(())
294}
295
296/// Check if an assignment satisfies a SAT formula.
297///
298/// # Arguments
299/// * `num_vars` - Number of variables
300/// * `clauses` - Clauses as vectors of literals (1-indexed, signed)
301/// * `assignment` - Boolean assignment (0-indexed)
302#[cfg(test)]
303pub(crate) fn is_satisfying_assignment(
304    _num_vars: usize,
305    clauses: &[Vec<i64>],
306    assignment: &[bool],
307) -> bool {
308    clauses.iter().all(|clause| {
309        clause.iter().any(|&lit| {
310            let var = lit.unsigned_abs() as usize - 1;
311            let value = assignment.get(var).copied().unwrap_or(false);
312            if lit > 0 {
313                value
314            } else {
315                !value
316            }
317        })
318    })
319}
320
321#[cfg(feature = "example-db")]
322pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
323    vec![crate::example_db::specs::ModelExampleSpec {
324        id: "satisfiability",
325        instance: Box::new(Satisfiability::new(
326            3,
327            vec![
328                CNFClause::new(vec![1, 2]),
329                CNFClause::new(vec![-1, 3]),
330                CNFClause::new(vec![-2, -3]),
331            ],
332        )),
333        optimal_config: serde_json::json!(vec![false, true, false]),
334        optimal_value: serde_json::json!(true),
335    }]
336}
337
338#[cfg(test)]
339#[path = "../../unit_tests/models/formula/sat.rs"]
340mod tests;
problemreductions/models/formula/sat.rs

problemreductions/models/formula/
sat.rs
