Skip to content
Merged
Show file tree
Hide file tree
Changes from all 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
56 changes: 56 additions & 0 deletions docs/paper/reductions.typ
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@
// Problem display names for theorem headers
#let display-name = (
"AdditionalKey": [Additional Key],
"AcyclicPartition": [Acyclic Partition],
"MaximumIndependentSet": [Maximum Independent Set],
"MinimumVertexCover": [Minimum Vertex Cover],
"MaxCut": [Max-Cut],
Expand Down Expand Up @@ -3636,6 +3637,61 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76],
]
}

#{
let x = load-model-example("AcyclicPartition")
let nv = x.instance.graph.num_vertices
let arcs = x.instance.graph.arcs.map(a => (a.at(0), a.at(1)))
let weights = x.instance.vertex_weights
let config = x.optimal_config
let B = x.instance.weight_bound
let K = x.instance.cost_bound
let part0 = range(nv).filter(v => config.at(v) == 0)
let part1 = range(nv).filter(v => config.at(v) == 1)
let part2 = range(nv).filter(v => config.at(v) == 2)
let part0w = part0.map(v => weights.at(v)).sum(default: 0)
let part1w = part1.map(v => weights.at(v)).sum(default: 0)
let part2w = part2.map(v => weights.at(v)).sum(default: 0)
let cross-arcs = arcs.filter(a => config.at(a.at(0)) != config.at(a.at(1)))
[
#problem-def("AcyclicPartition")[
Given a directed graph $G = (V, A)$ with vertex weights $w: V -> ZZ^+$, arc costs $c: A -> ZZ^+$, and bounds $B, K in ZZ^+$, determine whether there exists a partition $V = V_1 ∪ dots ∪ V_m$ such that every part satisfies $sum_(v in V_i) w(v) <= B$, the total cost of arcs crossing between different parts is at most $K$, and the quotient digraph on the parts is acyclic.
][
Acyclic Partition is the directed partitioning problem ND15 in Garey & Johnson @garey1979. Unlike ordinary graph partitioning, the goal is not merely to minimize the cut: the partition must preserve a global topological order after every part is contracted to a super-node. This makes the model a natural abstraction for DAG-aware task clustering in compiler scheduling, parallel execution pipelines, and automatic differentiation systems where coarse-grained blocks must still communicate without creating cyclic dependencies.

The implementation uses the natural witness encoding in which each of the $n = #nv$ vertices chooses one of at most $n$ part labels, so direct brute-force search explores $n^n$ assignments.#footnote[Many labelings represent the same unordered partition, but the full configuration space exposed to the solver is still $n^n$.]

*Example.* Consider the six-vertex digraph in the figure with vertex weights $w = (#weights.map(w => str(w)).join(", "))$, part bound $B = #B$, and cut-cost bound $K = #K$. The witness $V_0 = {#part0.map(v => $v_#v$).join(", ")}$, $V_1 = {#part1.map(v => $v_#v$).join(", ")}$, $V_2 = {#part2.map(v => $v_#v$).join(", ")}$ has part weights $#part0w$, $#part1w$, and $#part2w$, so every part respects the weight cap. Exactly #cross-arcs.len() arcs cross between different parts, namely #cross-arcs.map(a => $(v_#(a.at(0)) arrow v_#(a.at(1)))$).join($,$), so the total crossing cost is $#cross-arcs.len() <= K$. These crossings induce quotient arcs $V_0 arrow V_1$, $V_0 arrow V_2$, and $V_1 arrow V_2$, which form a DAG; hence this instance is a YES-instance.

#figure({
let verts = ((0, 1.6), (1.4, 2.4), (1.4, 0.8), (3.2, 2.4), (3.2, 0.8), (4.8, 1.6))
canvas(length: 1cm, {
for arc in arcs {
let (u, v) = arc
let crossing = config.at(u) != config.at(v)
draw.line(
verts.at(u),
verts.at(v),
stroke: if crossing { 1.3pt + black } else { 0.9pt + luma(170) },
mark: (end: "straight", scale: if crossing { 0.5 } else { 0.4 }),
)
}
for (v, pos) in verts.enumerate() {
let color = graph-colors.at(config.at(v))
g-node(
pos,
name: "v" + str(v),
fill: color,
label: text(fill: white)[$v_#v$],
)
}
})
},
caption: [A YES witness for Acyclic Partition. Node colors indicate the parts $V_0$, $V_1$, and $V_2$. Black arcs cross parts and define the quotient DAG $V_0 arrow V_1$, $V_0 arrow V_2$, $V_1 arrow V_2$; gray arcs stay inside a part and therefore do not contribute to the quotient graph.],
) <fig:acyclic-partition>
]
]
}

