problemreductions/models/formula/
planar_3_satisfiability.rs

1//! Planar 3-Satisfiability (Planar 3-SAT) problem implementation.
2//!
3//! Planar 3-SAT is a restricted variant of 3-SAT where the variable-clause
4//! incidence graph is planar. Each clause has exactly 3 literals. This
5//! restriction preserves NP-completeness while enabling reductions to
6//! geometric and planar problems.
7
8use crate::registry::{FieldInfo, ProblemSchemaEntry};
9use crate::traits::Problem;
10use serde::{Deserialize, Serialize};
11
12use super::{sat::validate_cnf_literals, CNFClause};
13
14inventory::submit! {
15    ProblemSchemaEntry {
16        name: "Planar3Satisfiability",
17        display_name: "Planar 3-Satisfiability",
18        aliases: &[],
19        dimensions: &[],
20        category: crate::registry::ProblemCategory::Formula,
21        module_path: module_path!(),
22        description: "3-SAT with planar variable-clause incidence graph",
23        fields: &[
24            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
25            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Clauses each with exactly 3 literals" },
26        ],
27    }
28}
29
30/// Planar 3-Satisfiability problem.
31///
32/// Given a 3-CNF formula where each clause has exactly 3 literals and the
33/// variable-clause incidence graph is planar, find a satisfying assignment.
34///
35/// The incidence graph H(F) is a bipartite graph with variable nodes and
36/// clause nodes, where an edge connects variable v to clause C if v appears
37/// (positively or negatively) in C. The formula is a valid Planar 3-SAT
38/// instance if H(F) is planar.
39///
40/// **Note:** Planarity of the incidence graph is NOT validated at construction
41/// time. Only the clause width (exactly 3 literals) and variable index range
42/// are validated. This is analogous to how `PlanarGraph` does not explicitly
43/// validate planarity in this codebase.
44///
45/// # Example
46///
47/// ```
48/// use problemreductions::models::formula::{Planar3Satisfiability, CNFClause};
49/// use problemreductions::{Problem, BruteForce};
50///
51/// // Formula: (x1 OR x2 OR x3) AND (NOT x1 OR x2 OR x4)
52/// //       AND (x1 OR NOT x3 OR x4) AND (NOT x2 OR x3 OR NOT x4)
53/// let problem = Planar3Satisfiability::new(
54///     4,
55///     vec![
56///         CNFClause::new(vec![1, 2, 3]),
57///         CNFClause::new(vec![-1, 2, 4]),
58///         CNFClause::new(vec![1, -3, 4]),
59///         CNFClause::new(vec![-2, 3, -4]),
60///     ],
61/// );
62///
63/// let solver = BruteForce::new();
64/// let solution = solver.solve(&problem).unwrap();
65/// assert!(solution.is_some());
66/// ```
67#[derive(Debug, Clone, Serialize, Deserialize)]
68#[serde(try_from = "Planar3SatisfiabilityDef")]
69pub struct Planar3Satisfiability {
70    /// Number of variables.
71    num_vars: usize,
72    /// Clauses in CNF, each with exactly 3 literals.
73    clauses: Vec<CNFClause>,
74}
75
76impl Planar3Satisfiability {
77    /// Create a new Planar 3-SAT problem.
78    ///
79    /// # Panics
80    /// Panics if any clause does not have exactly 3 literals, or if any
81    /// literal references a variable outside the range [1, num_vars].
82    ///
83    /// **Note:** Planarity of the incidence graph is not checked.
84    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
85        Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
86    }
87
88    /// Create a new Planar 3-SAT problem after validating its clauses.
89    pub fn try_new(
90        num_vars: usize,
91        clauses: Vec<CNFClause>,
92    ) -> Result<Self, crate::registry::ConstructionError> {
93        validate_cnf_literals(num_vars, &clauses)?;
94        for (i, clause) in clauses.iter().enumerate() {
95            if clause.len() != 3 {
96                return Err(format!("Clause {i} has {} literals, expected 3", clause.len()).into());
97            }
98        }
99        Ok(Self { num_vars, clauses })
100    }
101
102    /// Get the number of variables.
103    pub fn num_vars(&self) -> usize {
104        self.num_vars
105    }
106
107    /// Get the number of clauses.
108    pub fn num_clauses(&self) -> usize {
109        self.clauses.len()
110    }
111
112    /// Get the clauses.
113    pub fn clauses(&self) -> &[CNFClause] {
114        &self.clauses
115    }
116
117    /// Get a specific clause.
118    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
119        self.clauses.get(index)
120    }
121
122    /// Check if an assignment satisfies all clauses.
123    pub fn is_satisfying(&self, assignment: &[bool]) -> bool {
124        self.clauses.iter().all(|c| c.is_satisfied(assignment))
125    }
126}
127
128impl Problem for Planar3Satisfiability {
129    const NAME: &'static str = "Planar3Satisfiability";
130    type Solution = Vec<bool>;
131    type Value = crate::types::Or;
132
133    crate::problem_parameters![("num_vars", num_vars), ("num_clauses", num_clauses),];
134
135    fn evaluate(
136        &self,
137        config: &Self::Solution,
138    ) -> Result<crate::types::Or, crate::traits::EvaluationError> {
139        if config.len() != self.num_vars {
140            return Err(crate::traits::EvaluationError::InvalidConfiguration(
141                "assignment length does not match the formula variables".into(),
142            ));
143        }
144        Ok(crate::types::Or(self.is_satisfying(config)))
145    }
146
147    fn variant() -> Vec<(&'static str, &'static str)> {
148        crate::variant_params![]
149    }
150}
151
152impl crate::solvers::BruteForceProblem for Planar3Satisfiability {
153    fn dimensions(&self) -> Vec<usize> {
154        vec![2; self.num_vars]
155    }
156}
157
158crate::declare_variants! {
159    default Planar3Satisfiability => "1.307^num_vars",
160}
161
162crate::register_brute_force! {
163    Planar3Satisfiability decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
164}
165
166#[derive(Deserialize)]
167struct Planar3SatisfiabilityDef {
168    num_vars: usize,
169    clauses: Vec<CNFClause>,
170}
171
172impl TryFrom<Planar3SatisfiabilityDef> for Planar3Satisfiability {
173    type Error = crate::registry::ConstructionError;
174
175    fn try_from(value: Planar3SatisfiabilityDef) -> Result<Self, Self::Error> {
176        Self::try_new(value.num_vars, value.clauses)
177    }
178}
179
180#[cfg(feature = "example-db")]
181pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
182    vec![crate::example_db::specs::ModelExampleSpec {
183        id: "planar_3_satisfiability",
184        instance: Box::new(Planar3Satisfiability::new(
185            4,
186            vec![
187                CNFClause::new(vec![1, 2, 3]),
188                CNFClause::new(vec![-1, 2, 4]),
189                CNFClause::new(vec![1, -3, 4]),
190                CNFClause::new(vec![-2, 3, -4]),
191            ],
192        )),
193        optimal_config: serde_json::json!(vec![true, true, true, false]),
194        optimal_value: serde_json::json!(true),
195    }]
196}
197
198#[cfg(test)]
199#[path = "../../unit_tests/models/formula/planar_3_satisfiability.rs"]
200mod tests;
problemreductions/models/formula/planar_3_satisfiability.rs

problemreductions/models/formula/
planar_3_satisfiability.rs
