Optimizing Optimizations: Case Study on Detecting Specific Types of Mathematical Optimization Constraints with E-Graphs in JijModeling

Hiromi Ishii (1); Inc.); Taro Shimizu (1); Toshiki Teramura (1) ((1) Jij

REVIEW 3 major objections 3 minor 9 references

Optimizing Optimizations: Case Study on Detecting Specific Types of Mathematical Optimization Constraints with E-Graphs in JijModeling

T0 review · 3 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read JijModeling uses e-graphs to detect one-hot and SOS1 constraints even when algebraically disguised, and the detected structure makes solvers finish much faster.

desk verdict Solid industrial case study on e-graph based constraint detection; the speedup is real, but the benchmark needs a solution-quality check. read the letter →

arxiv 2506.06495 v1 pith:BSZ2VNWS submitted 2025-06-02 cs.PL cs.MSmath.OC

Hiromi Ishii (1) , Taro Shimizu (1) , Toshiki Teramura (1) ((1) Jij , Inc.) This is my paper

classification cs.PLcs.MSmath.OC

keywords e-graphsequalitysaturationconstraintdetectionmathematicaloptimizationJijModelingrewriterulesone-hotconstraintsSOS1

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper reports a production case study in constraint detection for mathematical optimization. JijModeling, a modeling tool that keeps symbolic problem descriptions separate from data, uses e-graphs to recognize one-hot and SOS1 constraints even when users write them in algebraically different but equivalent forms, such as $\sum_i x_i = 1$, $\sum_i x_i - 1 = 0$, or $0 = 1 - \sum_i x_i$. The authors' central claim is that e-graph-based equality saturation can detect these constraint types modulo algebraic congruence, and their benchmark shows that enabling SOS1 detection makes a plant-placement problem solve much faster because the solver can then use dedicated SOS1 algorithms. The paper also contributes heuristic design criteria for rewrite systems: bidirectionalize asymmetric rules, guard inverse rules with type side conditions, and prefer size-reducing rules. It additionally introduces egg_recursive, a utility library for writing e-graph rewrite rules as recursive syntax trees rather than S-expressions.

What carries the argument

The central machinery is the e-graph, a compact graph representation of many equivalent expressions, together with equality saturation: repeatedly applying rewrite rules until no new equivalences appear, then matching patterns against the saturated graph. An analysis phase computes a type approximation and performs constant folding; this analysis feeds side conditions such as is_of_type(var('?a'), TypeHint::Scalar) that keep bidirectional rewrite rules from producing ill-typed terms. The one-hot detection pattern is a sum over binary decision variables equated to 1, and SOS1 detection is expressed through binary-variable sums together with upper-bound constraints. A companion library, egg_recursive, lets the roughly 120 rules be written as recursive abstract syntax trees using record-style fields instead of S-expressions.

What would settle it

One concrete test: take a constraint known to be one-hot or SOS1 only after algebraic rewriting, for example $2\sum_i x_i - 1 = 1$, run JijModeling's detector on it, and check whether the constraint hint is emitted; a miss would refute the claim that detection works modulo congruence. A sharper test feeds a well-typed boolean or tensor expression into a scalar-expecting rule and looks for a false-positive hint, which would show the type approximation is unsound.

Watch

Extended reading notes

Core claim

The core discovery is that equality saturation, a technique usually aimed at program optimization, can be turned into a constraint-type detector. Each constraint is converted into its own e-graph; rewrite rules for commutativity, associativity, distributivity, constant folding, and a few reduction-operator laws are applied until saturation, and a light analysis phase computes an approximate type for each subexpression. A pattern then matches a sum of binary variables equated to 1 (one-hot) or the joint conditions that encode SOS1. The paper reports that the same benchmark problem is solved dramatically faster with detection and that hidden one-hot constraints in the TSP example are automatically found even when written as $2\sum_i x_i - 1 = 1$.

Load-bearing premise

The detector is only sound if the analysis phase's type approximation correctly labels every subexpression; the paper states that ill-typed rewrites caused unsound results in the past, but it does not prove the approximation sound.

Editorial extensions

If this is right

Users of JijModeling can write the same logical constraint in different algebraic forms and still receive specialized solver treatment, because matching is modulo congruence rather than exact syntax.
Enabling detection can turn a model that a generic solver treats as expensive into one where the solver invokes dedicated one-hot or SOS1 algorithms, shrinking wall-clock time (the benchmark shows a large gap at every tested $N$).
The design heuristics, such as making asymmetric rules bidirectional, adding type side conditions on inverse directions, and adding reductive rules like $a + (-a) \to 0$, apply to other domain-specific languages that need pattern matching modulo congruence.
The egg_recursive interface lowers the maintenance burden for rule sets of about 120 rules, making it practical to grow the detection library.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

An implicit next step is to apply the same e-graph detection to other structured constraint families, such as cardinality constraints, SOS2, or ordering constraints, where users naturally write many algebraically equivalent forms.
The paper's type-side-condition lesson suggests that a formal type system with a soundness proof for the type approximation, which the paper does not provide, would be the natural way to eliminate the risk of unsound rewrites in future versions.
If bound variables are later handled with locally nameless or higher-order abstract syntax, e-graph matching will face the harder problem of beta-equivalence, and detection rules may need to be restricted to avoid explosion.
Representing sums and products as variadic bags instead of binary trees could make associative-commutative matching direct and reduce saturation time, possibly removing the need for some rewrite rules.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short version: this is a worthwhile case study. It applies egg-based equality saturation to detect SOS1 and one-hot constraints in JijModeling, describes practical heuristics for rule design, and shows a large solve-time speedup on a plant placement problem. The code is on GitHub, and the paper is honest about its limitations.

What is new: constraint detection via e-graphs in a mathematical optimization DSL, matching modulo algebraic congruence without canonical normal forms. The heuristics in Section 3 are the real contribution: bidirectionalize asymmetric rules for pattern matching, use type side-conditions when reversing type-reducing rules, and prefer reductive rules over analysis for performance. The authors openly say they were bitten by ill-typed rules before, which adds credibility.

The main benchmark shows a big runtime gap between with and without detection. That is good evidence the detection works. But the stress-test note is right about one thing: the paper never reports solution quality for the with-detection runs. If detection were unsound, the solver could be solving a modified problem and the speedup would be meaningless. The authors plausibly argue the rewrite rules are sound algebraic equivalences and the type side-conditions prevent ill-typed rewrites, but since the type approximation is not formally verified, comparing objective values or feasibility between the two modes would close the gap. I see that as a moderate issue, not a fatal one. The single benchmark instance and missing error bars are minor.

Citations look fine: self-citations point to software artifacts the paper evaluates. No fitted parameters, no circularity.

Who is this for? Practitioners building symbolic matching on DSLs and the e-graph community. I would bring it to a reading group. It deserves peer review; the heuristics and benchmark are worth refereeing. Ask the authors to add the solution-quality check and ideally another instance.

Recommendation: conditional accept, with the correctness check as the main request.

Referee Report

3 major / 3 minor

Summary. The paper reports a case study of a constraint detection mechanism in the JijModeling optimization modeller. The mechanism uses e-graphs (via the egg library) to detect one-hot and SOS1 constraints modulo algebraic congruence, by converting each constraint into an e-graph, saturating it with a set of rewrite rules and an analysis phase, and then matching patterns against the saturated e-graph. The paper describes heuristic criteria for designing such rewrite systems, introduces the egg_recursive utility library for writing egg rules as recursive abstract syntax trees, and evaluates the runtime impact of SOS1 detection on a single plant placement problem instance, showing a drastic reduction in solve time. The paper also discusses future work, including the use of egglog and proper treatment of bound variables.

Significance. If the detection mechanism is sound, this is a practically useful contribution: automated detection of special constraint structures can substantially improve solver performance without requiring users to explicitly declare such structures. The paper provides a reproducible benchmark (code committed at 4e9fe48) and a utility library (egg_recursive), and the proposed heuristics are experience-based and likely transferable to other pattern-matching tasks built on e-graphs. However, the current manuscript does not fully verify the correctness of the detection, which is a prerequisite for trusting the reported speedup. The work is best viewed as an engineering case study rather than a formal systems result.

major comments (3)

[Section 4, Figure 2] The benchmark reports only solve times; it does not report objective values, feasibility status, or optimality gaps for the runs with and without detection. If the SOS1 detection is unsound and the emitted hints cause SCIP to solve a different constraint set, the speedup could be an artifact of solving an easier but incorrect problem. The paper should compare the final objective values (and ideally the solution feasibility) between the two configurations for every N in Figure 2, or otherwise establish that the detected SOS1 constraints are semantically equivalent to the original constraint set.
[Section 3.1.2] The soundness of the type approximation used in the analysis phase is not established. The paper states that ill-typed rewrite rules "can lead to unsound rewriting results" and that the authors "were bitten by such ill-typed rules in the past," yet no formal type system, abstract interpretation, or soundness argument for the analysis is provided, and the only safeguard is a side condition is_of_type(var('?a'), TypeHint::Scalar). Since the correctness of one-hot and SOS1 detection depends on this analysis, the paper should either present a concrete type system with a correctness argument, or provide empirical validation that the type approximation is sound on a nontrivial set of inputs (e.g., by comparing detected constraints against brute-force equivalence checks).
[Section 4] The empirical evaluation is based on a single problem instance (the plant placement problem) with no repeated trials or error bars in Figure 2. The claim of a "drastic" speedup would be substantially more convincing if the paper reported data from multiple independent runs (with distributions or error bars) and discussed how representative this instance is of broader optimization workloads. At minimum, the authors should explicitly acknowledge this limitation in the text and avoid over-generalizing the performance conclusion.

minor comments (3)

[Figure 1, rule (8)] The coefficient in the rule "c·∑_i a_i → ∑_i c·a_i" appears as "ci" in the figure, which is likely a typographical rendering issue; please ensure the notation is consistent with the surrounding text.
[Section 4] The plant placement problem formulation is typeset with unusual spacing around the norm notation in the objective, making it hard to read; please reformat the equation for clarity.
[Section 3.2] The description of egg_recursive is clear, but the paper would benefit from a brief note on which egg version it is compatible with, since the library is still under active development.

Circularity Check

0 steps flagged · score 1.0 of 10

No load-bearing circularity; the detection rules are standard algebraic equivalences evaluated against an external solver benchmark, and self-citations are to reproducible software artifacts.

full rationale

The paper's central claim is that an e-graph-based rewrite system in JijModeling detects one-hot and SOS1 constraints modulo algebraic congruence, and that this detection reduces solver runtime. No parameter is fitted to the benchmark data, and no quantity that is later called a 'prediction' is used as an input to the detector. The rewrite rules in Figure 1 are standard algebraic equivalences (commutativity, associativity, distributivity, identity and inverse laws), and the detection pattern in Listing 3 is a syntactic template, not a learned or fitted artifact. The benchmark compares the same plant placement problem, from Santos and Toffolo, solved with and without detection using an external solver (PySCIPOpt 1.8.1); this is an external, falsifiable evaluation. Self-citations to egg_recursive, JijModeling, and the benchmark repository describe the software being presented rather than supplying an unverified premise that forces the result. The paper's own warning that ill-typed rewrite rules 'can lead to unsound rewriting results' (Section 3.1.2) identifies a real soundness risk, and Section 4 reports only runtime without objective values or optimality gaps, which is a benchmarking and verification gap. However, that gap concerns correctness and experimental completeness, not circularity: the speedup claim is not true by construction of the input. Accordingly, the circularity score is low rather than zero because the paper relies partly on its own prior artifacts, but none of those citations is load-bearing in the derivation.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The detection relies on the soundness of the rewrite rules (they preserve constraint semantics) and on the type approximation in the analysis phase being accurate enough to keep rules well-typed. Floating-point commutativity and associativity are assumed for symbolic rewriting, though noted as approximate in future work.

assumptions (3)

domain assumption Rewrite rules in Figure 1 preserve the set of feasible solutions of a constraint (soundness).
The detection is only useful if a detected one-hot or SOS1 constraint truly has that structure; the paper states the rules are sound but not complete (Section 3.1).
domain assumption The type approximation computed in the analysis phase is accurate enough for side conditions like is_of_type(var('?a'), TypeHint::Scalar) to prevent ill-typed rewrites.
Section 3.1.2 argues this is needed for soundness and says ill-typed rules previously caused bugs; no formal proof of the approximation's correctness is given.
domain assumption Floating-point addition and multiplication are commutative and associative for the purpose of symbolic rewriting.
Rules (2) and (5) assume these laws; Section 5 admits this is 'up to floating-point error', which is not mathematically true for IEEE 754 but is treated as harmless in this symbolic context.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Optimizing Optimizations: Case Study on Detecting Specific Types of Mathematical Optimization Constraints with E-Graphs in JijModeling." pith.science (2026). https://pith.science/paper/BSZ2VNWS

@misc{pith2026250606495,
  author       = {Pith},
  title        = {Pith review of: Optimizing Optimizations: Case Study on Detecting Specific Types of Mathematical Optimization Constraints with E-Graphs in JijModeling},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BSZ2VNWS}},
  note         = {Machine review of arXiv:2506.06495}
}

