problemreductions/models/formula/
ksat.rs

1//! K-Satisfiability (K-SAT) problem implementation.
2//!
3//! K-SAT is a special case of SAT where each clause has exactly K literals.
4//! Common variants include 3-SAT (K=3) and 2-SAT (K=2). This is the decision
5//! version - for the optimization variant (MAX-K-SAT), see the separate
6//! MaxKSatisfiability type (if available).
7
8use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension};
9use crate::traits::Problem;
10use crate::variant::{KValue, K2, K3, KN};
11use serde::{Deserialize, Serialize};
12
13use super::CNFClause;
14
15pub(crate) fn first_n_odd_primes(count: usize) -> Vec<u64> {
16    let mut primes = Vec::with_capacity(count);
17    let mut candidate = 3u64;
18
19    while primes.len() < count {
20        if is_prime(candidate) {
21            primes.push(candidate);
22        }
23        candidate += 2;
24    }
25
26    primes
27}
28
29fn is_prime(candidate: u64) -> bool {
30    if candidate < 2 {
31        return false;
32    }
33    if candidate == 2 {
34        return true;
35    }
36    if candidate.is_multiple_of(2) {
37        return false;
38    }
39
40    let mut divisor = 3u64;
41    while divisor * divisor <= candidate {
42        if candidate.is_multiple_of(divisor) {
43            return false;
44        }
45        divisor += 2;
46    }
47
48    true
49}
50
51inventory::submit! {
52    ProblemSchemaEntry {
53        name: "KSatisfiability",
54        display_name: "K-Satisfiability",
55        aliases: &["KSAT"],
56        dimensions: &[VariantDimension::new("k", "KN", &["KN", "K2", "K3"])],
57        module_path: module_path!(),
58        description: "SAT with exactly k literals per clause",
59        fields: &[
60            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
61            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Clauses each with exactly K literals" },
62        ],
63    }
64}
65
66/// K-Satisfiability problem where each clause has exactly K literals.
67///
68/// This is a restricted form of SAT where every clause must contain
69/// exactly K literals. The most famous variant is 3-SAT (K=3), which
70/// is NP-complete, while 2-SAT (K=2) is solvable in polynomial time.
71/// This is the decision version of the problem.
72///
73/// # Type Parameters
74/// * `K` - A type implementing `KValue` that specifies the number of literals per clause
75///
76/// # Example
77///
78/// ```
79/// use problemreductions::models::formula::{KSatisfiability, CNFClause};
80/// use problemreductions::variant::K3;
81/// use problemreductions::{Problem, Solver, BruteForce};
82///
83/// // 3-SAT formula: (x1 OR x2 OR x3) AND (NOT x1 OR x2 OR NOT x3)
84/// let problem = KSatisfiability::<K3>::new(
85///     3,
86///     vec![
87///         CNFClause::new(vec![1, 2, 3]),       // x1 OR x2 OR x3
88///         CNFClause::new(vec![-1, 2, -3]),     // NOT x1 OR x2 OR NOT x3
89///     ],
90/// );
91///
92/// let solver = BruteForce::new();
93/// let solutions = solver.find_all_witnesses(&problem);
94/// assert!(!solutions.is_empty());
95/// ```
96#[derive(Debug, Clone, Serialize, Deserialize)]
97#[serde(bound(deserialize = ""))]
98pub struct KSatisfiability<K: KValue> {
99    /// Number of variables.
100    num_vars: usize,
101    /// Clauses in CNF, each with exactly K literals.
102    clauses: Vec<CNFClause>,
103    #[serde(skip)]
104    _phantom: std::marker::PhantomData<K>,
105}
106
107impl<K: KValue> KSatisfiability<K> {
108    /// Create a new K-SAT problem.
109    ///
110    /// # Panics
111    /// Panics if any clause does not have exactly K literals (when K is a
112    /// concrete value like K2, K3). When K is KN (arbitrary), no clause-length
113    /// validation is performed.
114    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
115        if let Some(k) = K::K {
116            for (i, clause) in clauses.iter().enumerate() {
117                assert!(
118                    clause.len() == k,
119                    "Clause {} has {} literals, expected {}",
120                    i,
121                    clause.len(),
122                    k
123                );
124            }
125        }
126        Self {
127            num_vars,
128            clauses,
129            _phantom: std::marker::PhantomData,
130        }
131    }
132
133    /// Create a new K-SAT problem allowing clauses with fewer than K literals.
134    ///
135    /// This is useful when the reduction algorithm produces clauses with
136    /// fewer literals (e.g., when allow_less is true in the Julia implementation).
137    ///
138    /// # Panics
139    /// Panics if any clause has more than K literals (when K is a concrete
140    /// value like K2, K3). When K is KN (arbitrary), no clause-length
141    /// validation is performed.
142    pub fn new_allow_less(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
143        if let Some(k) = K::K {
144            for (i, clause) in clauses.iter().enumerate() {
145                assert!(
146                    clause.len() <= k,
147                    "Clause {} has {} literals, expected at most {}",
148                    i,
149                    clause.len(),
150                    k
151                );
152            }
153        }
154        Self {
155            num_vars,
156            clauses,
157            _phantom: std::marker::PhantomData,
158        }
159    }
160
161    /// Get the number of variables.
162    pub fn num_vars(&self) -> usize {
163        self.num_vars
164    }
165
166    /// Get the number of clauses.
167    pub fn num_clauses(&self) -> usize {
168        self.clauses.len()
169    }
170
171    /// Get the clauses.
172    pub fn clauses(&self) -> &[CNFClause] {
173        &self.clauses
174    }
175
176    /// Get a specific clause.
177    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
178        self.clauses.get(index)
179    }
180
181    /// Get the total number of literals across all clauses.
182    pub fn num_literals(&self) -> usize {
183        self.clauses().iter().map(|c| c.len()).sum()
184    }
185
186    /// Padding term used by Sethi's Register Sufficiency reduction.
187    pub fn register_sufficiency_padding(&self) -> usize {
188        (2 * self.num_vars).saturating_sub(self.num_clauses())
189    }
190
191    pub fn simultaneous_incongruences_num_incongruences(&self) -> usize {
192        first_n_odd_primes(self.num_vars)
193            .into_iter()
194            .map(|prime| usize::try_from(prime - 2).expect("prime fits in usize"))
195            .sum::<usize>()
196            + self.num_clauses()
197    }
198
199    pub fn simultaneous_incongruences_bound(&self) -> usize {
200        first_n_odd_primes(self.num_vars)
201            .into_iter()
202            .try_fold(1usize, |product, prime| {
203                product.checked_mul(usize::try_from(prime).expect("prime fits in usize"))
204            })
205            .expect("simultaneous incongruences bound must fit in usize")
206    }
207
208    /// Count satisfied clauses for an assignment.
209    pub fn count_satisfied(&self, assignment: &[bool]) -> usize {
210        self.clauses
211            .iter()
212            .filter(|c| c.is_satisfied(assignment))
213            .count()
214    }
215
216    /// Check if an assignment satisfies all clauses.
217    pub fn is_satisfying(&self, assignment: &[bool]) -> bool {
218        self.clauses.iter().all(|c| c.is_satisfied(assignment))
219    }
220}
221
222impl<K: KValue> Problem for KSatisfiability<K> {
223    const NAME: &'static str = "KSatisfiability";
224    type Value = crate::types::Or;
225
226    fn dims(&self) -> Vec<usize> {
227        vec![2; self.num_vars]
228    }
229
230    fn evaluate(&self, config: &[usize]) -> crate::types::Or {
231        crate::types::Or({
232            let assignment = super::config_to_assignment(config);
233            self.is_satisfying(&assignment)
234        })
235    }
236
237    fn variant() -> Vec<(&'static str, &'static str)> {
238        crate::variant_params![K]
239    }
240}
241
242crate::declare_variants! {
243    default KSatisfiability<KN> => "2^num_variables",
244    KSatisfiability<K2> => "num_variables + num_clauses" aliases ["2SAT"],
245    KSatisfiability<K3> => "1.307^num_variables" aliases ["3SAT"],
246}
247
248#[cfg(feature = "example-db")]
249pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
250    use super::CNFClause;
251    vec![crate::example_db::specs::ModelExampleSpec {
252        id: "ksatisfiability_k3",
253        instance: Box::new(KSatisfiability::<K3>::new(
254            3,
255            vec![
256                CNFClause::new(vec![1, 2, 3]),
257                CNFClause::new(vec![-1, -2, 3]),
258                CNFClause::new(vec![1, -2, -3]),
259            ],
260        )),
261        optimal_config: vec![0, 0, 1],
262        optimal_value: serde_json::json!(true),
263    }]
264}
265
266#[cfg(test)]
267#[path = "../../unit_tests/models/formula/ksat.rs"]
268mod tests;
problemreductions/models/formula/ksat.rs

problemreductions/models/formula/
ksat.rs
