Struct Planar3Satisfiability 

pub struct Planar3Satisfiability { /* private fields */ }

Planar 3-Satisfiability problem.

Given a 3-CNF formula where each clause has exactly 3 literals and the variable-clause incidence graph is planar, find a satisfying assignment.

The incidence graph H(F) is a bipartite graph with variable nodes and clause nodes, where an edge connects variable v to clause C if v appears (positively or negatively) in C. The formula is a valid Planar 3-SAT instance if H(F) is planar.

Note: Planarity of the incidence graph is NOT validated at construction time. Only the clause width (exactly 3 literals) and variable index range are validated. This is analogous to how PlanarGraph does not explicitly validate planarity in this codebase.

Example

use problemreductions::models::formula::{Planar3Satisfiability, CNFClause};
use problemreductions::{Problem, Solver, BruteForce};

// Formula: (x1 OR x2 OR x3) AND (NOT x1 OR x2 OR x4)
//       AND (x1 OR NOT x3 OR x4) AND (NOT x2 OR x3 OR NOT x4)
let problem = Planar3Satisfiability::new(
    4,
    vec![
        CNFClause::new(vec![1, 2, 3]),
        CNFClause::new(vec![-1, 2, 4]),
        CNFClause::new(vec![1, -3, 4]),
        CNFClause::new(vec![-2, 3, -4]),
    ],
);

let solver = BruteForce::new();
let solution = solver.find_witness(&problem);
assert!(solution.is_some());

Implementations

impl Planar3Satisfiability

pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self

Create a new Planar 3-SAT problem.

Panics

Panics if any clause does not have exactly 3 literals, or if any literal references a variable outside the range [1, num_vars].

Note: Planarity of the incidence graph is not checked.

pub fn num_vars(&self) -> usize

Get the number of variables.

pub fn num_clauses(&self) -> usize

Get the number of clauses.

pub fn clauses(&self) -> &[CNFClause]

Get the clauses.

pub fn get_clause(&self, index: usize) -> Option<&CNFClause>

Get a specific clause.

pub fn is_satisfying(&self, assignment: &[bool]) -> bool

Check if an assignment satisfies all clauses.

Trait Implementations

impl Clone for Planar3Satisfiability

fn clone(&self) -> Planar3Satisfiability

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Planar3Satisfiability

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Planar3Satisfiability

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Problem for Planar3Satisfiability

const NAME: &'static str = "Planar3Satisfiability"

Base name of this problem type (e.g., “MaximumIndependentSet”).

type Value = Or

The evaluation value type.

fn dims(&self) -> Vec<usize>

Configuration space dimensions. Each entry is the cardinality of that variable.

fn evaluate(&self, config: &[usize]) -> Or

Evaluate the problem on a configuration.

fn variant() -> Vec<(&'static str, &'static str)>

Returns variant attributes derived from type parameters.

fn num_variables(&self) -> usize

Number of variables (derived from dims).

fn problem_type() -> ProblemType

Look up this problem’s catalog entry.

impl Serialize for Planar3Satisfiability

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl DeclaredVariant for Planar3Satisfiability