read the original abstract

In solving mathematical optimization problems efficiently, it is crucial to make use of information about specific types of constraints, such as the one-hot or Special-Ordered Set (SOS) constraints. In many cases, exploiting such information gives asymptotically better execution time. JijModeling, an industrial-strength mathematical optimization modeller, achieves this by separating the symbolic representation of an optimization problem from the input data. In this paper, we will report a real-world case study on a constraint detection mechanism modulo the algebraic congruence using e-graphs, and describe heuristic criteria for designing rewriting systems. We give benchmarking result that shows the performance impact of the constraint detection mechanism. We also introduce egg_recursive, a utility library for writing egg-terms as recursive abstract syntax trees, reducing the burden of writing and maintaining complex terms in S-expressions.

Figures

Figures reproduced from arXiv: 2506.06495 by the authors.

**Figure 2.** Runtime of solving the plant placement problem, [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

9 extracted references · 3 canonical work pages

[6]

Retrieved Jan

pytest-benchmark 5.1.0 documentation. Retrieved Jan. 30, 2025 from https://pytest-benchmark.readthedocs.io/en/latest. F. Pfenning and C. Elliott

work page 2025
[9]

Better Together: Unifying Datalog and Equality Saturation

“Better Together: Unifying Datalog and Equality Saturation. ”Proc. ACM Program. Lang. , 7, PLDI, Article 125, (June 2023), 25 pages. doi: 10.1145/3591239. 6

doi:10.1145/3591239 2023
[1988]

Higher-order abstract syntax

“Higher-order abstract syntax. ” In:Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implemen- tation (PLDI ’88). Association for Computing Machinery, Atlanta, Georgia, USA, 199–208. isbn: 0897912691. doi: 10.1145/53990.54010. Haroldo G Santos and T Toffolo

arXiv 1988
[2012]

The Locally Nameless Representation

“The Locally Nameless Representation. ”Journal of Auto- mated Reasoning, 49, 3, 363–408. isbn: 1573-0670. doi: 10.1007/s10817-011-9225-2. Jij, Inc

doi:10.1007/s10817-011-9225-2
[2014]

Stephen Maher, Matthias Miltenberger, João Pedro Pedroso, Daniel Rehfeldt, Robert Schwarz, and Felipe Serrano

doi: 10.3389/fphy.2014.00005. Stephen Maher, Matthias Miltenberger, João Pedro Pedroso, Daniel Rehfeldt, Robert Schwarz, and Felipe Serrano

arXiv 2014
[2016]

PySCIPOpt: Mathematical Programming in Python with the SCIP Optimization Suite

“PySCIPOpt: Mathematical Programming in Python with the SCIP Optimization Suite. ” In:Mathematical Software – ICMS 2016 . Springer International Publishing, 301–307. doi: 10.1007/978-3-319-42432-3_37. Ionel Cristian Măries,

doi:10.1007/978-3-319-42432-3_37 2016
[2021]

egg: Fast and Extensible Equality Saturation

“egg: Fast and Extensible Equality Saturation. ”Proc. ACM Program. Lang., 5, POPL, Article 23, (Jan. 2021), 29 pages.doi: 10.1145/3434304. Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. June

doi:10.1145/3434304 2021
[2023]

25, 2025 from https://jij-inc.github.i o/JijModeling-Tutorials/en/introduction.html

What is JijModeling? Retrieved Mar. 25, 2025 from https://jij-inc.github.i o/JijModeling-Tutorials/en/introduction.html. Jij, Inc.. 2025c. What is OMMX? – OMMX . Retrieved Mar. 31, 2025 from https://jij-inc.g ithub.io/ommx/en/introduction.html. Andrew Lucas

work page 2025

Show all 9 references

[2024]

Retrieved Mar

egg_recursive, an S-expression-free alternative interface to egg . Retrieved Mar. 31, 2025 from https://crates.io/crates/egg_recursive. Jij, Inc.. 2025a.Jij-Inc/sos1-detection-benchmarks at 4e9fe48da5795694aa0010f429ea8ec944860e9b. Retrieved Apr. 16, 2025 from https://github.c...

2025

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [6]

Retrieved Jan

pytest-benchmark 5.1.0 documentation. Retrieved Jan. 30, 2025 from https://pytest-benchmark.readthedocs.io/en/latest. F. Pfenning and C. Elliott

work page 2025

[2] [9]

Better Together: Unifying Datalog and Equality Saturation

“Better Together: Unifying Datalog and Equality Saturation. ”Proc. ACM Program. Lang. , 7, PLDI, Article 125, (June 2023), 25 pages. doi: 10.1145/3591239. 6

doi:10.1145/3591239 2023

[3] [1988]

Higher-order abstract syntax

“Higher-order abstract syntax. ” In:Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implemen- tation (PLDI ’88). Association for Computing Machinery, Atlanta, Georgia, USA, 199–208. isbn: 0897912691. doi: 10.1145/53990.54010. Haroldo G Santos and T Toffolo

arXiv 1988

[4] [2012]

The Locally Nameless Representation

“The Locally Nameless Representation. ”Journal of Auto- mated Reasoning, 49, 3, 363–408. isbn: 1573-0670. doi: 10.1007/s10817-011-9225-2. Jij, Inc

doi:10.1007/s10817-011-9225-2

[5] [2014]

Stephen Maher, Matthias Miltenberger, João Pedro Pedroso, Daniel Rehfeldt, Robert Schwarz, and Felipe Serrano

doi: 10.3389/fphy.2014.00005. Stephen Maher, Matthias Miltenberger, João Pedro Pedroso, Daniel Rehfeldt, Robert Schwarz, and Felipe Serrano

arXiv 2014

[6] [2016]

PySCIPOpt: Mathematical Programming in Python with the SCIP Optimization Suite

“PySCIPOpt: Mathematical Programming in Python with the SCIP Optimization Suite. ” In:Mathematical Software – ICMS 2016 . Springer International Publishing, 301–307. doi: 10.1007/978-3-319-42432-3_37. Ionel Cristian Măries,

doi:10.1007/978-3-319-42432-3_37 2016

[7] [2021]

egg: Fast and Extensible Equality Saturation

“egg: Fast and Extensible Equality Saturation. ”Proc. ACM Program. Lang., 5, POPL, Article 23, (Jan. 2021), 29 pages.doi: 10.1145/3434304. Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. June

doi:10.1145/3434304 2021

[8] [2023]

25, 2025 from https://jij-inc.github.i o/JijModeling-Tutorials/en/introduction.html

What is JijModeling? Retrieved Mar. 25, 2025 from https://jij-inc.github.i o/JijModeling-Tutorials/en/introduction.html. Jij, Inc.. 2025c. What is OMMX? – OMMX . Retrieved Mar. 31, 2025 from https://jij-inc.g ithub.io/ommx/en/introduction.html. Andrew Lucas

work page 2025