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
51 changes: 51 additions & 0 deletions docs/paper/reductions.typ
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,7 @@
"KSatisfiability": [$k$-SAT],
"CircuitSAT": [CircuitSAT],
"ConjunctiveQueryFoldability": [Conjunctive Query Foldability],
"EnsembleComputation": [Ensemble Computation],
"Factoring": [Factoring],
"KingsSubgraph": [King's Subgraph MIS],
"TriangularSubgraph": [Triangular Subgraph MIS],
Expand Down Expand Up @@ -2627,6 +2628,56 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76],
) <fig:cqf-example>
]

#problem-def("EnsembleComputation")[
Given a finite set $A$, a collection $C$ of subsets of $A$, and a positive integer $J$, determine whether there exists a sequence $S = (z_1 <- x_1 union y_1, z_2 <- x_2 union y_2, dots, z_j <- x_j union y_j)$ of $j <= J$ union operations such that each operand $x_i, y_i$ is either a singleton ${a}$ for some $a in A$ or a previously computed set $z_k$ with $k < i$, the two operands are disjoint for every step, and every target subset $c in C$ is equal to some computed set $z_i$.
][
Ensemble Computation is problem PO9 in Garey and Johnson @garey1979. It can be viewed as monotone circuit synthesis over set union: each operation introduces one reusable intermediate set, and the objective is simply to realize all targets within the given budget. The implementation in this library uses $2J$ operand variables with domain size $|A| + J$ and accepts as soon as some valid prefix has produced every target set, so the original "$j <= J$" semantics are preserved under brute-force enumeration. The resulting search space yields a straightforward exact upper bound of $(|A| + J)^(2J)$. Järvisalo, Kaski, Koivisto, and Korhonen study SAT encodings for finding efficient ensemble computations in a monotone-circuit setting @jarvisalo2012.

*Example.* Let $A = {0, 1, 2, 3}$, $C = {{0, 1, 2}, {0, 1, 3}}$, and $J = 4$. A satisfying witness uses three essential unions:
$z_1 = {0} union {1} = {0, 1}$,
$z_2 = z_1 union {2} = {0, 1, 2}$, and
$z_3 = z_1 union {3} = {0, 1, 3}$.
Thus both target subsets appear among the computed $z_i$ values while staying within the budget.

#figure(
canvas(length: 1cm, {
import draw: *
let node(pos, label, name, fill) = {
rect(
(pos.at(0) - 0.45, pos.at(1) - 0.18),
(pos.at(0) + 0.45, pos.at(1) + 0.18),
radius: 0.08,
fill: fill,
stroke: 0.5pt + luma(140),
name: name,
)
content(name, text(7pt, label))
}

let base = rgb("#4e79a7").transparentize(78%)
let target = rgb("#59a14f").transparentize(72%)
let aux = rgb("#f28e2b").transparentize(74%)

node((0.0, 1.4), [\{0\}], "a0", base)
node((1.2, 1.4), [\{1\}], "a1", base)
node((2.4, 1.4), [\{2\}], "a2", base)
node((3.6, 1.4), [\{3\}], "a3", base)

node((0.6, 0.6), [$z_1 = \{0,1\}$], "z1", aux)
node((1.8, -0.2), [$z_2 = \{0,1,2\}$], "z2", target)
node((3.0, -0.2), [$z_3 = \{0,1,3\}$], "z3", target)

line("a0.south", "z1.north-west", stroke: 0.5pt + luma(120), mark: (end: "straight", scale: 0.4))
line("a1.south", "z1.north-east", stroke: 0.5pt + luma(120), mark: (end: "straight", scale: 0.4))
line("z1.south-west", "z2.north-west", stroke: 0.5pt + luma(120), mark: (end: "straight", scale: 0.4))
line("a2.south", "z2.north-east", stroke: 0.5pt + luma(120), mark: (end: "straight", scale: 0.4))
line("z1.south-east", "z3.north-west", stroke: 0.5pt + luma(120), mark: (end: "straight", scale: 0.4))
line("a3.south", "z3.north-east", stroke: 0.5pt + luma(120), mark: (end: "straight", scale: 0.4))
}),
caption: [An ensemble computation for $A = {0,1,2,3}$ and $C = {{0,1,2}, {0,1,3}}$. The intermediate set $z_1 = {0,1}$ is reused to produce both target subsets.],
) <fig:ensemble-computation>
]

#{
let x = load-model-example("Factoring")
let N = x.instance.target
Expand Down
12 changes: 12 additions & 0 deletions docs/paper/references.bib
Original file line number Diff line number Diff line change
Expand Up @@ -504,6 +504,18 @@ @article{bjorklund2009
doi = {10.1137/070683933}
}

