Skip to content
Draft
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions cspuz_core/src/config.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ pub struct Config {
pub force_use_log_encoding: bool,
pub use_native_extension_supports: bool,
pub direct_encoding_for_binary_vars: bool,
pub encoding_domain_threshold: usize,
pub merge_equivalent_variables: bool,
pub alldifferent_bijection_constraints: bool,
pub glucose_random_seed: Option<f64>,
Expand Down Expand Up @@ -53,6 +54,7 @@ impl Config {
force_use_log_encoding: false,
use_native_extension_supports: false,
direct_encoding_for_binary_vars: false,
encoding_domain_threshold: 500,
merge_equivalent_variables: false,
alldifferent_bijection_constraints: false,
glucose_random_seed: None,
Expand Down Expand Up @@ -156,6 +158,7 @@ impl Config {
opts.optopt("", "domain-product-threshold", "Specify the threshold of domain product for introducing an auxiliary variable by Tseitin transformation.", "THRESHOLD");
opts.optopt("", "native-linear-encoding-terms", "Specify the maximum number of terms in a linear sum which is encoded by the native linear constraint (0 for disabling this).", "TERMS");
opts.optopt("", "native-linear-encoding-domain-product", "Specify the minimum domain product of linear sums which are encoded by the native linear constraint.", "DOMAIN_PRODUCT");
opts.optopt("", "encoding-domain-threshold", "Specify the domain size threshold for choosing encoding schemes (direct vs order vs log).", "THRESHOLD");

opts.optopt("", "backend", "Specify the SAT backend", "BACKEND");
opts.optopt(
Expand Down Expand Up @@ -236,6 +239,19 @@ impl Config {
};
config.native_linear_encoding_domain_product_threshold = v;
}
if let Some(s) = matches.opt_str("encoding-domain-threshold") {
let v = match s.parse::<usize>() {
Ok(v) => v,
Err(f) => {
println!(
"error: parse failed for --encoding-domain-threshold: {}",
f,
);
std::process::exit(1);
}
};
config.encoding_domain_threshold = v;
}
if let Some(s) = matches.opt_str("backend") {
if s == "glucose" {
config.backend = Backend::Glucose;
Expand Down
18 changes: 15 additions & 3 deletions cspuz_core/src/encoder/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -597,8 +597,7 @@ fn decide_encode_schemes(
for &var in new_vars {
let repr = norm_vars.int_var(var);
if let IntVarRepresentation::Domain(domain) = repr {
if domain.num_candidates() > 500 && complex_constraints_vars.contains(&var) {
// TODO: make this configurable
if domain.num_candidates() > config.encoding_domain_threshold && complex_constraints_vars.contains(&var) {

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

make it clear that this config is related to log encoding

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in commit a661300. Renamed the config field to log_encoding_domain_threshold and updated CLI option to --log-encoding-domain-threshold to make it clear this config is specifically for log encoding decisions.

scheme.insert(var, EncodeScheme::Log);
}
}
Expand Down Expand Up @@ -688,7 +687,7 @@ fn decide_encode_schemes(
for &var in &direct_encoding_vars {
let repr = norm_vars.int_var(var);
let use_direct_encoding = match repr {
IntVarRepresentation::Domain(domain) => domain.num_candidates() <= 500,
IntVarRepresentation::Domain(domain) => domain.num_candidates() <= config.encoding_domain_threshold,

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this threshold 500 is not related

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in commit a661300. Reverted this threshold back to the hardcoded value of 500, as you're correct - this threshold for direct encoding is conceptually different from the log encoding threshold and should not share the same configuration.

_ => true,
};
if use_direct_encoding {
Expand Down Expand Up @@ -1564,4 +1563,17 @@ mod tests {
}
}
}

#[test]
fn test_encoding_domain_threshold_configurable() {
let mut config = Config::default();
assert_eq!(config.encoding_domain_threshold, 500); // default value

config.encoding_domain_threshold = 1000;
assert_eq!(config.encoding_domain_threshold, 1000); // changed value

// Test that the field exists and can be modified
config.encoding_domain_threshold = 100;
assert_eq!(config.encoding_domain_threshold, 100);
}
}