Skip to content

Commit 458c682

Browse files
radevgitradevgit
committed
Implemented bool_clause
1 parent f3c8c4e commit 458c682

File tree

2 files changed

+340
-0
lines changed

2 files changed

+340
-0
lines changed

‎src/model/constraints.rs‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -653,4 +653,80 @@ impl Model {
653653
// Post less-than-or-equal constraint: sum ≤ constant
654654
self.props.less_than_or_equals(sum_var, Val::ValI(constant));
655655
}
656+
657+
// ═══════════════════════════════════════════════════════════════════════
658+
// 🔀 Boolean Clause (CNF/SAT Support)
659+
// ═══════════════════════════════════════════════════════════════════════
660+
661+
/// Post a boolean clause constraint: `(∨ pos[i]) ∨ (∨ ¬neg[i])`.
662+
///
663+
/// This implements the FlatZinc `bool_clause` constraint, which represents
664+
/// a clause in CNF (Conjunctive Normal Form). The clause is satisfied if:
665+
/// - At least one positive literal is true, OR
666+
/// - At least one negative literal is false
667+
///
668+
/// In other words: `pos[0] ∨ pos[1] ∨ ... ∨ ¬neg[0] ∨ ¬neg[1] ∨ ...`
669+
///
670+
/// # Arguments
671+
/// * `pos` - Array of positive boolean literals (variables that should be true)
672+
/// * `neg` - Array of negative boolean literals (variables that should be false)
673+
///
674+
/// # Examples
675+
/// ```
676+
/// use selen::prelude::*;
677+
/// let mut m = Model::default();
678+
/// let a = m.bool();
679+
/// let b = m.bool();
680+
/// let c = m.bool();
681+
///
682+
/// // At least one of: a is true, b is true, or c is false
683+
/// // Equivalent to: a ∨ b ∨ ¬c
684+
/// m.bool_clause(&[a, b], &[c]);
685+
/// ```
686+
///
687+
/// # Implementation
688+
///
689+
/// The clause is decomposed as:
690+
/// 1. If both arrays are empty, the clause is unsatisfiable (posts false)
691+
/// 2. Otherwise, we create: `(∨ pos[i]) ∨ (∨ ¬neg[i]) = true`
692+
/// - This ensures at least one positive literal is 1, or one negative literal is 0
693+
pub fn bool_clause(&mut self, pos: &[VarId], neg: &[VarId]) {
694+
// Empty clause is unsatisfiable
695+
if pos.is_empty() && neg.is_empty() {
696+
// Post an unsatisfiable constraint: 0 = 1
697+
self.props.equals(Val::ValI(0), Val::ValI(1));
698+
return;
699+
}
700+
701+
// Special case: only positive literals
702+
if neg.is_empty() {
703+
// At least one positive literal must be true: bool_or(pos) = 1
704+
let clause_result = self.bool_or(pos);
705+
self.props.equals(clause_result, Val::ValI(1));
706+
return;
707+
}
708+
709+
// Special case: only negative literals
710+
if pos.is_empty() {
711+
// At least one negative literal must be false
712+
// ¬neg[0] ∨ ¬neg[1] ∨ ... = ¬(neg[0] ∧ neg[1] ∧ ...)
713+
let all_neg = self.bool_and(neg);
714+
let not_all_neg = self.bool_not(all_neg);
715+
self.props.equals(not_all_neg, Val::ValI(1));
716+
return;
717+
}
718+
719+
// General case: both positive and negative literals
720+
// pos[0] ∨ ... ∨ ¬neg[0] ∨ ...
721+
// = (pos[0] ∨ ... ∨ pos[n]) ∨ (¬neg[0] ∨ ... ∨ ¬neg[m])
722+
// = (∨ pos[i]) ∨ ¬(∧ neg[i])
723+
724+
let pos_clause = self.bool_or(pos);
725+
let all_neg = self.bool_and(neg);
726+
let not_all_neg = self.bool_not(all_neg);
727+
728+
// At least one side must be true
729+
let final_clause = self.bool_or(&[pos_clause, not_all_neg]);
730+
self.props.equals(final_clause, Val::ValI(1));
731+
}
656732
}

‎tests/test_bool_clause.rs‎

