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::CNFClause;
13
14inventory::submit! {
15    ProblemSchemaEntry {
16        name: "Planar3Satisfiability",
17        display_name: "Planar 3-Satisfiability",
18        aliases: &[],
19        dimensions: &[],
20        module_path: module_path!(),
21        description: "3-SAT with planar variable-clause incidence graph",
22        fields: &[
23            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
24            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Clauses each with exactly 3 literals" },
25        ],
26    }
27}
28
29/// Planar 3-Satisfiability problem.
30///
31/// Given a 3-CNF formula where each clause has exactly 3 literals and the
32/// variable-clause incidence graph is planar, find a satisfying assignment.
33///
34/// The incidence graph H(F) is a bipartite graph with variable nodes and
35/// clause nodes, where an edge connects variable v to clause C if v appears
36/// (positively or negatively) in C. The formula is a valid Planar 3-SAT
37/// instance if H(F) is planar.
38///
39/// **Note:** Planarity of the incidence graph is NOT validated at construction
40/// time. Only the clause width (exactly 3 literals) and variable index range
41/// are validated. This is analogous to how `PlanarGraph` does not explicitly
42/// validate planarity in this codebase.
43///
44/// # Example
45///
46/// ```
47/// use problemreductions::models::formula::{Planar3Satisfiability, CNFClause};
48/// use problemreductions::{Problem, Solver, BruteForce};
49///
50/// // Formula: (x1 OR x2 OR x3) AND (NOT x1 OR x2 OR x4)
51/// //       AND (x1 OR NOT x3 OR x4) AND (NOT x2 OR x3 OR NOT x4)
52/// let problem = Planar3Satisfiability::new(
53///     4,
54///     vec![
55///         CNFClause::new(vec![1, 2, 3]),
56///         CNFClause::new(vec![-1, 2, 4]),
57///         CNFClause::new(vec![1, -3, 4]),
58///         CNFClause::new(vec![-2, 3, -4]),
59///     ],
60/// );
61///
62/// let solver = BruteForce::new();
63/// let solution = solver.find_witness(&problem);
64/// assert!(solution.is_some());
65/// ```
66#[derive(Debug, Clone, Serialize, Deserialize)]
67pub struct Planar3Satisfiability {
68    /// Number of variables.
69    num_vars: usize,
70    /// Clauses in CNF, each with exactly 3 literals.
71    clauses: Vec<CNFClause>,
72}
73
74impl Planar3Satisfiability {
75    /// Create a new Planar 3-SAT problem.
76    ///
77    /// # Panics
78    /// Panics if any clause does not have exactly 3 literals, or if any
79    /// literal references a variable outside the range [1, num_vars].
80    ///
81    /// **Note:** Planarity of the incidence graph is not checked.
82    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
83        for (i, clause) in clauses.iter().enumerate() {
84            assert!(
85                clause.len() == 3,
86                "Clause {} has {} literals, expected 3",
87                i,
88                clause.len()
89            );
90            for &lit in &clause.literals {
91                let var = lit.unsigned_abs() as usize;
92                assert!(
93                    var >= 1 && var <= num_vars,
94                    "Clause {} contains literal {} referencing variable {} outside range [1, {}]",
95                    i,
96                    lit,
97                    var,
98                    num_vars
99                );
100            }
101        }
102        Self { num_vars, clauses }
103    }
104
105    /// Get the number of variables.
106    pub fn num_vars(&self) -> usize {
107        self.num_vars
108    }
109
110    /// Get the number of clauses.
111    pub fn num_clauses(&self) -> usize {
112        self.clauses.len()
113    }
114
115    /// Get the clauses.
116    pub fn clauses(&self) -> &[CNFClause] {
117        &self.clauses
118    }
119
120    /// Get a specific clause.
121    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
122        self.clauses.get(index)
123    }
124
125    /// Check if an assignment satisfies all clauses.
126    pub fn is_satisfying(&self, assignment: &[bool]) -> bool {
127        self.clauses.iter().all(|c| c.is_satisfied(assignment))
128    }
129}
130
131impl Problem for Planar3Satisfiability {
132    const NAME: &'static str = "Planar3Satisfiability";
133    type Value = crate::types::Or;
134
135    fn dims(&self) -> Vec<usize> {
136        vec![2; self.num_vars]
137    }
138
139    fn evaluate(&self, config: &[usize]) -> crate::types::Or {
140        crate::types::Or({
141            let assignment = super::config_to_assignment(config);
142            self.is_satisfying(&assignment)
143        })
144    }
145
146    fn variant() -> Vec<(&'static str, &'static str)> {
147        crate::variant_params![]
148    }
149}
150
151crate::declare_variants! {
152    default Planar3Satisfiability => "1.307^num_variables",
153}
154
155#[cfg(feature = "example-db")]
156pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
157    vec![crate::example_db::specs::ModelExampleSpec {
158        id: "planar_3_satisfiability",
159        instance: Box::new(Planar3Satisfiability::new(
160            4,
161            vec![
162                CNFClause::new(vec![1, 2, 3]),
163                CNFClause::new(vec![-1, 2, 4]),
164                CNFClause::new(vec![1, -3, 4]),
165                CNFClause::new(vec![-2, 3, -4]),
166            ],
167        )),
168        optimal_config: vec![1, 1, 1, 0],
169        optimal_value: serde_json::json!(true),
170    }]
171}
172
173#[cfg(test)]
174#[path = "../../unit_tests/models/formula/planar_3_satisfiability.rs"]
175mod tests;
problemreductions/models/formula/planar_3_satisfiability.rs

problemreductions/models/formula/
planar_3_satisfiability.rs
