Skip to content

Commit b4a2c62

Browse files
isPANNclaude
andauthored
feat: add IntegerExpressionMembership model (#552) (#814)
* feat: add IntegerExpressionMembership model (#552) Add the Integer Expression Membership problem: given a recursive integer expression tree over union and Minkowski sum operations on singleton positive integers, and a target K, decide whether K belongs to the set represented by the expression. Includes model, tests, CLI support, canonical example, and paper entry. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * Fix agentic review issues: overflow safety, positive-integer validation - Use checked_add for u64 addition to prevent overflow panic (evaluates to Or(false) on overflow instead of crashing) - Validate all Atom values > 0 and target > 0 in constructor - Add CLI-side validation with clean error messages - Add boundary tests: overflow safety, zero atom/target rejection Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent f3837e2 commit b4a2c62

7 files changed

Lines changed: 635 additions & 14 deletions

File tree

docs/paper/reductions.typ

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -164,6 +164,7 @@
164164
"FlowShopScheduling": [Flow Shop Scheduling],
165165
"JobShopScheduling": [Job-Shop Scheduling],
166166
"GroupingBySwapping": [Grouping by Swapping],
167+
"IntegerExpressionMembership": [Integer Expression Membership],
167168
"MinimumCutIntoBoundedSets": [Minimum Cut Into Bounded Sets],
168169
"MinimumDummyActivitiesPert": [Minimum Dummy Activities in PERT Networks],
169170
"MinimumSumMulticenter": [Minimum Sum Multicenter],
@@ -6810,6 +6811,69 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76],
68106811
]
68116812
}
68126813

6814+
#{
6815+
let x = load-model-example("IntegerExpressionMembership")
6816+
[
6817+
#problem-def("IntegerExpressionMembership")[
6818+
Given a recursive integer expression $e$ over union ($union$) and Minkowski sum ($+$) operations on singleton positive integers, and a target $K in NN^+$, determine whether $K in "eval"(e)$, where $"eval"("Atom"(n)) = \{n\}$, $"eval"(F union G) = "eval"(F) union "eval"(G)$, and $"eval"(F + G) = \{m + n : m in "eval"(F), n in "eval"(G)\}$.
6819+
][
6820+
Integer Expression Membership asks whether a specific integer is reachable by selecting one branch at each union node in a recursive expression tree. Each configuration assigns a binary choice (left or right) at every union node in depth-first order; with all unions resolved, the expression reduces to a chain of sums and atoms that evaluates to a single integer.#footnote[No algorithm improving on brute-force enumeration of all $2^u$ union-branch combinations (where $u$ is the number of union nodes) is known for the general case.]
6821+
6822+
*Example.* Consider $e = (1 union 4) + (3 union 6) + (2 union 5)$ with $K = 12$. There are $u = 3$ union nodes, giving $2^3 = 8$ configurations. The reachable set is $\{6, 9, 12, 15\}$. Since $12 in \{6, 9, 12, 15\}$, the answer is YES. One witness: choose right ($4$), right ($6$), left ($2$) at the three union nodes, giving $4 + 6 + 2 = 12 = K$.
6823+
6824+
#pred-commands(
6825+
"pred create --example " + problem-spec(x) + " -o iem.json",
6826+
"pred solve iem.json --solver brute-force",
6827+
"pred evaluate iem.json --config " + x.optimal_config.map(str).join(","),
6828+
)
6829+
6830+
#figure(
6831+
canvas(length: 0.7cm, {
6832+
import draw: *
6833+
// Draw expression tree: Sum( Sum( Union(1,4), Union(3,6) ), Union(2,5) )
6834+
let node-r = 0.45
6835+
let level-gap = 1.5
6836+
let spread = 2.0
6837+
// Root: Sum (level 0)
6838+
circle((0, 0), radius: node-r, name: "root", fill: rgb("#e8f0fe"))
6839+
content("root", text(8pt, $+$))
6840+
// Left child: Sum (level 1)
6841+
circle((-spread, -level-gap), radius: node-r, name: "lsum", fill: rgb("#e8f0fe"))
6842+
content("lsum", text(8pt, $+$))
6843+
line("root.south-west", "lsum.north", mark: (end: "straight"))
6844+
// Right child: Union (level 1)
6845+
circle((spread, -level-gap), radius: node-r, name: "ru", fill: rgb("#fce8e6"))
6846+
content("ru", text(8pt, $union$))
6847+
line("root.south-east", "ru.north", mark: (end: "straight"))
6848+
// Left-Left: Union (level 2)
6849+
circle((-spread - 1.2, -2 * level-gap), radius: node-r, name: "llu", fill: rgb("#fce8e6"))
6850+
content("llu", text(8pt, $union$))
6851+
line("lsum.south-west", "llu.north", mark: (end: "straight"))
6852+
// Left-Right: Union (level 2)
6853+
circle((-spread + 1.2, -2 * level-gap), radius: node-r, name: "lru", fill: rgb("#fce8e6"))
6854+
content("lru", text(8pt, $union$))
6855+
line("lsum.south-east", "lru.north", mark: (end: "straight"))
6856+
// Leaves (level 3)
6857+
let leaf-spread = 0.7
6858+
for (parent, vals, xoff) in (
6859+
("llu", (1, 4), -spread - 1.2),
6860+
("lru", (3, 6), -spread + 1.2),
6861+
("ru", (2, 5), spread),
6862+
) {
6863+
circle((xoff - leaf-spread, -3 * level-gap), radius: node-r, name: parent + "l", fill: rgb("#e6f4ea"))
6864+
content(parent + "l", text(8pt, str(vals.at(0))))
6865+
line(parent + ".south-west", (parent + "l") + ".north", mark: (end: "straight"))
6866+
circle((xoff + leaf-spread, -3 * level-gap), radius: node-r, name: parent + "r", fill: rgb("#e6f4ea"))
6867+
content(parent + "r", text(8pt, str(vals.at(1))))
6868+
line(parent + ".south-east", (parent + "r") + ".north", mark: (end: "straight"))
6869+
}
6870+
}),
6871+
caption: [Expression tree $e = (1 union 4) + (3 union 6) + (2 union 5)$ with target $K = 12$. Blue nodes are sums ($+$), red nodes are unions ($union$), green leaves are atoms. Choosing right at the first two unions and left at the third yields $4 + 6 + 2 = 12$.],
6872+
) <fig:integer-expression-membership>
6873+
]
6874+
]
6875+
}
6876+
68136877
#{
68146878
let x = load-model-example("FeasibleBasisExtension")
68156879
let A = x.instance.matrix

