Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
0dd7448
Add verified direct decision QUBO reduction for integer staff scheduling
isPANN Oct 22, 2026
3d3b020
Tighten direct QUBO bounds and replace costly encodings
isPANN Oct 23, 2026
c6bfae6
Add binary decision ILP to SAT reduction
isPANN Oct 23, 2026
0daa9a8
Fix solution length validation and remove redundant test scaffolding
isPANN Oct 23, 2026
4da646d
Count ILP nonzeros per constraint family instead of rows times columns
isPANN Oct 27, 2026
f95447a
Check ILP nonzero bounds on dense sources
isPANN Oct 27, 2026
4ce1d38
Bound scheduling QUBO sizes by worker bits and start windows
isPANN Oct 27, 2026
0801132
Restate StaffScheduling and SWRTD QUBO sizes in the paper and tests
isPANN Oct 27, 2026
8523caa
Reject negative ConsecutiveOnesSubmatrix bounds at construction
isPANN Oct 27, 2026
3de4a67
Declare exact parameter counts the constructions always produce
isPANN Oct 27, 2026
b8867cf
Keep 3-SAT literal-dependent counts as upper bounds
isPANN Oct 27, 2026
0318bfd
Test exact construction counts on degenerate graphs
isPANN Oct 28, 2026
f7be538
Reduce negative-weight MaxCut to MinimumMatrixCover with an edge gadget
isPANN Oct 28, 2026
ef18c76
Simplify the MaxCut gadget, retype the COS bound, and clean up docs
isPANN Oct 28, 2026
5e512c7
Remove the KSatisfiability KN variant and short-clause constructors
isPANN Oct 28, 2026
86d6808
Declare MonochromaticTriangle counts exact and drop stale short-claus…
isPANN Oct 28, 2026
eafd02a
Bound KSatisfiability by FixedK and tidy the K-SAT reductions
isPANN Oct 28, 2026
3c2f9bd
Drop the FixedK trait
isPANN Oct 28, 2026
9b281d7
Align K3 reduction proofs with exact-width clauses
GiggleLiu Oct 29, 2026
52bd171
Check matrix-cover objective range before reduction
GiggleLiu Oct 29, 2026
3372d66
Merge pull request #1225 from CodingThrust/refactor/remove-ksat-kn
GiggleLiu Oct 29, 2026
5cab940
Merge pull request #1224 from CodingThrust/feat/exact-tight-bounds
GiggleLiu Oct 29, 2026
b4a4e06
Merge pull request #1222 from CodingThrust/fix/ilp-nonzeros-bounds
GiggleLiu Oct 29, 2026
b84842c
Merge pull request #1223 from CodingThrust/fix/qubo-scheduling-bounds
GiggleLiu Oct 29, 2026
2cd3218
Merge pull request #1218 from CodingThrust/feat/binary-ilp-to-sat
GiggleLiu Oct 29, 2026
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
247 changes: 172 additions & 75 deletions docs/paper/reductions.typ

Large diffs are not rendered by default.

