problemreductions/models/formula/
one_in_three_satisfiability.rs

1//! One-in-Three Satisfiability (1-in-3 SAT) problem implementation.
2//!
3//! 1-in-3 SAT is a variant of 3-SAT where each clause must have *exactly one*
4//! true literal (rather than *at least one*). This stronger constraint makes
5//! the problem NP-complete even without negations (monotone 1-in-3 SAT).
6
7use crate::registry::{FieldInfo, ProblemSchemaEntry};
8use crate::traits::Problem;
9use serde::{Deserialize, Serialize};
10
11use super::CNFClause;
12
13inventory::submit! {
14    ProblemSchemaEntry {
15        name: "OneInThreeSatisfiability",
16        display_name: "One-in-Three Satisfiability",
17        aliases: &[],
18        dimensions: &[],
19        module_path: module_path!(),
20        description: "3-SAT variant where each clause has exactly one true literal",
21        fields: &[
22            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
23            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Clauses each with exactly 3 literals" },
24        ],
25    }
26}
27
28/// One-in-Three Satisfiability problem.
29///
30/// Given a CNF formula where each clause has exactly 3 literals, find a truth
31/// assignment such that each clause has *exactly one* true literal.
32///
33/// This is a well-known NP-complete problem introduced by Schaefer (1978).
34/// Unlike standard 3-SAT which requires at least one true literal per clause,
35/// 1-in-3 SAT requires exactly one.
36///
37/// # Example
38///
39/// ```
40/// use problemreductions::models::formula::{OneInThreeSatisfiability, CNFClause};
41/// use problemreductions::{Problem, Solver, BruteForce};
42///
43/// // (x1 OR x2 OR x3) AND (NOT x1 OR x3 OR x4) AND (x2 OR NOT x3 OR NOT x4)
44/// let problem = OneInThreeSatisfiability::new(
45///     4,
46///     vec![
47///         CNFClause::new(vec![1, 2, 3]),
48///         CNFClause::new(vec![-1, 3, 4]),
49///         CNFClause::new(vec![2, -3, -4]),
50///     ],
51/// );
52///
53/// let solver = BruteForce::new();
54/// let solution = solver.find_witness(&problem);
55/// assert!(solution.is_some());
56/// ```
57#[derive(Debug, Clone, Serialize, Deserialize)]
58pub struct OneInThreeSatisfiability {
59    /// Number of variables.
60    num_vars: usize,
61    /// Clauses in CNF, each with exactly 3 literals.
62    clauses: Vec<CNFClause>,
63}
64
65impl OneInThreeSatisfiability {
66    /// Create a new 1-in-3 SAT problem.
67    ///
68    /// # Panics
69    /// Panics if any clause does not have exactly 3 literals, or if any
70    /// literal references a variable outside the range [1, num_vars].
71    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
72        for (i, clause) in clauses.iter().enumerate() {
73            assert!(
74                clause.len() == 3,
75                "Clause {} has {} literals, expected 3",
76                i,
77                clause.len()
78            );
79            for &lit in &clause.literals {
80                let var = lit.unsigned_abs() as usize;
81                assert!(
82                    var >= 1 && var <= num_vars,
83                    "Clause {} contains literal {} referencing variable {} outside range [1, {}]",
84                    i,
85                    lit,
86                    var,
87                    num_vars
88                );
89            }
90        }
91        Self { num_vars, clauses }
92    }
93
94    /// Get the number of variables.
95    pub fn num_vars(&self) -> usize {
96        self.num_vars
97    }
98
99    /// Get the number of clauses.
100    pub fn num_clauses(&self) -> usize {
101        self.clauses.len()
102    }
103
104    /// Get the clauses.
105    pub fn clauses(&self) -> &[CNFClause] {
106        &self.clauses
107    }
108
109    /// Get a specific clause.
110    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
111        self.clauses.get(index)
112    }
113
114    /// Check if exactly one literal is true in each clause.
115    pub fn is_one_in_three_satisfying(&self, assignment: &[bool]) -> bool {
116        self.clauses.iter().all(|clause| {
117            let true_count = clause
118                .literals
119                .iter()
120                .filter(|&&lit| {
121                    let var = lit.unsigned_abs() as usize - 1; // Convert to 0-indexed
122                    let value = assignment.get(var).copied().unwrap_or(false);
123                    if lit > 0 {
124                        value
125                    } else {
126                        !value
127                    }
128                })
129                .count();
130            true_count == 1
131        })
132    }
133}
134
135impl Problem for OneInThreeSatisfiability {
136    const NAME: &'static str = "OneInThreeSatisfiability";
137    type Value = crate::types::Or;
138
139    fn dims(&self) -> Vec<usize> {
140        vec![2; self.num_vars]
141    }
142
143    fn evaluate(&self, config: &[usize]) -> crate::types::Or {
144        crate::types::Or({
145            let assignment = super::config_to_assignment(config);
146            self.is_one_in_three_satisfying(&assignment)
147        })
148    }
149
150    fn variant() -> Vec<(&'static str, &'static str)> {
151        crate::variant_params![]
152    }
153}
154
155crate::declare_variants! {
156    default OneInThreeSatisfiability => "1.307^num_variables",
157}
158
159#[cfg(feature = "example-db")]
160pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
161    vec![crate::example_db::specs::ModelExampleSpec {
162        id: "one_in_three_satisfiability",
163        instance: Box::new(OneInThreeSatisfiability::new(
164            4,
165            vec![
166                CNFClause::new(vec![1, 2, 3]),
167                CNFClause::new(vec![-1, 3, 4]),
168                CNFClause::new(vec![2, -3, -4]),
169            ],
170        )),
171        optimal_config: vec![1, 0, 0, 1],
172        optimal_value: serde_json::json!(true),
173    }]
174}
175
176#[cfg(test)]
177#[path = "../../unit_tests/models/formula/one_in_three_satisfiability.rs"]
178mod tests;
problemreductions/models/formula/one_in_three_satisfiability.rs

problemreductions/models/formula/
one_in_three_satisfiability.rs