problemreductions-cli/src/cli.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -319,6 +319,7 @@ Flags by problem type:
319319
D2CIF --arcs, --capacities, --source-1, --sink-1, --source-2, --sink-2, --requirement-1, --requirement-2
320320
MinimumDummyActivitiesPert --arcs [--num-vertices]
321321
CBQ --domain-size, --relations, --conjuncts-spec
322+
IntegerExpressionMembership --expression (JSON), --target
322323
ILP, CircuitSAT (via reduction only)
323324
324325
Geometry graph variants (use slash notation, e.g., MIS/KingsSubgraph):
@@ -758,6 +759,9 @@ pub struct CreateArgs {
758759
/// Target string for StringToStringCorrection (comma-separated symbol indices, e.g., "0,1,3,2")
759760
#[arg(long)]
760761
pub target_string: Option<String>,
762+
/// Expression tree for IntegerExpressionMembership (JSON, e.g., '{"Sum":[{"Atom":1},{"Atom":2}]}')
763+
#[arg(long)]
764+
pub expression: Option<String>,
761765
/// Coefficient a for QuadraticDiophantineEquations (coefficient of x²)
762766
#[arg(long)]
763767
pub coeff_a: Option<u64>,

problemreductions-cli/src/commands/create.rs

Lines changed: 42 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -23,15 +23,15 @@ use problemreductions::models::graph::{
2323
use problemreductions::models::misc::{
2424
AdditionalKey, BinPacking, BoyceCoddNormalFormViolation, CapacityAssignment, CbqRelation,
2525
ConjunctiveBooleanQuery, ConsistencyOfDatabaseFrequencyTables, EnsembleComputation,
26-
ExpectedRetrievalCost, FlowShopScheduling, FrequencyTable, GroupingBySwapping,
27-
JobShopScheduling, KnownValue, KthLargestMTuple, LongestCommonSubsequence,
28-
MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, PartiallyOrderedKnapsack,
29-
ProductionPlanning, QueryArg, RectilinearPictureCompression, ResourceConstrainedScheduling,
30-
SchedulingToMinimizeWeightedCompletionTime, SchedulingWithIndividualDeadlines,
31-
SequencingToMinimizeMaximumCumulativeCost, SequencingToMinimizeWeightedCompletionTime,
32-
SequencingToMinimizeWeightedTardiness, SequencingWithReleaseTimesAndDeadlines,
33-
SequencingWithinIntervals, ShortestCommonSupersequence, StringToStringCorrection, SubsetSum,
34-
SumOfSquaresPartition, ThreePartition, TimetableDesign,
26+
ExpectedRetrievalCost, FlowShopScheduling, FrequencyTable, GroupingBySwapping, IntExpr,
27+
IntegerExpressionMembership, JobShopScheduling, KnownValue, KthLargestMTuple,
28+
LongestCommonSubsequence, MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop,
29+
PartiallyOrderedKnapsack, ProductionPlanning, QueryArg, RectilinearPictureCompression,
30+
ResourceConstrainedScheduling, SchedulingToMinimizeWeightedCompletionTime,
31+
SchedulingWithIndividualDeadlines, SequencingToMinimizeMaximumCumulativeCost,
32+
SequencingToMinimizeWeightedCompletionTime, SequencingToMinimizeWeightedTardiness,
33+
SequencingWithReleaseTimesAndDeadlines, SequencingWithinIntervals, ShortestCommonSupersequence,
34+
StringToStringCorrection, SubsetSum, SumOfSquaresPartition, ThreePartition, TimetableDesign,
3535
};
3636
use problemreductions::models::BiconnectivityAugmentation;
3737
use problemreductions::prelude::*;
@@ -193,6 +193,7 @@ fn all_data_flags_empty(args: &CreateArgs) -> bool {
193193
&& args.domain_size.is_none()
194194
&& args.relations.is_none()
195195
&& args.conjuncts_spec.is_none()
196+
&& args.expression.is_none()
196197
&& args.deps.is_none()
197198
&& args.query.is_none()
198199
&& args.coeff_a.is_none()
@@ -735,6 +736,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str {
735736
}
736737
"IntegerKnapsack" => "--sizes 3,4,5,2,7 --values 4,5,7,3,9 --capacity 15",
737738
"SubsetSum" => "--sizes 3,7,1,8,2,4 --target 11",
739+
"IntegerExpressionMembership" => {
740+
"--expression '{\"Sum\":[{\"Sum\":[{\"Union\":[{\"Atom\":1},{\"Atom\":4}]},{\"Union\":[{\"Atom\":3},{\"Atom\":6}]}]},{\"Union\":[{\"Atom\":2},{\"Atom\":5}]}]}' --target 12"
741+
}
738742
"ThreePartition" => "--sizes 4,5,6,4,6,5 --bound 15",
739743
"KthLargestMTuple" => "--sets \"2,5,8;3,6;1,4,7\" --k 14 --bound 12",
740744
"QuadraticDiophantineEquations" => "--coeff-a 3 --coeff-b 5 --coeff-c 53",
@@ -2401,6 +2405,34 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> {
24012405
)
24022406
}
24032407

2408+
// IntegerExpressionMembership
2409+
"IntegerExpressionMembership" => {
2410+
let usage = "Usage: pred create IntegerExpressionMembership --expression '{\"Sum\":[{\"Atom\":1},{\"Atom\":2}]}' --target 3";
2411+
let expr_str = args.expression.as_deref().ok_or_else(|| {
2412+
anyhow::anyhow!(
2413+
"IntegerExpressionMembership requires --expression and --target\n\n{usage}"
2414+
)
2415+
})?;
2416+
let target = args.target.as_deref().ok_or_else(|| {
2417+
anyhow::anyhow!("IntegerExpressionMembership requires --target\n\n{usage}")
2418+
})?;
2419+
let target: u64 = target
2420+
.parse()
2421+
.context("IntegerExpressionMembership --target must be a positive integer")?;
2422+
if target == 0 {
2423+
anyhow::bail!("IntegerExpressionMembership --target must be > 0");
2424+
}
2425+
let expr: IntExpr = serde_json::from_str(expr_str)
2426+
.context("IntegerExpressionMembership --expression must be valid JSON representing an IntExpr tree")?;
2427+
if !expr.all_atoms_positive() {
2428+
anyhow::bail!("IntegerExpressionMembership --expression must contain only positive integers (all Atom values > 0)");
2429+
}
2430+
(
2431+
ser(IntegerExpressionMembership::new(expr, target))?,
2432+
resolved_variant.clone(),
2433+
)
2434+
}
2435+
24042436
// ThreePartition
24052437
"ThreePartition" => {
24062438
let sizes_str = args.sizes.as_deref().ok_or_else(|| {
@@ -7804,6 +7836,7 @@ mod tests {
78047836
storage: None,
78057837
quantifiers: None,
78067838
homologous_pairs: None,
7839+
expression: None,
78077840
coeff_a: None,
78087841
coeff_b: None,
78097842
rhs: None,

0 commit comments

Comments
 (0)