#{
let x = load-model-example("FlowShopScheduling")
let m = x.instance.num_processors
Expand Down
7 changes: 7 additions & 0 deletions problemreductions-cli/src/cli.rs
Original file line number Diff line number Diff line change
Expand Up @@ -259,6 +259,7 @@ Flags by problem type:
ConsecutiveOnesSubmatrix --matrix (0/1), --k
SteinerTree --graph, --edge-weights, --terminals
MultipleCopyFileAllocation --graph, --usage, --storage, --bound
AcyclicPartition --arcs [--weights] [--arc-costs] --weight-bound --cost-bound [--num-vertices]
CVP --basis, --target-vec [--bounds]
MultiprocessorScheduling --lengths, --num-processors, --deadline
SequencingWithinIntervals --release-times, --deadlines, --lengths
Expand Down Expand Up @@ -506,6 +507,9 @@ pub struct CreateArgs {
/// Upper bound on total path weight
#[arg(long)]
pub weight_bound: Option<i32>,
/// Upper bound on total inter-partition arc cost
#[arg(long)]
pub cost_bound: Option<i32>,
/// Pattern graph edge list for SubgraphIsomorphism (e.g., 0-1,1-2,2-0)
#[arg(long)]
pub pattern: Option<String>,
Expand All @@ -515,6 +519,9 @@ pub struct CreateArgs {
/// Task costs for SequencingToMinimizeMaximumCumulativeCost (comma-separated, e.g., "2,-1,3,-2,1,-3")
#[arg(long, allow_hyphen_values = true)]
pub costs: Option<String>,
/// Arc costs for directed graph problems with per-arc costs (comma-separated, e.g., "1,1,2,3")
#[arg(long)]
pub arc_costs: Option<String>,
/// Directed arcs for directed graph problems (e.g., 0>1,1>2,2>0)
#[arg(long)]
pub arcs: Option<String>,
Expand Down
67 changes: 67 additions & 0 deletions problemreductions-cli/src/commands/create.rs
Original file line number Diff line number Diff line change
Expand Up @@ -100,9 +100,11 @@ fn all_data_flags_empty(args: &CreateArgs) -> bool {
&& args.bound.is_none()
&& args.length_bound.is_none()
&& args.weight_bound.is_none()
&& args.cost_bound.is_none()
&& args.pattern.is_none()
&& args.strings.is_none()
&& args.costs.is_none()
&& args.arc_costs.is_none()
&& args.arcs.is_none()
&& args.quantifiers.is_none()
&& args.usage.is_none()
Expand Down Expand Up @@ -580,6 +582,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str {
"MultipleCopyFileAllocation" => {
MULTIPLE_COPY_FILE_ALLOCATION_EXAMPLE_ARGS
}
"AcyclicPartition" => {
"--arcs \"0>1,0>2,1>3,1>4,2>4,2>5,3>5,4>5\" --weights 2,3,2,1,3,1 --arc-costs 1,1,1,1,1,1,1,1 --weight-bound 5 --cost-bound 5"
}
"OptimalLinearArrangement" => "--graph 0-1,1-2,2-3 --bound 5",
"DirectedTwoCommodityIntegralFlow" => {
"--arcs \"0>2,0>3,1>2,1>3,2>4,2>5,3>4,3>5\" --capacities 1,1,1,1,1,1,1,1 --source-1 0 --sink-1 4 --source-2 1 --sink-2 5 --requirement-1 1 --requirement-2 1"
Expand Down Expand Up @@ -3004,6 +3009,45 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> {
)
}

// AcyclicPartition
"AcyclicPartition" => {
let usage = "Usage: pred create AcyclicPartition/i32 --arcs \"0>1,0>2,1>3,1>4,2>4,2>5,3>5,4>5\" --weights 2,3,2,1,3,1 --arc-costs 1,1,1,1,1,1,1,1 --weight-bound 5 --cost-bound 5";
let arcs_str = args.arcs.as_deref().ok_or_else(|| {
anyhow::anyhow!("AcyclicPartition requires --arcs\n\n{usage}")
})?;
let (graph, num_arcs) = parse_directed_graph(arcs_str, args.num_vertices)?;
let vertex_weights = parse_vertex_weights(args, graph.num_vertices())?;
let arc_costs = parse_arc_costs(args, num_arcs)?;
let weight_bound = args.weight_bound.ok_or_else(|| {
anyhow::anyhow!("AcyclicPartition requires --weight-bound\n\n{usage}")
})?;
let cost_bound = args.cost_bound.ok_or_else(|| {
anyhow::anyhow!("AcyclicPartition requires --cost-bound\n\n{usage}")
})?;
if vertex_weights.iter().any(|&weight| weight <= 0) {
bail!("AcyclicPartition --weights must be positive (Z+)");
}
if arc_costs.iter().any(|&cost| cost <= 0) {
bail!("AcyclicPartition --arc-costs must be positive (Z+)");
}
if weight_bound <= 0 {
bail!("AcyclicPartition --weight-bound must be positive (Z+)");
}
if cost_bound <= 0 {
bail!("AcyclicPartition --cost-bound must be positive (Z+)");
}
(
ser(AcyclicPartition::new(
graph,
vertex_weights,
arc_costs,
weight_bound,
cost_bound,
))?,
resolved_variant.clone(),
)
}

// MinMaxMulticenter (vertex p-center)
"MinMaxMulticenter" => {
let usage = "Usage: pred create MinMaxMulticenter --graph 0-1,1-2,2-3 [--weights 1,1,1,1] [--edge-weights 1,1,1] --k 2 --bound 2";
Expand Down Expand Up @@ -4745,6 +4789,27 @@ fn parse_arc_weights(args: &CreateArgs, num_arcs: usize) -> Result<Vec<i32>> {
}
}

/// Parse `--arc-costs` as per-arc costs (i32), defaulting to all 1s.
fn parse_arc_costs(args: &CreateArgs, num_arcs: usize) -> Result<Vec<i32>> {
match &args.arc_costs {
Some(costs) => {
let parsed: Vec<i32> = costs
.split(',')
.map(|s| s.trim().parse::<i32>())
.collect::<std::result::Result<Vec<_>, _>>()?;
if parsed.len() != num_arcs {
bail!(
"Expected {} arc costs but got {}",
num_arcs,
parsed.len()
);
}
Ok(parsed)
}
None => Ok(vec![1i32; num_arcs]),
}
}

/// Parse `--candidate-arcs` as `u>v:w` entries for StrongConnectivityAugmentation.
fn parse_candidate_arcs(
args: &CreateArgs,
Expand Down Expand Up @@ -5670,8 +5735,10 @@ mod tests {
bound: None,
length_bound: None,
weight_bound: None,
cost_bound: None,
pattern: None,
strings: None,
arc_costs: None,
arcs: None,
values: None,
precedences: None,
Expand Down
153 changes: 153 additions & 0 deletions problemreductions-cli/tests/cli_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1951,6 +1951,100 @@ fn test_create_model_example_multiple_choice_branching_round_trips_into_solve()
std::fs::remove_file(&path).ok();
}

#[test]
fn test_create_acyclic_partition() {
let output = pred()
.args([
"create",
"AcyclicPartition/i32",
"--arcs",
"0>1,0>2,1>3,1>4,2>4,2>5,3>5,4>5",
"--weights",
"2,3,2,1,3,1",
"--arc-costs",
"1,1,1,1,1,1,1,1",
"--weight-bound",
"5",
"--cost-bound",
"5",
])
.output()
.unwrap();
assert!(
output.status.success(),
"stderr: {}",
String::from_utf8_lossy(&output.stderr)
);

let stdout = String::from_utf8(output.stdout).unwrap();
let json: serde_json::Value = serde_json::from_str(&stdout).unwrap();
assert_eq!(json["type"], "AcyclicPartition");
assert_eq!(json["variant"]["weight"], "i32");
assert_eq!(json["data"]["vertex_weights"], serde_json::json!([2, 3, 2, 1, 3, 1]));
assert_eq!(json["data"]["arc_costs"], serde_json::json!([1, 1, 1, 1, 1, 1, 1, 1]));
assert_eq!(json["data"]["weight_bound"], 5);
assert_eq!(json["data"]["cost_bound"], 5);
}

#[test]
fn test_create_model_example_acyclic_partition() {
let output = pred()
.args(["create", "--example", "AcyclicPartition/i32"])
.output()
.unwrap();
assert!(
output.status.success(),
"stderr: {}",
String::from_utf8_lossy(&output.stderr)
);

let stdout = String::from_utf8(output.stdout).unwrap();
let json: serde_json::Value = serde_json::from_str(&stdout).unwrap();
assert_eq!(json["type"], "AcyclicPartition");
assert_eq!(json["variant"]["weight"], "i32");
assert_eq!(json["data"]["weight_bound"], 5);
assert_eq!(json["data"]["cost_bound"], 5);
assert_eq!(json["data"]["graph"]["num_vertices"], 6);
}

#[test]
fn test_create_model_example_acyclic_partition_round_trips_into_solve() {
let path = std::env::temp_dir().join(format!(
"pred_test_model_example_acyclic_partition_{}.json",
std::time::SystemTime::now()
.duration_since(std::time::UNIX_EPOCH)
.unwrap()
.as_nanos()
));
let create = pred()
.args([
"create",
"--example",
"AcyclicPartition/i32",
"-o",
path.to_str().unwrap(),
])
.output()
.unwrap();
assert!(
create.status.success(),
"stderr: {}",
String::from_utf8_lossy(&create.stderr)
);

let solve = pred()
.args(["solve", path.to_str().unwrap(), "--solver", "brute-force"])
.output()
.unwrap();
assert!(
solve.status.success(),
"stderr: {}",
String::from_utf8_lossy(&solve.stderr)
);

std::fs::remove_file(&path).ok();
}

#[test]
fn test_create_multiple_choice_branching_rejects_negative_bound() {
let output = pred()
Expand Down Expand Up @@ -5355,6 +5449,65 @@ fn test_inspect_undirected_two_commodity_integral_flow_reports_size_fields() {
std::fs::remove_file(&result_file).ok();
}

#[test]
fn test_inspect_acyclic_partition_reports_size_fields() {
let problem_file = std::env::temp_dir().join("pred_test_acyclic_partition_inspect_in.json");
let result_file = std::env::temp_dir().join("pred_test_acyclic_partition_inspect_out.json");
let create_out = pred()
.args([
"-o",
problem_file.to_str().unwrap(),
"create",
"--example",
"AcyclicPartition/i32",
])
.output()
.unwrap();
assert!(
create_out.status.success(),
"stderr: {}",
String::from_utf8_lossy(&create_out.stderr)
);

let output = pred()
.args([
"-o",
result_file.to_str().unwrap(),
"inspect",
problem_file.to_str().unwrap(),
])
.output()
.unwrap();
assert!(
output.status.success(),
"stderr: {}",
String::from_utf8_lossy(&output.stderr)
);
assert!(result_file.exists());

let content = std::fs::read_to_string(&result_file).unwrap();
let json: serde_json::Value = serde_json::from_str(&content).unwrap();
let size_fields: Vec<&str> = json["size_fields"]
.as_array()
.expect("size_fields should be an array")
.iter()
.map(|v| v.as_str().unwrap())
.collect();
assert!(
size_fields.contains(&"num_vertices"),
"AcyclicPartition size_fields should contain num_vertices, got: {:?}",
size_fields
);
assert!(
size_fields.contains(&"num_arcs"),
"AcyclicPartition size_fields should contain num_arcs, got: {:?}",
size_fields
);

std::fs::remove_file(&problem_file).ok();
std::fs::remove_file(&result_file).ok();
}

#[test]
fn test_inspect_multiple_copy_file_allocation_reports_size_fields() {
let problem_file = std::env::temp_dir().join("pred_test_mcfa_inspect_in.json");
Expand Down
2 changes: 1 addition & 1 deletion src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ pub mod prelude {
Satisfiability,
};
pub use crate::models::graph::{
BalancedCompleteBipartiteSubgraph, BicliqueCover, BiconnectivityAugmentation,
AcyclicPartition, BalancedCompleteBipartiteSubgraph, BicliqueCover, BiconnectivityAugmentation,
BoundedComponentSpanningForest, DirectedTwoCommodityIntegralFlow, GeneralizedHex,
GraphPartitioning, HamiltonianCircuit, HamiltonianPath, IsomorphicSpanningTree, KClique,
KthBestSpanningTree, LengthBoundedDisjointPaths, SpinGlass, SteinerTree,
Expand Down
Loading
Loading