diff --git a/cspuz_core/src/encoder/log.rs b/cspuz_core/src/encoder/log.rs index e297bd72..8d066e85 100644 --- a/cspuz_core/src/encoder/log.rs +++ b/cspuz_core/src/encoder/log.rs @@ -7,34 +7,48 @@ use super::mixed::{encode_linear_eq_mixed_from_info, encode_linear_ge_mixed_from use super::order::{LinearInfoForOrderEncoding, OrderEncoding}; use super::{new_var, new_vars_as_lits, ClauseSet, EncoderEnv, LinearInfo, LinearLit}; use crate::arithmetic::{CheckedInt, CmpOp, Range}; -use crate::norm_csp::{IntVar, IntVarRepresentation, LinearSum}; +use crate::domain::Domain; +use crate::encoder::EncodeMap; +use crate::norm_csp::{IntVar, IntVarRepresentation, LinearSum, NormCSPVars}; use crate::sat::{Lit, SAT}; /// Representation of a log-encoded variable. /// /// The value of the variable equals lits[0] * 2^0 + lits[1] * 2^1 + ... + lits[n-1] * 2^(n-1) + offset. -/// `low` and `high` represent the range of the value after applying the offset. +/// `range` represents the range of the actual value (offsets are added). +/// Currently, `offset` is used only to handle negative values in the domain. +/// Therefore, `offset` is always non-positive. pub(super) struct LogEncoding { pub lits: Vec, pub range: Range, + pub offset: CheckedInt, } -pub fn encode_var_log(sat: &mut SAT, repr: &IntVarRepresentation) -> LogEncoding { +pub fn encode_var_log( + encode_map: &mut EncodeMap, + norm_vars: &NormCSPVars, + sat: &mut SAT, + repr: &IntVarRepresentation, +) -> LogEncoding { match repr { IntVarRepresentation::Domain(domain) => { let low = domain.lower_bound_checked(); let high = domain.upper_bound_checked(); - if low < 0 { - todo!("negative values not supported in log encoding"); - } - let n_bits = (32 - high.get().leading_zeros()) as usize; + + // Calculate offset to handle negative values + let offset = if low < 0 { low } else { CheckedInt::new(0) }; + let shifted_low = low - offset; + let shifted_high = high - offset; + + let n_bits = (32 - shifted_high.get().leading_zeros()) as usize; let lits = new_vars_as_lits!(sat, n_bits, "{}.log", var.id()); + // Add constraints for the lower bound for i in 0..n_bits { - if ((low.get() >> i) & 1) != 0 { + if ((shifted_low.get() >> i) & 1) != 0 { let mut clause = vec![lits[i]]; for j in (i + 1)..n_bits { - clause.push(if (low.get() >> j) & 1 != 0 { + clause.push(if (shifted_low.get() >> j) & 1 != 0 { !lits[j] } else { lits[j] @@ -44,11 +58,12 @@ pub fn encode_var_log(sat: &mut SAT, repr: &IntVarRepresentation) -> LogEncoding } } + // Add constraints for the upper bound for i in 0..n_bits { - if (high.get() >> i) & 1 == 0 { + if (shifted_high.get() >> i) & 1 == 0 { let mut clause = vec![!lits[i]]; for j in (i + 1)..n_bits { - clause.push(if (high.get() >> j) & 1 != 0 { + clause.push(if (shifted_high.get() >> j) & 1 != 0 { !lits[j] } else { lits[j] @@ -58,26 +73,78 @@ pub fn encode_var_log(sat: &mut SAT, repr: &IntVarRepresentation) -> LogEncoding } } + // Add constraints to exclude gaps in the domain let domain = domain.enumerate(); for i in 1..domain.len() { let gap_low = domain[i - 1].get() + 1; let gap_high = domain[i].get(); for n in gap_low..gap_high { - let mut clause = vec![]; - for j in 0..n_bits { - clause.push(if (n >> j) & 1 != 0 { !lits[j] } else { lits[j] }); + let shifted_n = n - offset.get(); + if shifted_n >= 0 { + let mut clause = vec![]; + for j in 0..n_bits { + clause.push(if (shifted_n >> j) & 1 != 0 { + !lits[j] + } else { + lits[j] + }); + } + sat.add_clause(&clause); } - sat.add_clause(&clause); } } LogEncoding { lits, range: Range::new(low, high), + offset, } } - IntVarRepresentation::Binary { .. } => { - todo!(); + &IntVarRepresentation::Binary { + cond, + v_false, + v_true, + } => { + let cond = encode_map.convert_bool_lit(norm_vars, sat, cond); + + assert!(v_false < v_true); + + let offset = if v_false < 0 { + v_false + } else { + CheckedInt::new(0) + }; + let shifted_v_false = v_false - offset; + let shifted_v_true = v_true - offset; + let n_bits = (32 - shifted_v_true.get().leading_zeros()) as usize; + + let mut lits = vec![]; + for i in 0..n_bits { + match ( + (shifted_v_false.get() >> i) & 1, + (shifted_v_true.get() >> i) & 1, + ) { + (0, 0) => { + let lit = sat.new_var().as_lit(false); + lits.push(lit); + sat.add_clause(&[!lit]); + } + (0, 1) => lits.push(cond), + (1, 0) => lits.push(!cond), + (1, 1) => { + let lit = sat.new_var().as_lit(false); + lits.push(lit); + sat.add_clause(&[lit]); + } + _ => unreachable!(), + } + } + + LogEncoding { + lits, + range: Range::new(v_false, v_true), + offset, + } } } } @@ -176,10 +243,15 @@ pub(super) fn encode_linear_log(env: &mut EncoderEnv, sum: &LinearSum, op: CmpOp // TODO: some clauses should be directly added to `env` if op == CmpOp::Eq { let mut values = vec![]; + let mut constant = sum.constant; + for (&var, &coef) in sum.iter() { let encoding = env.map.int_map[var].as_ref().unwrap(); let log_encoding = encoding.log_encoding.as_ref().unwrap(); + // Accumulate offset contributions + constant += coef * log_encoding.offset; + if coef > 0 { let mut coef = coef.get() as u32; for i in 0usize.. { @@ -208,16 +280,20 @@ pub(super) fn encode_linear_log(env: &mut EncoderEnv, sum: &LinearSum, op: CmpOp } } } - return log_encoding_adder2(env, values, sum.constant); + return log_encoding_adder2(env, values, constant); } let mut values_positive = vec![]; let mut values_negative = vec![]; + let mut constant = sum.constant; for (&var, &coef) in sum.iter() { let encoding = env.map.int_map[var].as_ref().unwrap(); let log_encoding = encoding.log_encoding.as_ref().unwrap(); + // Accumulate offset contributions + constant += coef * log_encoding.offset; + if coef > 0 { let mut coef = coef.get() as u32; for i in 0usize.. { @@ -247,13 +323,13 @@ pub(super) fn encode_linear_log(env: &mut EncoderEnv, sum: &LinearSum, op: CmpOp let (aux_clauses1, sum_positive) = log_encoding_adder( env, values_positive, - vec![sum.constant.max(CheckedInt::new(0))], + vec![constant.max(CheckedInt::new(0))], vec![], ); let (aux_clauses2, sum_negative) = log_encoding_adder( env, values_negative, - vec![(-sum.constant).max(CheckedInt::new(0))], + vec![(-constant).max(CheckedInt::new(0))], vec![], ); @@ -725,33 +801,85 @@ fn log_encoding_adder2_direct( } pub(super) fn encode_mul_log(env: &mut EncoderEnv, x: IntVar, y: IntVar, m: IntVar) -> ClauseSet { - let x_repr = env.map.int_map[x] + let x_encoding = env.map.int_map[x] .as_ref() .unwrap() .log_encoding .as_ref() - .unwrap() - .lits - .clone(); - let y_repr = env.map.int_map[y] + .unwrap(); + let y_encoding = env.map.int_map[y] .as_ref() .unwrap() .log_encoding .as_ref() - .unwrap() - .lits - .clone(); - let m_repr = env.map.int_map[m] + .unwrap(); + let m_encoding = env.map.int_map[m] .as_ref() .unwrap() .log_encoding .as_ref() - .unwrap() - .lits - .clone(); - let m_repr_len = m_repr.len(); + .unwrap(); + + if x_encoding.offset != 0 || y_encoding.offset != 0 || m_encoding.offset != 0 { + let x_ofs = x_encoding.offset; + let y_ofs = y_encoding.offset; + + assert!(x_ofs <= 0); + assert!(y_ofs <= 0); + assert!(m_encoding.offset <= 0); + + let w = + env.norm_vars + .new_int_var(IntVarRepresentation::Domain(Domain::range_from_checked( + (x_encoding.range.low - x_ofs) * (y_encoding.range.low - y_ofs), + (x_encoding.range.high - x_ofs) * (y_encoding.range.high - y_ofs), + ))); + + let x_lits = x_encoding.lits.clone(); + let y_lits = y_encoding.lits.clone(); + + env.map + .convert_int_var_log_encoding(&env.norm_vars, &mut env.sat, w); + + let w_encoding = env.map.int_map[w] + .as_ref() + .unwrap() + .log_encoding + .as_ref() + .unwrap(); + assert!(w_encoding.offset == 0); + + let w_lits = w_encoding.lits.clone(); + + // w = (x - x_ofs) * (y - y_ofs) + // => m = x * y = w + x_ofs * y + y_ofs * x - x_ofs * y_ofs + let mut linear_sum = LinearSum::new(); + linear_sum.add_coef(m, CheckedInt::new(-1)); + linear_sum.add_coef(w, CheckedInt::new(1)); + linear_sum.add_coef(x, y_ofs); + linear_sum.add_coef(y, x_ofs); + linear_sum.add_constant(-x_ofs * y_ofs); + + let mut clause_set = encode_linear_log(env, &linear_sum, CmpOp::Eq); + + let w_repr_len = w_lits.len(); + let (clause_set2, w_all) = log_encoding_multiplier(env, x_lits, y_lits, w_lits); + + for i in w_repr_len..w_all.len() { + clause_set.push(&[!w_all[i]]); + } + clause_set.append(clause_set2); + + return clause_set; + } - let (mut clause_set, m_all) = log_encoding_multiplier(env, x_repr, y_repr, m_repr); + let m_repr_len = m_encoding.lits.len(); + let (mut clause_set, m_all) = log_encoding_multiplier( + env, + x_encoding.lits.clone(), + y_encoding.lits.clone(), + m_encoding.lits.clone(), + ); for i in m_repr_len..m_all.len() { clause_set.push(&[!m_all[i]]); @@ -795,7 +923,7 @@ mod tests { use super::super::encode_constraint; use super::super::tests::{linear_sum, EncoderTester}; use crate::domain::Domain; - use crate::norm_csp::{Constraint, ExtraConstraint, LinearLit}; + use crate::norm_csp::{BoolLit, Constraint, ExtraConstraint, LinearLit}; #[test] fn test_encode_log_var() { @@ -806,6 +934,124 @@ mod tests { tester.run_check(); } + #[test] + fn test_encode_log_var_with_negative_values() { + let mut tester = EncoderTester::new(); + + let _ = tester.add_int_var_log_encoding(Domain::range(-5, 3)); + + tester.run_check(); + } + + #[test] + fn test_encode_log_var_all_negative() { + let mut tester = EncoderTester::new(); + + let _ = tester.add_int_var_log_encoding(Domain::range(-10, -2)); + + tester.run_check(); + } + + #[test] + fn test_encode_linear_eq_log_encoding_with_negative_values() { + let mut tester = EncoderTester::new(); + + let x = tester.add_int_var_log_encoding(Domain::range(-5, 5)); + let y = tester.add_int_var_log_encoding(Domain::range(-7, 2)); + let z = tester.add_int_var_log_encoding(Domain::range(-1, 8)); + + let lit = LinearLit::new(linear_sum(&[(x, 2), (y, -1), (z, 1)], 3), CmpOp::Eq); + { + let clause_set = encode_linear_log(&mut tester.env(), &lit.sum, CmpOp::Eq); + tester.add_clause_set(clause_set); + } + + tester.add_constraint_linear_lit(lit); + tester.run_check(); + } + + #[test] + fn test_encode_log_var_sparse_domain() { + let mut tester = EncoderTester::new(); + + // Test sparse domain with positive values + let _x = tester.add_int_var_log_encoding(Domain::enumerative(vec![1, 3, 7, 15])); + + tester.run_check(); + } + + #[test] + fn test_encode_log_var_sparse_domain_with_negatives() { + let mut tester = EncoderTester::new(); + + // Test sparse domain with negative and positive values + let _x = tester.add_int_var_log_encoding(Domain::enumerative(vec![-10, -5, 0, 3, 8])); + + tester.run_check(); + } + + #[test] + fn test_encode_log_var_binary() { + let mut tester = EncoderTester::new(); + + // Test binary variable with log encoding + let x = tester.add_bool_var(); + let _a = tester.add_int_var_log_encoding_binary( + BoolLit::new(x, true), + CheckedInt::new(1), + CheckedInt::new(3), + ); + let _b = tester.add_int_var_log_encoding_binary( + BoolLit::new(x, true), + CheckedInt::new(-3), + CheckedInt::new(-1), + ); + let _c = tester.add_int_var_log_encoding_binary( + BoolLit::new(x, true), + CheckedInt::new(-2), + CheckedInt::new(3), + ); + + tester.run_check(); + } + + #[test] + fn test_encode_linear_eq_log_encoding_sparse_domain() { + let mut tester = EncoderTester::new(); + + let x = tester.add_int_var_log_encoding(Domain::enumerative(vec![1, 3, 5, 7])); + let y = tester.add_int_var_log_encoding(Domain::enumerative(vec![2, 4, 6])); + let z = tester.add_int_var_log_encoding(Domain::enumerative(vec![5, 8, 11, 14])); + + // Test linear constraint: x + y = z + let lit = LinearLit::new(linear_sum(&[(x, 1), (y, 1), (z, -1)], 0), CmpOp::Eq); + { + let clause_set = encode_linear_log(&mut tester.env(), &lit.sum, CmpOp::Eq); + tester.add_clause_set(clause_set); + } + + tester.add_constraint_linear_lit(lit); + tester.run_check(); + } + + #[test] + fn test_encode_linear_eq_log_encoding_sparse_domain_with_negatives() { + let mut tester = EncoderTester::new(); + + let x = tester.add_int_var_log_encoding(Domain::enumerative(vec![-5, -2, 1, 4])); + let y = tester.add_int_var_log_encoding(Domain::enumerative(vec![-3, 0, 2])); + + // Test linear constraint: 2*x + y = 0 + let lit = LinearLit::new(linear_sum(&[(x, 2), (y, 1)], 0), CmpOp::Eq); + { + let clause_set = encode_linear_log(&mut tester.env(), &lit.sum, CmpOp::Eq); + tester.add_clause_set(clause_set); + } + + tester.add_constraint_linear_lit(lit); + tester.run_check(); + } + #[test] fn test_encode_linear_eq_log_encoding_1() { let mut tester = EncoderTester::new(); @@ -958,4 +1204,23 @@ mod tests { tester.add_extra_constraint(ExtraConstraint::Mul(x, y, z)); tester.run_check(); } + + #[test] + fn test_encode_mul_log_negative_domain() { + let mut tester = EncoderTester::new(); + + let x = tester.add_int_var_log_encoding(Domain::range(-5, 4)); + let y = tester.add_int_var_log_encoding(Domain::range(-3, 8)); + let z = tester.add_int_var_log_encoding(Domain::enumerative(vec![ + -20, -15, -10, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 15, 24, + ])); + + { + let clause_set = encode_mul_log(&mut tester.env(), x, y, z); + tester.add_clause_set(clause_set); + } + + tester.add_extra_constraint(ExtraConstraint::Mul(x, y, z)); + tester.run_check(); + } } diff --git a/cspuz_core/src/encoder/mod.rs b/cspuz_core/src/encoder/mod.rs index 465c0220..80b3437d 100644 --- a/cspuz_core/src/encoder/mod.rs +++ b/cspuz_core/src/encoder/mod.rs @@ -280,6 +280,8 @@ impl EncodeMap { ) { assert!(self.int_map[var].is_none()); self.int_map[var] = Some(Encoding::log_encoding(log::encode_var_log( + self, + norm_vars, sat, norm_vars.int_var(var), ))); @@ -342,7 +344,7 @@ impl EncodeMap { ret |= 1 << i; } } - Some(CheckedInt::new(ret)) + Some(CheckedInt::new(ret) + encoding.offset) } #[cfg(not(feature = "csp-extra-constraints"))] @@ -1223,6 +1225,28 @@ mod tests { v } + pub fn add_int_var_log_encoding_binary( + &mut self, + cond: BoolLit, + v_false: CheckedInt, + v_true: CheckedInt, + ) -> IntVar { + let v = self + .norm_csp + .vars + .new_int_var(IntVarRepresentation::Binary { + cond, + v_false, + v_true, + }); + self.int_vars.push(v); + + self.map + .convert_int_var_log_encoding(&self.norm_csp.vars, &mut self.sat, v); + + v + } + pub fn enumerate_valid_assignments_by_sat(&mut self) -> Vec<(Vec, Vec)> { let mut sat_vars_set = std::collections::HashSet::new(); for var in &self.bool_vars { diff --git a/cspuz_core/src/integration.rs b/cspuz_core/src/integration.rs index 70d5511e..482996b6 100644 --- a/cspuz_core/src/integration.rs +++ b/cspuz_core/src/integration.rs @@ -1671,6 +1671,13 @@ mod tests { tester.check(); } + #[derive(Debug, PartialEq, Eq, Clone, Copy)] + enum FuzzerLogEncodingMode { + None, + Allow, + Force, + } + struct Fuzzer { random_state: u64, } @@ -1704,9 +1711,11 @@ mod tests { num_int_vars: usize, num_exprs: usize, max_complexity: u32, + log_encoding_mode: FuzzerLogEncodingMode, ) { let mut tester = IntegrationTester::with_config(Config { - use_log_encoding: false, // do not use log encoding because negative numbers are not supported + use_log_encoding: log_encoding_mode != FuzzerLogEncodingMode::None, + force_use_log_encoding: log_encoding_mode == FuzzerLogEncodingMode::Force, ..Config::default() }); @@ -1889,13 +1898,25 @@ mod tests { #[test] fn test_integration_fuzz_quick() { let mut fuzzer = Fuzzer::new(); - for _ in 0..1000 { - let num_bool_vars = fuzzer.next_i32(3, 6) as usize; - let num_int_vars = fuzzer.next_i32(1, 4) as usize; - let num_exprs = fuzzer.next_i32(2, 11) as usize; - let max_complexity = 7; - - fuzzer.run_single_trial(num_bool_vars, num_int_vars, num_exprs, max_complexity); + for (mode, rep) in [ + (FuzzerLogEncodingMode::None, 1000), + (FuzzerLogEncodingMode::Allow, 500), + (FuzzerLogEncodingMode::Force, 100), + ] { + for _ in 0..rep { + let num_bool_vars = fuzzer.next_i32(3, 6) as usize; + let num_int_vars = fuzzer.next_i32(1, 4) as usize; + let num_exprs = fuzzer.next_i32(2, 11) as usize; + let max_complexity = 7; + + fuzzer.run_single_trial( + num_bool_vars, + num_int_vars, + num_exprs, + max_complexity, + mode, + ); + } } } @@ -1903,13 +1924,25 @@ mod tests { #[ignore] // This test can take a long time to run fn test_integration_fuzz_long() { let mut fuzzer = Fuzzer::new(); - for _ in 0..100000 { - let num_bool_vars = fuzzer.next_i32(3, 7) as usize; - let num_int_vars = fuzzer.next_i32(1, 5) as usize; - let num_exprs = fuzzer.next_i32(2, 12) as usize; - let max_complexity = 10; - - fuzzer.run_single_trial(num_bool_vars, num_int_vars, num_exprs, max_complexity); + for (mode, rep) in [ + (FuzzerLogEncodingMode::None, 100000), + (FuzzerLogEncodingMode::Allow, 50000), + (FuzzerLogEncodingMode::Force, 10000), + ] { + for _ in 0..rep { + let num_bool_vars = fuzzer.next_i32(3, 7) as usize; + let num_int_vars = fuzzer.next_i32(1, 5) as usize; + let num_exprs = fuzzer.next_i32(2, 12) as usize; + let max_complexity = 10; + + fuzzer.run_single_trial( + num_bool_vars, + num_int_vars, + num_exprs, + max_complexity, + mode, + ); + } } } }