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::{sat::validate_cnf_literals, CNFClause};
13
14inventory::submit! {
15    ProblemSchemaEntry {
16        name: "Maximum2Satisfiability",
17        display_name: "Maximum 2-Satisfiability",
18        aliases: &["MAX2SAT"],
19        dimensions: &[],
20        category: crate::registry::ProblemCategory::Formula,
21        module_path: module_path!(),
22        description: "Maximize the number of satisfied 2-literal clauses",
23        fields: &[
24            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
25            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Collection of 2-literal clauses" },
26        ],
27    }
28}
29
30/// Maximum 2-Satisfiability problem where each clause has exactly 2 literals.
31///
32/// Given a set of Boolean variables and a collection of clauses, each containing
33/// exactly 2 literals, find a truth assignment that maximizes the number of
34/// simultaneously satisfied clauses.
35///
36/// # Example
37///
38/// ```
39/// use problemreductions::models::formula::{Maximum2Satisfiability, CNFClause};
40/// use problemreductions::{Problem, BruteForce};
41///
42/// let problem = Maximum2Satisfiability::new(
43///     3,
44///     vec![
45///         CNFClause::new(vec![1, 2]),    // x1 OR x2
46///         CNFClause::new(vec![-1, -2]),  // NOT x1 OR NOT x2
47///         CNFClause::new(vec![1, 3]),    // x1 OR x3
48///     ],
49/// );
50///
51/// let solver = BruteForce::new();
52/// let value = solver.solve(&problem).unwrap();
53/// ```
54#[derive(Debug, Clone, Serialize, Deserialize)]
55#[serde(try_from = "Maximum2SatisfiabilityDef")]
56pub struct Maximum2Satisfiability {
57    /// Number of Boolean variables.
58    num_vars: usize,
59    /// Clauses in CNF, each with exactly 2 literals.
60    clauses: Vec<CNFClause>,
61}
62
63impl Maximum2Satisfiability {
64    /// Create a new MAX-2-SAT problem.
65    ///
66    /// # Panics
67    /// Panics if any clause does not have exactly 2 literals.
68    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
69        Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
70    }
71
72    /// Create a new MAX-2-SAT problem after validating its clauses.
73    pub fn try_new(
74        num_vars: usize,
75        clauses: Vec<CNFClause>,
76    ) -> Result<Self, crate::registry::ConstructionError> {
77        validate_cnf_literals(num_vars, &clauses)?;
78        for (i, clause) in clauses.iter().enumerate() {
79            if clause.len() != 2 {
80                return Err(format!("Clause {i} has {} literals, expected 2", clause.len()).into());
81            }
82        }
83        Ok(Self { num_vars, clauses })
84    }
85
86    /// Get the number of variables.
87    pub fn num_vars(&self) -> usize {
88        self.num_vars
89    }
90
91    /// Get the number of clauses.
92    pub fn num_clauses(&self) -> usize {
93        self.clauses.len()
94    }
95
96    /// Get the clauses.
97    pub fn clauses(&self) -> &[CNFClause] {
98        &self.clauses
99    }
100
101    /// Count satisfied clauses for an assignment.
102    pub fn count_satisfied(
103        &self,
104        assignment: &[bool],
105    ) -> Result<i64, crate::traits::EvaluationError> {
106        let count = self
107            .clauses
108            .iter()
109            .filter(|c| c.is_satisfied(assignment))
110            .count();
111        i64::try_from(count).map_err(|_| {
112            crate::traits::EvaluationError::IntegerOverflow(
113                "converting satisfied-clause count to i64".into(),
114            )
115        })
116    }
117}
118
119impl Problem for Maximum2Satisfiability {
120    const NAME: &'static str = "Maximum2Satisfiability";
121    type Solution = Vec<bool>;
122    type Value = Max<i64>;
123
124    crate::problem_parameters![("num_clauses", num_clauses), ("num_vars", num_vars),];
125
126    fn evaluate(
127        &self,
128        config: &Self::Solution,
129    ) -> Result<Max<i64>, crate::traits::EvaluationError> {
130        if config.len() != self.num_vars {
131            return Err(crate::traits::EvaluationError::InvalidConfiguration(
132                "assignment length does not match the formula variables".into(),
133            ));
134        }
135        Ok(Max(Some(self.count_satisfied(config)?)))
136    }
137
138    fn variant() -> Vec<(&'static str, &'static str)> {
139        crate::variant_params![]
140    }
141}
142
143impl crate::solvers::BruteForceProblem for Maximum2Satisfiability {
144    fn dimensions(&self) -> Vec<usize> {
145        vec![2; self.num_vars]
146    }
147}
148
149crate::declare_variants! {
150    default Maximum2Satisfiability => "2^(0.7905 * num_vars)",
151}
152
153crate::register_brute_force! {
154    Maximum2Satisfiability decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
155}
156
157#[derive(Deserialize)]
158struct Maximum2SatisfiabilityDef {
159    num_vars: usize,
160    clauses: Vec<CNFClause>,
161}
162
163impl TryFrom<Maximum2SatisfiabilityDef> for Maximum2Satisfiability {
164    type Error = crate::registry::ConstructionError;
165
166    fn try_from(value: Maximum2SatisfiabilityDef) -> Result<Self, Self::Error> {
167        Self::try_new(value.num_vars, value.clauses)
168    }
169}
170
171#[cfg(feature = "example-db")]
172pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
173    vec![crate::example_db::specs::ModelExampleSpec {
174        id: "maximum_2_satisfiability",
175        instance: Box::new(Maximum2Satisfiability::new(
176            4,
177            vec![
178                CNFClause::new(vec![1, 2]),
179                CNFClause::new(vec![1, -2]),
180                CNFClause::new(vec![-1, 3]),
181                CNFClause::new(vec![-1, -3]),
182                CNFClause::new(vec![2, 4]),
183                CNFClause::new(vec![-3, -4]),
184                CNFClause::new(vec![3, 4]),
185            ],
186        )),
187        optimal_config: serde_json::json!(vec![true, true, false, true]),
188        optimal_value: serde_json::json!(6),
189    }]
190}
191
192#[cfg(test)]
193#[path = "../../unit_tests/models/formula/maximum_2_satisfiability.rs"]
194mod tests;
195
196crate::decision_problem_meta!(Maximum2Satisfiability, "DecisionMaximum2Satisfiability");
197crate::register_decision_variant!(
198    Maximum2Satisfiability, "DecisionMaximum2Satisfiability", "2^(0.7905 * num_vars)", &[],
199    "Does a feasible solution have objective value >= the bound?",
200    category: crate::registry::ProblemCategory::Formula,
201    dims: [],
202    fields: [
203        crate::registry::FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
204        crate::registry::FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Collection of 2-literal clauses" },
205        crate::registry::FieldInfo { name: "bound", type_name: "i64", description: "Accept objective values >= this bound" },
206    ],
207    decode: |_, indices: Vec<usize>| crate::config::config_to_bits(&indices)
208);
209
210#[cfg(feature = "example-db")]
211pub(crate) fn decision_canonical_rule_example_specs(
212) -> Vec<crate::example_db::specs::RuleExampleSpec> {
213    vec![crate::example_db::specs::RuleExampleSpec {
214        id: "decision_maximum_2_satisfiability_to_maximum_2_satisfiability",
215        build: || {
216            let source = crate::models::decision::Decision::new(
217                Maximum2Satisfiability::new(
218                    4,
219                    vec![
220                        CNFClause::new(vec![1, 2]),
221                        CNFClause::new(vec![1, -2]),
222                        CNFClause::new(vec![-1, 3]),
223                        CNFClause::new(vec![-1, -3]),
224                        CNFClause::new(vec![2, 4]),
225                        CNFClause::new(vec![-3, -4]),
226                        CNFClause::new(vec![3, 4]),
227                    ],
228                ),
229                6,
230            );
231            let witness = serde_json::json!(vec![true, true, false, true]);
232            crate::example_db::specs::rule_example_with_witness::<_, Maximum2Satisfiability>(
233                source,
234                crate::export::SolutionPair {
235                    source_config: witness.clone(),
236                    target_config: witness,
237                },
238            )
239        },
240    }]
241}
problemreductions/models/formula/maximum_2_satisfiability.rs

problemreductions/models/formula/
maximum_2_satisfiability.rs