Lines changed: 264 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,264 @@
1+
use selen::prelude::*;
2+
3+
// ═══════════════════════════════════════════════════════════════════════════
4+
// Test Suite: bool_clause Constraint
5+
// ═══════════════════════════════════════════════════════════════════════════
6+
//
7+
// The `bool_clause` constraint represents a CNF clause:
8+
// bool_clause(pos, neg) ≡ (∨ pos[i]) ∨ (∨ ¬neg[i])
9+
//
10+
// This means: at least one positive literal is true OR at least one negative
11+
// literal is false.
12+
//
13+
// Coverage:
14+
// - Simple positive-only clauses
15+
// - Simple negative-only clauses
16+
// - Mixed positive and negative literals
17+
// - Edge cases: empty arrays, tautologies
18+
// - SAT/UNSAT scenarios
19+
// ═══════════════════════════════════════════════════════════════════════════
20+
21+
#[test]
22+
fn test_bool_clause_positive_only_sat() {
23+
// Clause: a ∨ b ∨ c (at least one must be true)
24+
let mut m = Model::default();
25+
let a = m.bool();
26+
let b = m.bool();
27+
let c = m.bool();
28+
29+
m.bool_clause(&[a, b, c], &[]);
30+
31+
let solution = m.solve().expect("Should find solution where at least one is true");
32+
33+
let val_a = solution[a] == Val::ValI(1);
34+
let val_b = solution[b] == Val::ValI(1);
35+
let val_c = solution[c] == Val::ValI(1);
36+
37+
// At least one must be true
38+
assert!(val_a || val_b || val_c, "At least one variable should be true");
39+
}
40+
41+
#[test]
42+
fn test_bool_clause_positive_only_with_fixed() {
43+
// Clause: a ∨ b where we force both false (should be UNSAT)
44+
let mut m = Model::default();
45+
let a = m.bool();
46+
let b = m.bool();
47+
48+
m.bool_clause(&[a, b], &[]);
49+
m.props.equals(a, Val::ValI(0)); // Force a = false
50+
m.props.equals(b, Val::ValI(0)); // Force b = false
51+
52+
assert!(m.solve().is_err(), "Should be UNSAT when all positive literals forced false");
53+
}
54+
55+
#[test]
56+
fn test_bool_clause_negative_only_sat() {
57+
// Clause: ¬a ∨ ¬b ∨ ¬c (at least one must be false)
58+
let mut m = Model::default();
59+
let a = m.bool();
60+
let b = m.bool();
61+
let c = m.bool();
62+
63+
m.bool_clause(&[], &[a, b, c]);
64+
65+
let solution = m.solve().expect("Should find solution where at least one is false");
66+
67+
let val_a = solution[a] == Val::ValI(1);
68+
let val_b = solution[b] == Val::ValI(1);
69+
let val_c = solution[c] == Val::ValI(1);
70+
71+
// At least one must be false
72+
assert!(!val_a || !val_b || !val_c, "At least one variable should be false");
73+
}
74+
75+
#[test]
76+
fn test_bool_clause_negative_only_with_fixed() {
77+
// Clause: ¬a ∨ ¬b where we force both true (should be UNSAT)
78+
let mut m = Model::default();
79+
let a = m.bool();
80+
let b = m.bool();
81+
82+
m.bool_clause(&[], &[a, b]);
83+
m.props.equals(a, Val::ValI(1)); // Force a = true
84+
m.props.equals(b, Val::ValI(1)); // Force b = true
85+
86+
assert!(m.solve().is_err(), "Should be UNSAT when all negative literals forced true");
87+
}
88+
89+
#[test]
90+
fn test_bool_clause_mixed_sat() {
91+
// Clause: a ∨ b ∨ ¬c ∨ ¬d
92+
// At least one of: a is true, b is true, c is false, or d is false
93+
let mut m = Model::default();
94+
let a = m.bool();
95+
let b = m.bool();
96+
let c = m.bool();
97+
let d = m.bool();
98+
99+
m.bool_clause(&[a, b], &[c, d]);
100+
101+
let solution = m.solve().expect("Should find a satisfying assignment");
102+
103+
let val_a = solution[a] == Val::ValI(1);
104+
let val_b = solution[b] == Val::ValI(1);
105+
let val_c = solution[c] == Val::ValI(1);
106+
let val_d = solution[d] == Val::ValI(1);
107+
108+
// At least one condition must hold
109+
assert!(
110+
val_a || val_b || !val_c || !val_d,
111+
"Clause should be satisfied: a ∨ b ∨ ¬c ∨ ¬d"
112+
);
113+
}
114+
115+
#[test]
116+
fn test_bool_clause_mixed_with_constraints() {
117+
// Clause: a ∨ ¬b with additional constraints
118+
let mut m = Model::default();
119+
let a = m.bool();
120+
let b = m.bool();
121+
122+
m.bool_clause(&[a], &[b]);
123+
124+
// Force a = false, so b must be false too
125+
m.props.equals(a, Val::ValI(0));
126+
127+
let solution = m.solve().expect("Should be SAT");
128+
129+
assert_eq!(solution[a], Val::ValI(0), "a should be false (forced)");
130+
assert_eq!(solution[b], Val::ValI(0), "b must be false since a is false");
131+
}
132+
133+
#[test]
134+
fn test_bool_clause_mixed_unsat() {
135+
// Clause: a ∨ ¬b where we force a=false and b=true (should be UNSAT)
136+
let mut m = Model::default();
137+
let a = m.bool();
138+
let b = m.bool();
139+
140+
m.bool_clause(&[a], &[b]);
141+
m.props.equals(a, Val::ValI(0)); // Force a = false
142+
m.props.equals(b, Val::ValI(1)); // Force b = true
143+
144+
assert!(m.solve().is_err(), "Should be UNSAT: a=false and b=true violates a ∨ ¬b");
145+
}
146+
147+
#[test]
148+
fn test_bool_clause_single_positive() {
149+
// Clause: a (just one positive literal)
150+
let mut m = Model::default();
151+
let a = m.bool();
152+
153+
m.bool_clause(&[a], &[]);
154+
155+
let solution = m.solve().expect("Should be SAT");
156+
assert_eq!(solution[a], Val::ValI(1), "a must be true");
157+
}
158+
159+
#[test]
160+
fn test_bool_clause_single_negative() {
161+
// Clause: ¬a (just one negative literal)
162+
let mut m = Model::default();
163+
let a = m.bool();
164+
165+
m.bool_clause(&[], &[a]);
166+
167+
let solution = m.solve().expect("Should be SAT");
168+
assert_eq!(solution[a], Val::ValI(0), "a must be false");
169+
}
170+
171+
#[test]
172+
fn test_bool_clause_empty_unsat() {
173+
// Empty clause: no literals at all (should be UNSAT)
174+
let mut m = Model::default();
175+
176+
m.bool_clause(&[], &[]);
177+
178+
assert!(m.solve().is_err(), "Empty clause should be UNSAT");
179+
}
180+
181+
#[test]
182+
fn test_bool_clause_tautology() {
183+
// Clause: a ∨ ¬a (always true - tautology)
184+
let mut m = Model::default();
185+
let a = m.bool();
186+
187+
m.bool_clause(&[a], &[a]);
188+
189+
let _solution = m.solve().expect("Tautology should always be SAT");
190+
}
191+
192+
#[test]
193+
fn test_bool_clause_complex_cnf() {
194+
// Multiple clauses forming a CNF formula
195+
// (a ∨ b) ∧ (¬a ∨ c) ∧ (¬b ∨ ¬c)
196+
let mut m = Model::default();
197+
let a = m.bool();
198+
let b = m.bool();
199+
let c = m.bool();
200+
201+
m.bool_clause(&[a, b], &[]); // a ∨ b
202+
m.bool_clause(&[c], &[a]); // ¬a ∨ c
203+
m.bool_clause(&[], &[b, c]); // ¬b ∨ ¬c
204+
205+
let solution = m.solve().expect("CNF should be SAT");
206+
207+
let val_a = solution[a] == Val::ValI(1);
208+
let val_b = solution[b] == Val::ValI(1);
209+
let val_c = solution[c] == Val::ValI(1);
210+
211+
// Verify all clauses are satisfied
212+
assert!(val_a || val_b, "Clause 1: a ∨ b");
213+
assert!(!val_a || val_c, "Clause 2: ¬a ∨ c");
214+
assert!(!val_b || !val_c, "Clause 3: ¬b ∨ ¬c");
215+
}
216+
217+
#[test]
218+
fn test_bool_clause_large_positive() {
219+
// Large clause with many positive literals
220+
let mut m = Model::default();
221+
let vars: Vec<VarId> = (0..10).map(|_| m.bool()).collect();
222+
223+
m.bool_clause(&vars, &[]);
224+
225+
// Force all but last to false
226+
for i in 0..9 {
227+
m.props.equals(vars[i], Val::ValI(0));
228+
}
229+
230+
let solution = m.solve().expect("Should be SAT");
231+
assert_eq!(solution[vars[9]], Val::ValI(1), "Last variable must be true");
232+
}
233+
234+
#[test]
235+
fn test_bool_clause_large_negative() {
236+
// Large clause with many negative literals
237+
let mut m = Model::default();
238+
let vars: Vec<VarId> = (0..10).map(|_| m.bool()).collect();
239+
240+
m.bool_clause(&[], &vars);
241+
242+
// Force all but last to true
243+
for i in 0..9 {
244+
m.props.equals(vars[i], Val::ValI(1));
245+
}
246+
247+
let solution = m.solve().expect("Should be SAT");
248+
assert_eq!(solution[vars[9]], Val::ValI(0), "Last variable must be false");
249+
}
250+
251+
#[test]
252+
fn test_bool_clause_implications() {
253+
// Test clause as implication: a → b is equivalent to ¬a ∨ b
254+
let mut m = Model::default();
255+
let a = m.bool();
256+
let b = m.bool();
257+
258+
m.bool_clause(&[b], &[a]); // ¬a ∨ b (i.e., a → b)
259+
m.props.equals(a, Val::ValI(1)); // Force a = true
260+
261+
let solution = m.solve().expect("Should be SAT");
262+
assert_eq!(solution[a], Val::ValI(1), "a is true (forced)");
263+
assert_eq!(solution[b], Val::ValI(1), "b must be true (by implication)");
264+
}

0 commit comments

Comments
 (0)