Research map / Learning theory and algorithms / Combinatorial and search optimization
On the Modelling of Constraints with Tractable Logical Operators
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes constraint representation pairs (primal/dual) to get tractable negation on binary constraint trees and OMVD/OMDD, yielding op-BCT and op-OMVD subforms that are more succinct than OMDD while supporting tractable logical operators.
Problem
Negation (and general logical combinations) of ad-hoc constraints is intractable in many constraint representations, so modellers cannot combine basic constraints with (∧, ∨, ¬) efficiently while keeping representation size small.
Approach
A constraint representation pair (A, B) stores a constraint and its negation in the same structure, so negation is just swapping the pair and conjunction/disjunction reduce to operations on the two components; ordered pairs (same variable ordering or constraint graph) give tractable conjunction and disjunction too.
Key results
- BCT AC propagator on op-BCT reified constraints is up to 124 times faster than the MDDc propagator, and at least 4 times faster on 54% of instances.
- On product configuration instances (e.g., big, master, megane), op-BCT representations are much more compact than OMDD under the same MinFill ordering (e.g., megane: about 34K words total vs 326K nodes and 439K edges for OMDD).
- Theoretical results show op-BCT and op-OMVD are strictly more succinct than OMDD and that conjunction/disjunction of op-BCT/op-OMVD constraints with the same structure are tractable, while arbitrary-structure conjunction is not polytime.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use op-BCT AC propagation instead of MDDc propagation for reified constraints | reified constraint models · 122 reification benchmark instances | running time: up to 124 times faster; at least 4 times faster on 54% of instances | Helped |
| model the product configuration instances with op-BCT instead of OMDD using the same variable ordering | product configuration models · product configuration benchmarks | representation size | Helped |
Surprising findings
- Conjunction and disjunction of a set of op-BCT or op-OMVD constraints with the same structure are intractable, despite pairwise tractability.
Limitations
- Tractable logical operators only hold when operands share the same structure (variable ordering or constraint graph).
- Experiments are limited to a single reification benchmark family and a product configuration benchmark, with preliminary results.
- Negation tractability is achieved by doubling representation (primal and dual).
Experimental setup
Datasets: CSP competition 2009 instances (bddSmall, dag-half, lexVg, ukVg, wordsVg, TSP-20, TSP-25) product configuration benchmarks (Bessiere, Fargier, Lecoutre 2016)
Benchmarks: CSP competition 2009 reification instances (122 after filtering) product configuration benchmarks
Metrics: running time (seconds) time ratio MDDc/BCT-AC representation size (nodes, edges, hidden values, words)
Baselines: MDDc propagator OMDD
Builds on: OMDD OMVD binary constraint tree MDDc GAC propagator BCT AC propagator
Closest papers by meaning
- The Expressive Power of Ad-Hoc Constraints for Modelling CSPs (AAAI 2023 · similarity 0.90)
- Encoding Constraints as Binary Constraint Networks Satisfying BTP (AAAI 2024 · similarity 0.85)
- Logic.py: Bridging the Gap between LLMs and Constraint Solvers (NeurIPS 2025 · similarity 0.84)
- The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.83)
- Decomposing Constraint Networks for Calculating c-Representations (AAAI 2024 · similarity 0.83)
- Self-Supervised Transformers as Iterative Solution Improvers for Constraint Satisfaction (ICML 2025 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.