@incollection{jarvisalo2012,
author = {Matti J\"{a}rvisalo and Petteri Kaski and Mikko Koivisto and Janne H. Korhonen},
title = {Finding Efficient Circuits for Ensemble Computation},
booktitle = {Theory and Applications of Satisfiability Testing -- SAT 2012},
series = {Lecture Notes in Computer Science},
volume = {7317},
pages = {369--382},
year = {2012},
publisher = {Springer},
doi = {10.1007/978-3-642-31612-8_28}
}

@article{aspvall1979,
author = {Bengt Aspvall and Michael F. Plass and Robert Endre Tarjan},
title = {A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas},
Expand Down
1 change: 1 addition & 0 deletions problemreductions-cli/src/cli.rs
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,7 @@ Flags by problem type:
MaximumSetPacking --sets [--weights]
MinimumHittingSet --universe, --sets
MinimumSetCovering --universe, --sets [--weights]
EnsembleComputation --universe, --sets, --budget
ComparativeContainment --universe, --r-sets, --s-sets [--r-weights] [--s-weights]
X3C (ExactCoverBy3Sets) --universe, --sets (3 elements each)
SetBasis --universe, --sets, --k
Expand Down
64 changes: 61 additions & 3 deletions problemreductions-cli/src/commands/create.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,9 @@ use problemreductions::models::graph::{
};
use problemreductions::models::misc::{
AdditionalKey, BinPacking, BoyceCoddNormalFormViolation, CbqRelation, ConjunctiveBooleanQuery,
ConsistencyOfDatabaseFrequencyTables, FlowShopScheduling, FrequencyTable, KnownValue,
LongestCommonSubsequence, MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop,
PartiallyOrderedKnapsack, QueryArg, RectilinearPictureCompression,
ConsistencyOfDatabaseFrequencyTables, EnsembleComputation, FlowShopScheduling, FrequencyTable,
KnownValue, LongestCommonSubsequence, MinimumTardinessSequencing, MultiprocessorScheduling,
PaintShop, PartiallyOrderedKnapsack, QueryArg, RectilinearPictureCompression,
ResourceConstrainedScheduling, SchedulingWithIndividualDeadlines,
SequencingToMinimizeMaximumCumulativeCost, SequencingToMinimizeWeightedCompletionTime,
SequencingToMinimizeWeightedTardiness, SequencingWithReleaseTimesAndDeadlines,
Expand Down Expand Up @@ -498,6 +498,7 @@ fn type_format_hint(type_name: &str, graph_type: Option<&str>) -> &'static str {

fn cli_flag_name(field_name: &str) -> String {
match field_name {
"universe_size" => "universe".to_string(),
"vertex_weights" => "weights".to_string(),
"edge_lengths" => "edge-weights".to_string(),
_ => field_name.replace('_', "-"),
Expand Down Expand Up @@ -554,6 +555,7 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str {
"SpinGlass" => "--graph 0-1,1-2 --couplings 1,1",
"KColoring" => "--graph 0-1,1-2,2-0 --k 3",
"HamiltonianCircuit" => "--graph 0-1,1-2,2-3,3-0",
"EnsembleComputation" => "--universe 4 --sets \"0,1,2;0,1,3\" --budget 4",
"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 @@ -1992,6 +1994,31 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> {
)
}

// EnsembleComputation
"EnsembleComputation" => {
let usage =
"Usage: pred create EnsembleComputation --universe 4 --sets \"0,1,2;0,1,3\" --budget 4";
let universe_size = args.universe.ok_or_else(|| {
anyhow::anyhow!("EnsembleComputation requires --universe\n\n{usage}")
})?;
let subsets = parse_sets(args)?;
let budget = args
.budget
.as_deref()
.ok_or_else(|| anyhow::anyhow!("EnsembleComputation requires --budget\n\n{usage}"))?
.parse::<usize>()
.map_err(|e| {
anyhow::anyhow!(
"Invalid --budget value for EnsembleComputation: {e}\n\n{usage}"
)
})?;
(
ser(EnsembleComputation::try_new(universe_size, subsets, budget)
.map_err(anyhow::Error::msg)?)?,
resolved_variant.clone(),
)
}

// ComparativeContainment
"ComparativeContainment" => {
let universe = args.universe.ok_or_else(|| {
Expand Down Expand Up @@ -5826,6 +5853,37 @@ mod tests {
std::fs::remove_file(output_path).ok();
}

#[test]
fn test_create_ensemble_computation_json() {
let mut args = empty_args();
args.problem = Some("EnsembleComputation".to_string());
args.universe = Some(4);
args.sets = Some("0,1,2;0,1,3".to_string());
args.budget = Some("4".to_string());

let output_path = std::env::temp_dir().join("pred_test_create_ensemble_computation.json");
let out = OutputConfig {
output: Some(output_path.clone()),
quiet: true,
json: false,
auto_json: false,
};

create(&args, &out).unwrap();

let content = std::fs::read_to_string(&output_path).unwrap();
let json: serde_json::Value = serde_json::from_str(&content).unwrap();
assert_eq!(json["type"], "EnsembleComputation");
assert_eq!(json["data"]["universe_size"], 4);
assert_eq!(
json["data"]["subsets"],
serde_json::json!([[0, 1, 2], [0, 1, 3]])
);
assert_eq!(json["data"]["budget"], 4);

std::fs::remove_file(output_path).ok();
}

#[test]
fn test_create_balanced_complete_bipartite_subgraph() {
use crate::dispatch::ProblemJsonOutput;
Expand Down
107 changes: 107 additions & 0 deletions problemreductions-cli/tests/cli_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7335,6 +7335,97 @@ fn test_create_sequencing_within_intervals() {
std::fs::remove_file(&output_file).ok();
}

#[test]
fn test_create_ensemble_computation() {
let output_file = std::env::temp_dir().join("pred_test_create_ensemble_computation.json");
let output = pred()
.args([
"-o",
output_file.to_str().unwrap(),
"create",
"EnsembleComputation",
"--universe",
"4",
"--sets",
"0,1,2;0,1,3",
"--budget",
"4",
])
.output()
.unwrap();
assert!(
output.status.success(),
"stderr: {}",
String::from_utf8_lossy(&output.stderr)
);
let content = std::fs::read_to_string(&output_file).unwrap();
let json: serde_json::Value = serde_json::from_str(&content).unwrap();
assert_eq!(json["type"], "EnsembleComputation");
assert_eq!(json["data"]["universe_size"], 4);
assert_eq!(
json["data"]["subsets"],
serde_json::json!([[0, 1, 2], [0, 1, 3]])
);
assert_eq!(json["data"]["budget"], 4);
std::fs::remove_file(&output_file).ok();
}

#[test]
fn test_create_ensemble_computation_no_flags_uses_cli_flag_names() {
let output = pred()
.args(["create", "EnsembleComputation"])
.output()
.unwrap();
assert!(
!output.status.success(),
"problem-specific help should exit non-zero"
);
let stderr = String::from_utf8_lossy(&output.stderr);
assert!(
stderr.contains("--universe"),
"expected --universe in help, got: {stderr}"
);
assert!(
stderr.contains("--sets"),
"expected --sets in help, got: {stderr}"
);
assert!(
stderr.contains("--budget"),
"expected --budget in help, got: {stderr}"
);
assert!(
!stderr.contains("--universe-size"),
"help should use actual CLI flags, got: {stderr}"
);
}

#[test]
fn test_create_ensemble_computation_rejects_out_of_range_elements_without_panicking() {
let output = pred()
.args([
"create",
"EnsembleComputation",
"--universe",
"4",
"--sets",
"0,1,5",
"--budget",
"4",
])
.output()
.unwrap();
assert!(!output.status.success());
let stderr = String::from_utf8_lossy(&output.stderr);
assert!(
!stderr.contains("panicked at"),
"expected graceful CLI error, got panic: {stderr}"
);
assert!(
stderr.contains("outside universe") || stderr.contains("universe of size"),
"expected out-of-range subset error, got: {stderr}"
);
}

#[test]
fn test_create_scheduling_with_individual_deadlines_with_m_alias() {
let output_file =
Expand Down Expand Up @@ -7483,6 +7574,22 @@ fn test_create_model_example_sequencing_within_intervals() {
assert_eq!(json["type"], "SequencingWithinIntervals");
}

#[test]
fn test_create_model_example_ensemble_computation() {
let output = pred()
.args(["create", "--example", "EnsembleComputation"])
.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"], "EnsembleComputation");
}

#[test]
fn test_create_minimum_multiway_cut_rejects_single_terminal() {
let output = pred()
Expand Down
2 changes: 1 addition & 1 deletion src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ pub mod prelude {
pub use crate::models::misc::{
AdditionalKey, BinPacking, BoyceCoddNormalFormViolation, CbqRelation,
ConjunctiveBooleanQuery, ConjunctiveQueryFoldability, ConsistencyOfDatabaseFrequencyTables,
Factoring, FlowShopScheduling, Knapsack, LongestCommonSubsequence,
EnsembleComputation, Factoring, FlowShopScheduling, Knapsack, LongestCommonSubsequence,
MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, Partition, QueryArg,
RectilinearPictureCompression, ResourceConstrainedScheduling,
SchedulingWithIndividualDeadlines, SequencingToMinimizeMaximumCumulativeCost,
Expand Down
Loading
Loading