11 changes: 11 additions & 0 deletions docs/paper/references.bib
Original file line number Diff line number Diff line change
Expand Up @@ -2332,3 +2332,14 @@ @article{axler2019
year = {2019},
url = {https://www.maths.tcd.ie/EMIS/journals/JIS/VOL22/Axler/axler17.pdf}
}

@article{een2006,
author = {Niklas E{\'e}n and Niklas S{\"o}rensson},
title = {Translating Pseudo-Boolean Constraints into {SAT}},
journal = {Journal on Satisfiability, Boolean Modeling and Computation},
year = {2006},
volume = {2},
number = {1--4},
pages = {1--26},
doi = {10.3233/SAT190014},
}
6 changes: 3 additions & 3 deletions problemreductions-cli/src/cli.rs
Original file line number Diff line number Diff line change
Expand Up @@ -507,17 +507,17 @@ mod tests {
let cli = Cli::try_parse_from([
"pred",
"create",
"3SAT",
"2SAT",
"--num-vars",
"3",
"--clauses",
"1,2,3",
"1,2",
])
.expect("variant alias parses");
let Commands::Create(args) = cli.command else {
panic!("expected create command");
};
assert_eq!(args.problem.as_deref(), Some("KSatisfiability/K3"));
assert_eq!(args.problem.as_deref(), Some("KSatisfiability/K2"));
assert_eq!(args.raw("num-vars"), Some("3"));
}

Expand Down
21 changes: 4 additions & 17 deletions problemreductions-cli/src/commands/create/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -747,7 +747,7 @@ fn test_create_path_constrained_network_flow_rejects_invalid_paths() {
}

#[test]
fn test_create_staff_scheduling_reports_invalid_schedule_without_panic() {
fn test_create_staff_scheduling_rejects_ragged_schedule() {
let cli = Cli::try_parse_from([
"pred",
"create",
Expand Down Expand Up @@ -775,14 +775,7 @@ fn test_create_staff_scheduling_reports_invalid_schedule_without_panic() {
auto_json: false,
};

let result = std::panic::catch_unwind(|| create(&args, &out));
assert!(result.is_ok(), "create should return an error, not panic");
let err = result.unwrap().unwrap_err().to_string();
// parse_bool_rows catches ragged rows before validate_staff_scheduling_args
assert!(
err.contains("All rows") || err.contains("schedule 1 has 6 periods, expected 7"),
"expected row-length validation error, got: {err}"
);
assert!(create(&args, &out).is_err());
}

#[test]
Expand Down Expand Up @@ -955,7 +948,7 @@ fn test_create_timetable_design_outputs_problem_json() {
}

#[test]
fn test_create_timetable_design_reports_invalid_matrix_without_panic() {
fn test_create_timetable_design_rejects_invalid_matrix() {
let cli = Cli::try_parse_from([
"pred",
"create",
Expand Down Expand Up @@ -987,13 +980,7 @@ fn test_create_timetable_design_reports_invalid_matrix_without_panic() {
auto_json: false,
};

let result = std::panic::catch_unwind(|| create(&args, &out));
assert!(result.is_ok(), "create should return an error, not panic");
let err = result.unwrap().unwrap_err().to_string();
assert!(
err.contains("--craftsman-avail"),
"expected timetable matrix validation error, got: {err}"
);
assert!(create(&args, &out).is_err());
}

#[test]
Expand Down
32 changes: 0 additions & 32 deletions problemreductions-macros/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1340,38 +1340,6 @@ mod tests {
assert_eq!(error.to_string(), "duplicate `create` clause");
}

#[test]
fn declare_variants_generates_model_dispatch_without_solver_dispatch() {
let input: DeclareVariantsInput = syn::parse_quote! {
default Foo => "1",
};
let tokens = generate_declare_variants(&input).unwrap().to_string();
assert!(tokens.contains("factory :"), "expected factory field");
assert!(
tokens.contains("serialize_fn :"),
"expected serialize_fn field"
);
assert!(!tokens.contains("solve_typed_fn :"));
assert!(!tokens.contains("solve_fn :"));
assert!(
!tokens.contains("factory : None"),
"factory should not be None"
);
assert!(
!tokens.contains("serialize_fn : None"),
"serialize_fn should not be None"
);
assert!(!tokens.contains("find_cartesian"));
assert!(
!tokens.contains("find_best"),
"did not expect legacy find_best in tokens"
);
assert!(
!tokens.contains("SolutionSize :: Invalid"),
"did not expect legacy invalid fallback in tokens"
);
}

#[test]
fn reduction_rejects_unexpected_attribute() {
let extra_attr = syn::Ident::new("extra", proc_macro2::Span::call_site());
Expand Down
16 changes: 8 additions & 8 deletions src/models/algebraic/consecutive_ones_submatrix.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ inventory::submit! {
description: "Find K columns of a binary matrix that can be permuted to have the consecutive ones property",
fields: &[
FieldInfo { name: "matrix", type_name: "Vec<Vec<bool>>", description: "m×n binary matrix A" },
FieldInfo { name: "bound", type_name: "i64", description: "Required number of columns K" },
FieldInfo { name: "bound", type_name: "usize", description: "Required number of columns K" },
],
}
}
Expand Down Expand Up @@ -62,13 +62,13 @@ inventory::submit! {
#[serde(try_from = "ConsecutiveOnesSubmatrixData")]
pub struct ConsecutiveOnesSubmatrix {
matrix: Vec<Vec<bool>>,
bound: i64,
bound: usize,
}

#[derive(Deserialize)]
struct ConsecutiveOnesSubmatrixData {
matrix: Vec<Vec<bool>>,
bound: i64,
bound: usize,
}

impl TryFrom<ConsecutiveOnesSubmatrixData> for ConsecutiveOnesSubmatrix {
Expand All @@ -85,19 +85,19 @@ impl ConsecutiveOnesSubmatrix {
/// # Panics
///
/// Panics if `bound > n`, or if rows have inconsistent lengths.
pub fn new(matrix: Vec<Vec<bool>>, bound: i64) -> Self {
pub fn new(matrix: Vec<Vec<bool>>, bound: usize) -> Self {
Self::try_new(matrix, bound).unwrap_or_else(|error| panic!("{error}"))
}

fn try_new(
matrix: Vec<Vec<bool>>,
bound: i64,
bound: usize,
) -> Result<Self, crate::registry::ConstructionError> {
let n = matrix.first().map_or(0, Vec::len);
if matrix.iter().any(|row| row.len() != n) {
return Err("all matrix rows must have the same length".into());
}
if !(bound < 0 || usize::try_from(bound).is_ok_and(|bound| bound <= n)) {
if bound > n {
return Err(format!("bound ({bound}) must be <= number of columns ({n})").into());
}
Ok(Self { matrix, bound })
Expand All @@ -109,7 +109,7 @@ impl ConsecutiveOnesSubmatrix {
}

/// Returns the bound (the required number of columns).
pub fn bound(&self) -> i64 {
pub fn bound(&self) -> usize {
self.bound
}

Expand Down Expand Up @@ -222,7 +222,7 @@ impl Problem for ConsecutiveOnesSubmatrix {
.filter(|(_, &v)| v)
.map(|(i, _)| i)
.collect();
if usize::try_from(self.bound) != Ok(selected.len()) {
if self.bound != selected.len() {
return Ok(crate::types::Or(false));
}
self.any_permutation_has_c1p(&selected)
Expand Down
46 changes: 46 additions & 0 deletions src/models/algebraic/ilp.rs
Original file line number Diff line number Diff line change
Expand Up @@ -690,9 +690,41 @@ crate::declare_variants! {
ILP<i64, f64> => "num_vars^num_vars",
}

impl crate::solvers::BruteForceProblem for ILP<bool> {
fn dimensions(&self) -> Vec<usize> {
vec![2; self.num_vars()]
}
}

crate::decision_problem_meta!(ILP<bool>, "DecisionILP");
crate::register_decision_variant!(without_turing;
ILP<bool>, "DecisionILP", "2^num_vars", &[],
"Does a binary ILP have a feasible solution meeting its objective bound?",
category: crate::registry::ProblemCategory::Algebraic,
dims: [
VariantDimension::new("variable", "bool", &["bool"]),
VariantDimension::new("coefficient", "i64", &["i64"]),
VariantDimension::new("bounds", "general", &["general"]),
],
fields: [
FieldInfo { name: "variables", type_name: "Vec<IntegerVariable>", description: "Binary variable bounds [0, 1]" },
FieldInfo { name: "constraints", type_name: "Vec<LinearConstraint<i64>>", description: "Sparse integer linear constraints" },
FieldInfo { name: "objective", type_name: "Vec<(usize, i64)>", description: "Sparse integer objective coefficients" },
FieldInfo { name: "sense", type_name: "ObjectiveSense", description: "Optimization direction" },
FieldInfo { name: "bound", type_name: "i64", description: "Upper bound for minimization, lower bound for maximization" },
],
decode: |_, indices: Vec<usize>| indices.into_iter().map(|bit| i64::try_from(bit).expect("binary coordinate fits i64")).collect::<Vec<_>>()
);

#[cfg(feature = "example-db")]
pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
vec![
crate::example_db::specs::ModelExampleSpec {
id: "decision_ilp",
instance: Box::new(canonical_decision_example()),
optimal_config: serde_json::json!([0, 0, 1]),
optimal_value: serde_json::json!(true),
},
crate::example_db::specs::ModelExampleSpec {
id: "ilp",
instance: Box::new(
Expand Down Expand Up @@ -733,3 +765,17 @@ pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::M
#[cfg(test)]
#[path = "../../unit_tests/models/algebraic/ilp.rs"]
mod tests;

#[cfg(feature = "example-db")]
pub(crate) fn canonical_decision_example() -> crate::models::Decision<ILP<bool>> {
crate::models::Decision::new(
ILP::new(
3,
vec![LinearConstraint::eq(vec![(0, 1), (1, 1), (2, 1)], 1)],
vec![(0, 3), (1, 2), (2, 1)],
ObjectiveSense::Minimize,
)
.unwrap(),
1,
)
}
18 changes: 14 additions & 4 deletions src/models/decision.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,16 @@ macro_rules! decision_problem_meta {
/// variant's construction fields and decoder without adding another schema or default.
/// Both decision/optimization edges derive their identity parameter transforms directly
/// from the inner problem's canonical parameter schema.
/// Prefix with `without_turing;` to omit the reverse optimization-to-decision Turing edge.
#[macro_export]
macro_rules! register_decision_variant {
(
(without_turing; $($body:tt)*) => {
$crate::register_decision_variant!(@register witness_edge; $($body)*);
};
($inner:ty, $($body:tt)*) => {
$crate::register_decision_variant!(@register edges; $inner, $($body)*);
};
(@register $edges:ident;
$inner:ty,
$name:literal,
$complexity:literal,
Expand Down Expand Up @@ -61,16 +68,16 @@ macro_rules! register_decision_variant {
}
}

$crate::register_decision_variant!(@edges $inner, $name);
$crate::register_decision_variant!(@$edges $inner, $name);
$($(
$crate::register_brute_force! {
$crate::models::decision::Decision<$additional> decode $decoder,
}
$crate::register_decision_variant!(@edges $additional, $name);
$crate::register_decision_variant!(@$edges $additional, $name);
)*)?
};

(@edges $inner:ty, $name:literal) => {
(@witness_edge $inner:ty, $name:literal) => {
// Decision<P> → P: both witness (identity config) and aggregate (solve + compare)
$crate::inventory::submit! {
$crate::rules::ReductionEntry {
Expand Down Expand Up @@ -114,7 +121,10 @@ macro_rules! register_decision_variant {
turing: false,
}
}
};

(@edges $inner:ty, $name:literal) => {
$crate::register_decision_variant!(@witness_edge $inner, $name);
// Reverse edge: P → Decision<P> (Turing/multi-query reduction via binary search)
$crate::inventory::submit! {
$crate::rules::ReductionEntry {
Expand Down
Loading