From 6d7a0b91b413e2a3190906d2052c1da5647e81b9 Mon Sep 17 00:00:00 2001 From: semiexp Date: Sun, 16 Aug 2026 07:55:35 +0000 Subject: [PATCH 1/2] add erase_subsumed_clauses flag to encode_linear_eq_direct_from_info --- cspuz_core/src/encoder/direct.rs | 158 +++++++++++++++++++++++++++---- cspuz_core/src/encoder/log.rs | 2 +- 2 files changed, 143 insertions(+), 17 deletions(-) diff --git a/cspuz_core/src/encoder/direct.rs b/cspuz_core/src/encoder/direct.rs index 377a47a9..bbea2215 100644 --- a/cspuz_core/src/encoder/direct.rs +++ b/cspuz_core/src/encoder/direct.rs @@ -171,7 +171,7 @@ pub(super) fn encode_linear_eq_direct(env: &EncoderEnv, sum: &LinearSum) -> Clau .len() .cmp(&encoding2.encoding.lits.len()) }); - encode_linear_eq_direct_from_info(env, &info, sum.constant) + encode_linear_eq_direct_from_info(env, &info, sum.constant, true) } fn encode_linear_eq_direct_two_terms( @@ -199,11 +199,22 @@ pub(super) fn encode_linear_eq_direct_from_info( _env: &EncoderEnv, info: &[LinearInfoForDirectEncoding], constant: CheckedInt, + erase_subsumed_clauses: bool, ) -> ClauseSet { if info.len() == 2 { return encode_linear_eq_direct_two_terms(info, constant); } + // Recursively enumerate partial value assignments for all terms except the last one. + // `clause` contains the negations of the selected values, while `lower_bound` and + // `upper_bound` are the possible range of the sum under those selections. + // `min_relax_for_lb` and `min_relax_for_ub` are the minimum amounts by which the + // corresponding bound would be relaxed if any one selected value were unselected; + // they are used to avoid emitting a nogood subsumed by a shorter one. The branch + // that advances `idx` without selecting a value enumerates such less-specific + // partial assignments, allowing shorter nogoods and more general support clauses + // to be found. If the range excludes zero, emit a preferably minimal nogood; at + // the last term, emit a support clause containing all values that may make the sum zero. fn encode_sub( info: &[LinearInfoForDirectEncoding], clause: &mut Vec, @@ -213,23 +224,18 @@ pub(super) fn encode_linear_eq_direct_from_info( min_relax_for_lb: Option, min_relax_for_ub: Option, clauses_buf: &mut ClauseSet, + erase_subsumed_clauses: bool, ) { if lower_bound > 0 || upper_bound < 0 { - let mut cannot_prune = true; - if lower_bound > 0 - && min_relax_for_lb - .map(|m| lower_bound - m <= 0) - .unwrap_or(true) - { - cannot_prune = true; - } - if upper_bound < 0 - && min_relax_for_ub - .map(|m| upper_bound + m >= 0) - .unwrap_or(true) - { - cannot_prune = true; - } + let cannot_prune = !erase_subsumed_clauses + || (lower_bound > 0 + && min_relax_for_lb + .map(|m| lower_bound - m <= 0) + .unwrap_or(true)) + || (upper_bound < 0 + && min_relax_for_ub + .map(|m| upper_bound + m >= 0) + .unwrap_or(true)); if cannot_prune { clauses_buf.push(clause); } @@ -295,6 +301,7 @@ pub(super) fn encode_linear_eq_direct_from_info( next_min_relax_for_lb, next_min_relax_for_ub, clauses_buf, + erase_subsumed_clauses, ); clause.pop(); } @@ -308,6 +315,7 @@ pub(super) fn encode_linear_eq_direct_from_info( min_relax_for_lb, min_relax_for_ub, clauses_buf, + erase_subsumed_clauses, ); } @@ -328,6 +336,7 @@ pub(super) fn encode_linear_eq_direct_from_info( None, None, &mut clauses_buf, + erase_subsumed_clauses, ); clauses_buf @@ -431,6 +440,93 @@ mod tests { use crate::arithmetic::CmpOp; use crate::domain::Domain; use crate::norm_csp::LinearLit; + use std::collections::BTreeSet; + + fn canonical_clause_set(clauses: ClauseSet) -> BTreeSet> { + let mut ret = BTreeSet::new(); + for i in 0..clauses.len() { + let mut clause = clauses[i].to_vec(); + clause.sort_unstable(); + clause.dedup(); + ret.insert(clause); + } + ret + } + + fn subsumes(lhs: &[Lit], rhs: &[Lit]) -> bool { + lhs.iter().all(|lit| rhs.binary_search(lit).is_ok()) + } + + fn check_erase_subsumed_clauses(domains: &[Vec], coefs: &[i32], constant: i32) { + assert_eq!(domains.len(), coefs.len()); + + let mut tester = EncoderTester::new(); + let vars = domains + .iter() + .map(|domain| tester.add_int_var(Domain::enumerative(domain.clone()), true)) + .collect::>(); + let terms = vars + .iter() + .copied() + .zip(coefs.iter().copied()) + .collect::>(); + let sum = linear_sum(&terms, constant); + + let env = tester.env(); + let mut info = sum + .iter() + .map(|(&var, &coef)| { + LinearInfoForDirectEncoding::new( + coef, + env.map.int_map[var].as_ref().unwrap().as_direct_encoding(), + ) + }) + .collect::>(); + info.sort_by_key(|term| term.encoding.lits.len()); + + let erased = canonical_clause_set(encode_linear_eq_direct_from_info( + &env, + &info, + sum.constant, + true, + )); + let all = canonical_clause_set(encode_linear_eq_direct_from_info( + &env, + &info, + sum.constant, + false, + )); + + let instance = || format!("domains={domains:?}, coefs={coefs:?}, constant={constant}"); + + assert!( + erased.len() < all.len() && erased.is_subset(&all), + "the erased clause set must be a proper subset: {}\nerased={erased:?}\nall={all:?}", + instance() + ); + + for removed in all.difference(&erased) { + assert!( + erased.iter().any(|clause| subsumes(clause, removed)), + "removed clause is not subsumed by a retained clause: {}\nremoved={removed:?}\nerased={erased:?}", + instance() + ); + } + + // TODO: Enable this minimality check after the optimization also + // removes subsumed support clauses from the retained clause set. + /* + for clause in &erased { + assert!( + !erased + .iter() + .any(|other| other != clause && subsumes(other, clause)), + "retained clause is subsumed by another retained clause: {}\nclause={clause:?}\nerased={erased:?}", + instance() + ); + } + */ + } #[test] fn test_encode_simple_linear_direct_encoding() { @@ -490,6 +586,36 @@ mod tests { tester.run_check(); } + #[test] + fn test_encode_linear_eq_direct_erase_subsumed_clauses() { + let instances = [ + ( + vec![vec![0, 2], vec![0, 6], vec![0, 1, 2]], + vec![1, 1, 1], + -5, + ), + ( + vec![vec![-2, 0], vec![-6, 0], vec![-2, -1, 0]], + vec![1, 1, 1], + 5, + ), + ( + vec![vec![0, 2], vec![-6, 0], vec![0, 1, 2]], + vec![1, -1, 1], + -5, + ), + ( + vec![vec![0, 2], vec![0, 3], vec![0, 10], vec![0, 1, 2, 3]], + vec![1, 1, 1, 1], + -10, + ), + ]; + + for (domains, coefs, constant) in instances { + check_erase_subsumed_clauses(&domains, &coefs, constant); + } + } + #[test] fn test_encode_linear_ne_direct() { let mut tester = EncoderTester::new(); diff --git a/cspuz_core/src/encoder/log.rs b/cspuz_core/src/encoder/log.rs index ee0df6ec..4bcc30ff 100644 --- a/cspuz_core/src/encoder/log.rs +++ b/cspuz_core/src/encoder/log.rs @@ -783,7 +783,7 @@ fn log_encoding_adder2_direct( }); } - let c = encode_linear_eq_direct_from_info(env, &infos, target); + let c = encode_linear_eq_direct_from_info(env, &infos, target, true); clause_set.append(c); carry_low = new_carry_low; From 39b3e9749d334a6a0df8a06ae5466029eb260f86 Mon Sep 17 00:00:00 2001 From: semiexp Date: Sun, 16 Aug 2026 08:04:49 +0000 Subject: [PATCH 2/2] add subsumption tests for encode_linear_ge_mixed_from_info --- cspuz_core/src/encoder/direct.rs | 62 ++----------- cspuz_core/src/encoder/log.rs | 4 +- cspuz_core/src/encoder/mixed.rs | 125 ++++++++++++++++++++++++--- cspuz_core/src/encoder/mod.rs | 2 + cspuz_core/src/encoder/test_utils.rs | 48 ++++++++++ 5 files changed, 172 insertions(+), 69 deletions(-) create mode 100644 cspuz_core/src/encoder/test_utils.rs diff --git a/cspuz_core/src/encoder/direct.rs b/cspuz_core/src/encoder/direct.rs index bbea2215..80c40e42 100644 --- a/cspuz_core/src/encoder/direct.rs +++ b/cspuz_core/src/encoder/direct.rs @@ -436,26 +436,11 @@ pub(super) fn encode_linear_ne_direct(env: &EncoderEnv, sum: &LinearSum) -> Clau mod tests { use super::*; + use super::super::test_utils::assert_erase_subsumed_clauses; use super::super::tests::{linear_sum, EncoderTester}; use crate::arithmetic::CmpOp; use crate::domain::Domain; use crate::norm_csp::LinearLit; - use std::collections::BTreeSet; - - fn canonical_clause_set(clauses: ClauseSet) -> BTreeSet> { - let mut ret = BTreeSet::new(); - for i in 0..clauses.len() { - let mut clause = clauses[i].to_vec(); - clause.sort_unstable(); - clause.dedup(); - ret.insert(clause); - } - ret - } - - fn subsumes(lhs: &[Lit], rhs: &[Lit]) -> bool { - lhs.iter().all(|lit| rhs.binary_search(lit).is_ok()) - } fn check_erase_subsumed_clauses(domains: &[Vec], coefs: &[i32], constant: i32) { assert_eq!(domains.len(), coefs.len()); @@ -484,48 +469,11 @@ mod tests { .collect::>(); info.sort_by_key(|term| term.encoding.lits.len()); - let erased = canonical_clause_set(encode_linear_eq_direct_from_info( - &env, - &info, - sum.constant, - true, - )); - let all = canonical_clause_set(encode_linear_eq_direct_from_info( - &env, - &info, - sum.constant, - false, - )); - - let instance = || format!("domains={domains:?}, coefs={coefs:?}, constant={constant}"); - - assert!( - erased.len() < all.len() && erased.is_subset(&all), - "the erased clause set must be a proper subset: {}\nerased={erased:?}\nall={all:?}", - instance() - ); - - for removed in all.difference(&erased) { - assert!( - erased.iter().any(|clause| subsumes(clause, removed)), - "removed clause is not subsumed by a retained clause: {}\nremoved={removed:?}\nerased={erased:?}", - instance() - ); - } + let erased = encode_linear_eq_direct_from_info(&env, &info, sum.constant, true); + let all = encode_linear_eq_direct_from_info(&env, &info, sum.constant, false); - // TODO: Enable this minimality check after the optimization also - // removes subsumed support clauses from the retained clause set. - /* - for clause in &erased { - assert!( - !erased - .iter() - .any(|other| other != clause && subsumes(other, clause)), - "retained clause is subsumed by another retained clause: {}\nclause={clause:?}\nerased={erased:?}", - instance() - ); - } - */ + let instance = format!("domains={domains:?}, coefs={coefs:?}, constant={constant}"); + assert_erase_subsumed_clauses(erased, all, &instance); } #[test] diff --git a/cspuz_core/src/encoder/log.rs b/cspuz_core/src/encoder/log.rs index 4bcc30ff..d1a61413 100644 --- a/cspuz_core/src/encoder/log.rs +++ b/cspuz_core/src/encoder/log.rs @@ -525,7 +525,7 @@ fn log_encoding_adder( })); { - let c = encode_linear_ge_mixed_from_info(&infos, pos_constant[i]); + let c = encode_linear_ge_mixed_from_info(&infos, pos_constant[i], true); clause_set.append(c); } { @@ -535,7 +535,7 @@ fn log_encoding_adder( _ => unreachable!(), } } - let c = encode_linear_ge_mixed_from_info(&infos, -pos_constant[i]); + let c = encode_linear_ge_mixed_from_info(&infos, -pos_constant[i], true); clause_set.append(c); } carry = carry_next; diff --git a/cspuz_core/src/encoder/mixed.rs b/cspuz_core/src/encoder/mixed.rs index 277aa5b5..580eac10 100644 --- a/cspuz_core/src/encoder/mixed.rs +++ b/cspuz_core/src/encoder/mixed.rs @@ -24,7 +24,7 @@ pub(super) fn encode_linear_ge_mixed(env: &EncoderEnv, sum: &LinearSum) -> Claus } } - encode_linear_ge_mixed_from_info(&info, sum.constant) + encode_linear_ge_mixed_from_info(&info, sum.constant, true) } #[allow(unused)] @@ -33,20 +33,21 @@ pub(super) fn encode_linear_eq_mixed_from_info( mut info: Vec, constant: CheckedInt, ) -> ClauseSet { - let mut ret = encode_linear_ge_mixed_from_info(&info, constant); + let mut ret = encode_linear_ge_mixed_from_info(&info, constant, true); for x in &mut info { match x { LinearInfo::Direct(x) => x.coef *= CheckedInt::new(-1), LinearInfo::Order(x) => x.coef *= CheckedInt::new(-1), } } - ret.append(encode_linear_ge_mixed_from_info(&info, -constant)); + ret.append(encode_linear_ge_mixed_from_info(&info, -constant, true)); ret } pub(super) fn encode_linear_ge_mixed_from_info( info: &[LinearInfo], constant: CheckedInt, + erase_subsumed_clauses: bool, ) -> ClauseSet { fn encode_sub( info: &[LinearInfo], @@ -55,14 +56,16 @@ pub(super) fn encode_linear_ge_mixed_from_info( upper_bound: CheckedInt, min_relax_on_erasure: Option, clauses_buf: &mut ClauseSet, + erase_subsumed_clauses: bool, ) { if upper_bound < 0 { - if let Some(min_relax_on_erasure) = min_relax_on_erasure { - if upper_bound + min_relax_on_erasure < 0 { - return; - } + let cannot_prune = !erase_subsumed_clauses + || min_relax_on_erasure + .map(|min_relax| upper_bound + min_relax >= 0) + .unwrap_or(true); + if cannot_prune { + clauses_buf.push(clause); } - clauses_buf.push(clause); return; } if idx == info.len() { @@ -92,7 +95,15 @@ pub(super) fn encode_linear_ge_mixed_from_info( let next_ub = upper_bound - ub_for_this_term + value; // let next_min_relax = min_relax_on_erasure.unwrap_or(CheckedInt::max_value()).min(order_encoding.domain(i + 1) - value); clause.push(order_encoding.at_least(i + 1)); - encode_sub(info, clause, idx + 1, next_ub, None, clauses_buf); + encode_sub( + info, + clause, + idx + 1, + next_ub, + None, + clauses_buf, + erase_subsumed_clauses, + ); clause.pop(); } @@ -103,6 +114,7 @@ pub(super) fn encode_linear_ge_mixed_from_info( upper_bound, min_relax_on_erasure, clauses_buf, + erase_subsumed_clauses, ); } LinearInfo::Direct(direct_encoding) => { @@ -122,6 +134,7 @@ pub(super) fn encode_linear_ge_mixed_from_info( next_ub, Some(next_min_relax), clauses_buf, + erase_subsumed_clauses, ); clause.pop(); } @@ -133,6 +146,7 @@ pub(super) fn encode_linear_ge_mixed_from_info( upper_bound, min_relax_on_erasure, clauses_buf, + erase_subsumed_clauses, ); } } @@ -147,7 +161,15 @@ pub(super) fn encode_linear_ge_mixed_from_info( } let mut clauses_buf = ClauseSet::new(); - encode_sub(info, &mut vec![], 0, upper_bound, None, &mut clauses_buf); + encode_sub( + info, + &mut vec![], + 0, + upper_bound, + None, + &mut clauses_buf, + erase_subsumed_clauses, + ); clauses_buf } @@ -156,11 +178,60 @@ pub(super) fn encode_linear_ge_mixed_from_info( mod tests { use super::*; + use super::super::test_utils::assert_erase_subsumed_clauses; use super::super::tests::{linear_sum, EncoderTester}; use crate::arithmetic::CmpOp; use crate::domain::Domain; use crate::norm_csp::{BoolLit, LinearLit}; + fn check_erase_subsumed_clauses( + domains: &[Vec], + coefs: &[i32], + direct_encoding: &[bool], + constant: i32, + ) { + assert_eq!(domains.len(), coefs.len()); + assert_eq!(domains.len(), direct_encoding.len()); + + let mut tester = EncoderTester::new(); + let vars = domains + .iter() + .zip(direct_encoding.iter().copied()) + .map(|(domain, is_direct)| { + tester.add_int_var(Domain::enumerative(domain.clone()), is_direct) + }) + .collect::>(); + let terms = vars + .iter() + .copied() + .zip(coefs.iter().copied()) + .collect::>(); + let sum = linear_sum(&terms, constant); + + let env = tester.env(); + let info = sum + .iter() + .map(|(&var, &coef)| { + let encoding = env.map.int_map[var].as_ref().unwrap(); + if let Some(order_encoding) = &encoding.order_encoding { + LinearInfo::Order(LinearInfoForOrderEncoding::new(coef, order_encoding)) + } else { + LinearInfo::Direct(LinearInfoForDirectEncoding::new( + coef, + encoding.as_direct_encoding(), + )) + } + }) + .collect::>(); + + let erased = encode_linear_ge_mixed_from_info(&info, sum.constant, true); + let all = encode_linear_ge_mixed_from_info(&info, sum.constant, false); + let instance = format!( + "domains={domains:?}, coefs={coefs:?}, direct_encoding={direct_encoding:?}, constant={constant}" + ); + assert_erase_subsumed_clauses(erased, all, &instance); + } + #[test] fn test_encode_linear_ge_mixed() { for mask in 0..8 { @@ -208,4 +279,38 @@ mod tests { tester.run_check(); } } + + #[test] + fn test_encode_linear_ge_mixed_erase_subsumed_clauses() { + let instances = [ + ( + vec![vec![0, 2], vec![0, 6], vec![0, 1, 2]], + vec![1, 1, 1], + vec![true, true, false], + -5, + ), + ( + vec![vec![-2, 0], vec![-6, 0], vec![-2, -1, 0]], + vec![-1, -1, -1], + vec![true, true, false], + -5, + ), + ( + vec![vec![0, 2], vec![-6, 0], vec![0, 1, 2]], + vec![1, -1, 1], + vec![true, true, false], + -5, + ), + ( + vec![vec![0, 2], vec![0, 3], vec![0, 10], vec![0, 1, 2, 3]], + vec![1, 1, 1, 1], + vec![true, false, true, false], + -10, + ), + ]; + + for (domains, coefs, direct_encoding, constant) in instances { + check_erase_subsumed_clauses(&domains, &coefs, &direct_encoding, constant); + } + } } diff --git a/cspuz_core/src/encoder/mod.rs b/cspuz_core/src/encoder/mod.rs index 0327ae95..badba4a9 100644 --- a/cspuz_core/src/encoder/mod.rs +++ b/cspuz_core/src/encoder/mod.rs @@ -3,6 +3,8 @@ mod direct; mod log; mod mixed; mod order; +#[cfg(test)] +mod test_utils; use std::cmp::Reverse; use std::collections::{BTreeMap, BTreeSet, BinaryHeap}; diff --git a/cspuz_core/src/encoder/test_utils.rs b/cspuz_core/src/encoder/test_utils.rs new file mode 100644 index 00000000..6af26c4b --- /dev/null +++ b/cspuz_core/src/encoder/test_utils.rs @@ -0,0 +1,48 @@ +use super::ClauseSet; +use crate::sat::Lit; +use std::collections::BTreeSet; + +fn canonical_clause_set(clauses: ClauseSet) -> BTreeSet> { + let mut ret = BTreeSet::new(); + for i in 0..clauses.len() { + let mut clause = clauses[i].to_vec(); + clause.sort_unstable(); + clause.dedup(); + ret.insert(clause); + } + ret +} + +fn subsumes(lhs: &[Lit], rhs: &[Lit]) -> bool { + lhs.iter().all(|lit| rhs.binary_search(lit).is_ok()) +} + +pub(super) fn assert_erase_subsumed_clauses(erased: ClauseSet, all: ClauseSet, instance: &str) { + let erased = canonical_clause_set(erased); + let all = canonical_clause_set(all); + + assert!( + erased.len() < all.len() && erased.is_subset(&all), + "the erased clause set must be a proper subset: {instance}\nerased={erased:?}\nall={all:?}" + ); + + for removed in all.difference(&erased) { + assert!( + erased.iter().any(|clause| subsumes(clause, removed)), + "removed clause is not subsumed by a retained clause: {instance}\nremoved={removed:?}\nerased={erased:?}" + ); + } + + // TODO: Enable this minimality check after the optimizations also remove + // subsumed clauses from the retained clause set. + /* + for clause in &erased { + assert!( + !erased + .iter() + .any(|other| other != clause && subsumes(other, clause)), + "retained clause is subsumed by another retained clause: {instance}\nclause={clause:?}\nerased={erased:?}" + ); + } + */ +}