|
| 1 | +use super::*; |
| 2 | +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; |
| 3 | +use crate::solvers::BruteForce; |
| 4 | +use crate::traits::Problem; |
| 5 | + |
| 6 | +fn reduce(source: &NAESatisfiability) -> ReductionNAESATToSAT { |
| 7 | + ReduceTo::<Satisfiability>::reduce_to(source).expect("reduction should succeed") |
| 8 | +} |
| 9 | + |
| 10 | +fn assignments(num_vars: usize) -> impl Iterator<Item = Vec<bool>> { |
| 11 | + (0..1usize << num_vars).map(move |mask| (0..num_vars).map(|i| (mask >> i) & 1 == 1).collect()) |
| 12 | +} |
| 13 | + |
| 14 | +/// Checks that source and target agree on every assignment, that satisfying |
| 15 | +/// assignments extract unchanged, and that all others are rejected. |
| 16 | +fn assert_equivalent_on_all_assignments(source: &NAESatisfiability) { |
| 17 | + let reduction = reduce(source); |
| 18 | + let target = reduction.target_problem(); |
| 19 | + assert_eq!(target.num_vars(), source.num_vars()); |
| 20 | + for assignment in assignments(source.num_vars()) { |
| 21 | + let source_ok = source.evaluate(&assignment).unwrap().0; |
| 22 | + assert_eq!( |
| 23 | + source_ok, |
| 24 | + target.evaluate(&assignment).unwrap().0, |
| 25 | + "disagreement on {assignment:?}" |
| 26 | + ); |
| 27 | + match reduction.extract_solution(&assignment) { |
| 28 | + Ok(extracted) => { |
| 29 | + assert!(source_ok, "accepted non-witness {assignment:?}"); |
| 30 | + assert_eq!(extracted, assignment); |
| 31 | + } |
| 32 | + Err(_) => assert!(!source_ok, "rejected witness {assignment:?}"), |
| 33 | + } |
| 34 | + } |
| 35 | +} |
| 36 | + |
| 37 | +fn canonical_source() -> NAESatisfiability { |
| 38 | + NAESatisfiability::new( |
| 39 | + 3, |
| 40 | + vec![ |
| 41 | + CNFClause::new(vec![1, 2, 3]), |
| 42 | + CNFClause::new(vec![-1, 2]), |
| 43 | + CNFClause::new(vec![1, -2, -3]), |
| 44 | + ], |
| 45 | + ) |
| 46 | +} |
| 47 | + |
| 48 | +#[test] |
| 49 | +fn test_naesatisfiability_to_satisfiability_closed_loop() { |
| 50 | + let source = canonical_source(); |
| 51 | + let reduction = reduce(&source); |
| 52 | + assert_satisfaction_round_trip_from_satisfaction_target( |
| 53 | + &source, |
| 54 | + &reduction, |
| 55 | + "NAE-SAT->SAT closed loop", |
| 56 | + ); |
| 57 | +} |
| 58 | + |
| 59 | +#[test] |
| 60 | +fn test_naesatisfiability_to_satisfiability_structure() { |
| 61 | + let source = canonical_source(); |
| 62 | + let reduction = reduce(&source); |
| 63 | + let target = reduction.target_problem(); |
| 64 | + |
| 65 | + assert_eq!(target.num_vars(), 3); |
| 66 | + assert_eq!(target.num_clauses(), 2 * source.num_clauses()); |
| 67 | + assert_eq!(target.num_literals(), 2 * source.num_literals()); |
| 68 | + let literals: Vec<Vec<i64>> = target |
| 69 | + .clauses() |
| 70 | + .iter() |
| 71 | + .map(|clause| clause.literals.clone()) |
| 72 | + .collect(); |
| 73 | + assert_eq!( |
| 74 | + literals, |
| 75 | + vec![ |
| 76 | + vec![1, 2, 3], |
| 77 | + vec![-1, -2, -3], |
| 78 | + vec![-1, 2], |
| 79 | + vec![1, -2], |
| 80 | + vec![1, -2, -3], |
| 81 | + vec![-1, 2, 3], |
| 82 | + ] |
| 83 | + ); |
| 84 | +} |
| 85 | + |
| 86 | +#[test] |
| 87 | +fn test_naesatisfiability_to_satisfiability_canonical_all_assignments() { |
| 88 | + let source = canonical_source(); |
| 89 | + assert_equivalent_on_all_assignments(&source); |
| 90 | + |
| 91 | + let witnesses: Vec<Vec<bool>> = assignments(3) |
| 92 | + .filter(|assignment| source.evaluate(assignment).unwrap().0) |
| 93 | + .collect(); |
| 94 | + assert_eq!( |
| 95 | + witnesses, |
| 96 | + vec![vec![true, true, false], vec![false, false, true]] |
| 97 | + ); |
| 98 | +} |
| 99 | + |
| 100 | +#[test] |
| 101 | +fn test_naesatisfiability_to_satisfiability_witness_and_near_witness() { |
| 102 | + let reduction = reduce(&canonical_source()); |
| 103 | + |
| 104 | + assert_eq!( |
| 105 | + reduction.extract_solution(&vec![false, false, true]).unwrap(), |
| 106 | + vec![false, false, true] |
| 107 | + ); |
| 108 | + // [0,1,0] makes (¬x1, x2) all true, so the excluded all-true CNF clause fails. |
| 109 | + let error = reduction |
| 110 | + .extract_solution(&vec![false, true, false]) |
| 111 | + .unwrap_err(); |
| 112 | + assert!(error |
| 113 | + .to_string() |
| 114 | + .contains("target assignment does not satisfy CNF clauses")); |
| 115 | +} |
| 116 | + |
| 117 | +#[test] |
| 118 | +fn test_naesatisfiability_to_satisfiability_rejects_malformed_assignment() { |
| 119 | + let reduction = reduce(&canonical_source()); |
| 120 | + assert!(reduction.extract_solution(&vec![false, false]).is_err()); |
| 121 | + assert!(reduction |
| 122 | + .extract_solution(&vec![false, false, true, false]) |
| 123 | + .is_err()); |
| 124 | +} |
| 125 | + |
| 126 | +#[test] |
| 127 | +fn test_naesatisfiability_to_satisfiability_empty_conjunction() { |
| 128 | + for num_vars in [0, 2] { |
| 129 | + let source = NAESatisfiability::new(num_vars, vec![]); |
| 130 | + let reduction = reduce(&source); |
| 131 | + let target = reduction.target_problem(); |
| 132 | + assert_eq!(target.num_vars(), num_vars); |
| 133 | + assert_eq!(target.num_clauses(), 0); |
| 134 | + assert_eq!(target.num_literals(), 0); |
| 135 | + assert_equivalent_on_all_assignments(&source); |
| 136 | + } |
| 137 | +} |
| 138 | + |
| 139 | +#[test] |
| 140 | +fn test_naesatisfiability_to_satisfiability_unsatisfiable_repeated_variable() { |
| 141 | + let source = NAESatisfiability::new(1, vec![CNFClause::new(vec![1, 1])]); |
| 142 | + let reduction = reduce(&source); |
| 143 | + let literals: Vec<Vec<i64>> = reduction |
| 144 | + .target_problem() |
| 145 | + .clauses() |
| 146 | + .iter() |
| 147 | + .map(|clause| clause.literals.clone()) |
| 148 | + .collect(); |
| 149 | + assert_eq!(literals, vec![vec![1, 1], vec![-1, -1]]); |
| 150 | + |
| 151 | + let solver = BruteForce::new(); |
| 152 | + assert!(solver.solve(&source).unwrap().is_none()); |
| 153 | + assert!(solver.solve(reduction.target_problem()).unwrap().is_none()); |
| 154 | + assert_equivalent_on_all_assignments(&source); |
| 155 | +} |
| 156 | + |
| 157 | +#[test] |
| 158 | +fn test_naesatisfiability_to_satisfiability_repeated_literals() { |
| 159 | + // NAE(x1, x1, x2) holds exactly when x1 != x2. |
| 160 | + let source = NAESatisfiability::new(2, vec![CNFClause::new(vec![1, 1, 2])]); |
| 161 | + assert_equivalent_on_all_assignments(&source); |
| 162 | +} |
| 163 | + |
| 164 | +#[test] |
| 165 | +fn test_naesatisfiability_to_satisfiability_tautological_clauses() { |
| 166 | + // (x1, ¬x1) always has one true and one false literal. |
| 167 | + let source = NAESatisfiability::new( |
| 168 | + 2, |
| 169 | + vec![CNFClause::new(vec![1, -1]), CNFClause::new(vec![2, -2, 1])], |
| 170 | + ); |
| 171 | + let reduction = reduce(&source); |
| 172 | + assert_eq!( |
| 173 | + reduction.target_problem().clauses()[1].literals, |
| 174 | + vec![-1, 1] |
| 175 | + ); |
| 176 | + assert_equivalent_on_all_assignments(&source); |
| 177 | +} |
| 178 | + |
| 179 | +#[test] |
| 180 | +fn test_naesatisfiability_to_satisfiability_arbitrary_clause_lengths() { |
| 181 | + let source = NAESatisfiability::new( |
| 182 | + 5, |
| 183 | + vec![ |
| 184 | + CNFClause::new(vec![1, -2]), |
| 185 | + CNFClause::new(vec![2, 3, -4]), |
| 186 | + CNFClause::new(vec![-1, 3, 4, 5]), |
| 187 | + CNFClause::new(vec![1, 2, -3, -4, 5]), |
| 188 | + ], |
| 189 | + ); |
| 190 | + let reduction = reduce(&source); |
| 191 | + let target = reduction.target_problem(); |
| 192 | + assert_eq!(target.num_clauses(), 8); |
| 193 | + assert_eq!(target.num_literals(), 2 * 14); |
| 194 | + assert_equivalent_on_all_assignments(&source); |
| 195 | + assert_satisfaction_round_trip_from_satisfaction_target( |
| 196 | + &source, |
| 197 | + &reduction, |
| 198 | + "NAE-SAT->SAT mixed clause lengths", |
| 199 | + ); |
| 200 | +} |
0 commit comments