contrib.cp interface to Google OR-Tools CP-SAT solver - #4037
Closed
emma58 wants to merge 2 commits into
Closed
Conversation
Pull the solver-agnostic pieces of the docplex CP writer out into a new repn/util.py so the upcoming CP-SAT writer can share them instead of duplicating them: - categorize_cp_model(), replacing the writer's own collect_valid_components() with the standard categorize_valid_components() from pyomo.repn.util (the old helper had a mutable-default-argument bug and its own TODO flagging it as inefficient). collect_valid_components() is kept as a @deprecated shim that reconstructs its old return shape for any external caller. - getitem_arg_domain(), the brute-force index-domain enumeration used to handle GetItemExpression indirection - this had no docplex-specific content at all. - CPExpressionVisitorBase, a shared StreamBasedExpressionVisitor engine (initializeWalker/beforeChild/exitNode) that LogicalToDoCplex now subclasses instead of duplicating; concrete writers just supply their own var_handles/exit_node_dispatcher/step_function_handles tables. - The visitor's pyomo-to-native-variable map is renamed pyomo_to_docplex -> pyomo_to_native accordingly (updated throughout docplex_writer.py and the low-level test_docplex_walker.py suite that exercises it directly). Also factors the two scheduling-heavy models used in test_docplex_writer.py's solver tests out into tests/models.py (pure model builders) and tests/common_tests.py (solver-name-parametrized checks), mirroring the existing pyomo/gdp/tests/ models.py + common_tests.py pattern, so the planned CP-SAT writer's tests can reuse them unmodified instead of retyping the same models. No intended behavior change: the full pyomo/contrib/cp/tests/ suite (181 tests, plus the docplex-specific ones that only skip here because the cpoptimizer solver executable isn't installed) passes before and after. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Adds repn/cpsat_writer.py, a StreamBasedExpressionVisitor-based writer and
solver plugin for Google OR-Tools' CP-SAT (ortools.sat.python.cp_model),
registered as WriterFactory('cpsat_model') / SolverFactory('cp_sat'),
mirroring docplex_writer.py's architecture and sharing the solver-agnostic
infrastructure extracted in the prior commit (repn/util.py).
CP-SAT's cp_model API is statement-oriented (model.add(...)/
model.add_bool_and(...)/etc. post a constraint rather than returning a
reusable Boolean-valued expression the way docplex's does), so every
Boolean-valued Pyomo node carries a lazy (assert_fn, reify_fn) pair (tagged
_AUXILIARY) instead of docplex's ~13 special-case tags: assert_fn posts the
statement directly when it's the root of a LogicalConstraint (no extra
variable), reify_fn manufactures an auxiliary literal and reifies it when
the node is nested inside something else.
Two constructs have no native CP-SAT primitive and needed a real design
(both worked out and confirmed with the user beforehand):
- SequenceVar-based ordering (first_in_sequence/last_in_sequence/
before_in_sequence/predecessor_to): resolved via a hybrid encoding.
Whether a NoOverlapExpression is unconditionally asserted over the same
SequenceVar elsewhere in the model determines whether these translate to
cheap reified start-time comparisons, or need the fully general
position/rank-variable + AllDifferent fallback. Determining "elsewhere in
the model" requires seeing every LogicalConstraint regardless of
declaration order, so these four constraint types are never resolved at
exitNode time -- each just records a task, and CPSatWriter.write() walks
and asserts every LogicalConstraint first, then resolves every deferred
sequencing task afterward.
- Cumulative/step-function resource constraints (Pulse/Step/
CumulativeFunction/AlwaysIn): a fast path for a pure-Pulse sum over the
whole horizon (-> add_cumulative) and a special case for a pure-Step sum
(-> add_reservoir_constraint_with_active); anything else (mixed terms,
non-constant heights/bounds, a partial window) raises a clear
NotImplementedError naming the failing condition, rather than attempting
an unverified general encoding.
Span/Alternative/Synchronize similarly have no native primitive and are
decomposed into reified presence + start/end/size (in)equalities; only
asserting them directly is supported (reifying one as a nested Boolean term
raises NotImplementedError) since that's how Pyomo models actually use them
in practice.
Also fixes a real bug caught while testing against a live ortools install:
OR-Tools' IntVar.proto.domain is a protobuf repeated-field wrapper, not a
plain list, and its negative indexing (dom[-1]) silently returns the wrong
element -- affects bound inference for GetItemExpression element
constraints and auxiliary target variables.
Extensively hand-verified against a real ortools install beyond the new
pytest suite (pyomo/contrib/cp/tests/test_cpsat_writer.py): both sequencing
branches, nested logical reification, span/alternative/synchronize, the
cumulative fast path and reservoir special case, the mixed-term
NotImplementedError, and specifically that predecessor_to's adjacency
semantics reject an interloper scheduled strictly between a direct pair
(distinguishing it from before_in_sequence's weaker non-adjacent ordering).
Known limitations, called out in code comments where they arise: CP-SAT
requires finite bounds on every variable (unlike CP Optimizer's effectively
unbounded horizon) and truncates integer division (unlike CP Optimizer's
float_div); indirected method calls (e.g. 'm.i[m.x].before(...)') are not
yet supported.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Contributor
Author
|
Eeeek, sorry and she doesn't know how to use github. Please ignore this! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes # .
Summary/Motivation:
First AI-generated draft of an interface to the Google OR-Tools CP-SAT solver. Just putting it here so that I can review it and ask Claude to do stuff...
Changes proposed in this PR:
AI-Use Disclosure
or
AI tools contributed to the development of this PR
Review process (select ONE):
Notes for reviewers (optional):
Legal Acknowledgement
By contributing to this software project, I have read the contribution guide and agree to the following terms and conditions for my contribution: