problemreductions/models/formula/
maximum_2_satisfiability.rs

1//! Maximum 2-Satisfiability (MAX-2-SAT) problem implementation.
2//!
3//! MAX-2-SAT is an optimization variant of 2-SAT where each clause has exactly
4//! 2 literals, and the goal is to maximize the number of satisfied clauses.
5//! While 2-SAT (decision) is solvable in polynomial time, MAX-2-SAT is NP-hard.
6
7use crate::registry::{FieldInfo, ProblemSchemaEntry};
8use crate::traits::Problem;
9use crate::types::Max;
10use serde::{Deserialize, Serialize};
11
12use super::CNFClause;
13
14inventory::submit! {
15    ProblemSchemaEntry {
16        name: "Maximum2Satisfiability",
17        display_name: "Maximum 2-Satisfiability",
18        aliases: &["MAX2SAT"],
19        dimensions: &[],
20        module_path: module_path!(),
21        description: "Maximize the number of satisfied 2-literal clauses",
22        fields: &[
23            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
24            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Collection of 2-literal clauses" },
25        ],
26    }
27}
28
29/// Maximum 2-Satisfiability problem where each clause has exactly 2 literals.
30///
31/// Given a set of Boolean variables and a collection of clauses, each containing
32/// exactly 2 literals, find a truth assignment that maximizes the number of
33/// simultaneously satisfied clauses.
34///
35/// # Example
36///
37/// ```
38/// use problemreductions::models::formula::{Maximum2Satisfiability, CNFClause};
39/// use problemreductions::{Problem, Solver, BruteForce};
40///
41/// let problem = Maximum2Satisfiability::new(
42///     3,
43///     vec![
44///         CNFClause::new(vec![1, 2]),    // x1 OR x2
45///         CNFClause::new(vec![-1, -2]),  // NOT x1 OR NOT x2
46///         CNFClause::new(vec![1, 3]),    // x1 OR x3
47///     ],
48/// );
49///
50/// let solver = BruteForce::new();
51/// let value = solver.solve(&problem);
52/// ```
53#[derive(Debug, Clone, Serialize, Deserialize)]
54pub struct Maximum2Satisfiability {
55    /// Number of Boolean variables.
56    num_vars: usize,
57    /// Clauses in CNF, each with exactly 2 literals.
58    clauses: Vec<CNFClause>,
59}
60
61impl Maximum2Satisfiability {
62    /// Create a new MAX-2-SAT problem.
63    ///
64    /// # Panics
65    /// Panics if any clause does not have exactly 2 literals.
66    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
67        for (i, clause) in clauses.iter().enumerate() {
68            assert!(
69                clause.len() == 2,
70                "Clause {} has {} literals, expected 2",
71                i,
72                clause.len()
73            );
74        }
75        Self { num_vars, clauses }
76    }
77
78    /// Get the number of variables.
79    pub fn num_vars(&self) -> usize {
80        self.num_vars
81    }
82
83    /// Get the number of clauses.
84    pub fn num_clauses(&self) -> usize {
85        self.clauses.len()
86    }
87
88    /// Get the clauses.
89    pub fn clauses(&self) -> &[CNFClause] {
90        &self.clauses
91    }
92
93    /// Count satisfied clauses for an assignment.
94    pub fn count_satisfied(&self, assignment: &[bool]) -> usize {
95        self.clauses
96            .iter()
97            .filter(|c| c.is_satisfied(assignment))
98            .count()
99    }
100}
101
102impl Problem for Maximum2Satisfiability {
103    const NAME: &'static str = "Maximum2Satisfiability";
104    type Value = Max<usize>;
105
106    fn dims(&self) -> Vec<usize> {
107        vec![2; self.num_vars]
108    }
109
110    fn evaluate(&self, config: &[usize]) -> Max<usize> {
111        let assignment = super::config_to_assignment(config);
112        Max(Some(self.count_satisfied(&assignment)))
113    }
114
115    fn variant() -> Vec<(&'static str, &'static str)> {
116        crate::variant_params![]
117    }
118}
119
120crate::declare_variants! {
121    default Maximum2Satisfiability => "2^(0.7905 * num_variables)",
122}
123
124#[cfg(feature = "example-db")]
125pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
126    vec![crate::example_db::specs::ModelExampleSpec {
127        id: "maximum_2_satisfiability",
128        instance: Box::new(Maximum2Satisfiability::new(
129            4,
130            vec![
131                CNFClause::new(vec![1, 2]),
132                CNFClause::new(vec![1, -2]),
133                CNFClause::new(vec![-1, 3]),
134                CNFClause::new(vec![-1, -3]),
135                CNFClause::new(vec![2, 4]),
136                CNFClause::new(vec![-3, -4]),
137                CNFClause::new(vec![3, 4]),
138            ],
139        )),
140        optimal_config: vec![1, 1, 0, 1],
141        optimal_value: serde_json::json!(6),
142    }]
143}
144
145#[cfg(test)]
146#[path = "../../unit_tests/models/formula/maximum_2_satisfiability.rs"]
147mod tests;
problemreductions/models/formula/maximum_2_satisfiability.rs

problemreductions/models/formula/
maximum_2_satisfiability.rs
