Struct OneInThreeSatisfiability 

pub struct OneInThreeSatisfiability { /* private fields */ }

One-in-Three Satisfiability problem.

Given a CNF formula where each clause has exactly 3 literals, find a truth assignment such that each clause has exactly one true literal.

This is a well-known NP-complete problem introduced by Schaefer (1978). Unlike standard 3-SAT which requires at least one true literal per clause, 1-in-3 SAT requires exactly one.

Example

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

// (x1 OR x2 OR x3) AND (NOT x1 OR x3 OR x4) AND (x2 OR NOT x3 OR NOT x4)
let problem = OneInThreeSatisfiability::new(
    4,
    vec![
        CNFClause::new(vec![1, 2, 3]),
        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 OneInThreeSatisfiability

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

Create a new 1-in-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].

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_one_in_three_satisfying(&self, assignment: &[bool]) -> bool

Check if exactly one literal is true in each clause.

Trait Implementations

impl Clone for OneInThreeSatisfiability

fn clone(&self) -> OneInThreeSatisfiability

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for OneInThreeSatisfiability

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for OneInThreeSatisfiability

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Problem for OneInThreeSatisfiability

const NAME: &'static str = "OneInThreeSatisfiability"

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 ReduceTo<OneInThreeSatisfiability> for KSatisfiability<K3>

type Result = Reduction3SATToOneInThreeSAT

The reduction result type.

fn reduce_to(&self) -> Self::Result

Reduce this problem to the target problem type.

impl Serialize for OneInThreeSatisfiability

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 OneInThreeSatisfiability