Rc2 maxsat solver #729

tias · 2025-09-10T16:34:45Z

this needs more extensive testing...

(but its small test-case works)

also, there was a tricky aspect of using direct encoding (with weight 0 literals) in the objective... henk could you have a look?

hbierlee

Ok, looks good to me!

The transform_objective should become part of the int2bool encode_expr (as it just encodes a linear sum, which is implemented that as part of encoding a linear constraint). This can wait until we need it for other optimization-compatible Boolean solvers.

cpmpy/solvers/rc2.py

tests/test_constraints.py

tests/test_rc2_obj.py

tests/test_solvers.py

tests/test_rc2_obj.py

hbierlee · 2025-11-03T13:03:58Z

@tias

as discussed in the meeting, more important than the above review questions, is that we should consider whether we can add RC2 as a subsolver? Just from a user perspective, should "Pysat" and "RC2" seen side by side, or RC2 as part/subsolver of Pysat?

If subsolver, I can try to refactor that. If not, probably I can still remove some duplication by perhaps subclassing.

hbierlee · 2025-12-12T09:55:58Z

Currently working on this, my idea is:

try to make RC2 a sub-solver of PySAT, since this duplicates quite a bit of code
see if we can also make it work for decision problems
process my above comments

hbierlee · 2025-12-15T14:28:29Z

@tias since you made the original draft, could you review? Two executive decisions are needed:

should we make RC2 a sub-solver of pysat, which would be easy to do, it's just about the user perspective. Since the solver properties (supports objectives, but only once, is incremental but without assumptions,..) are fairly different.. I'm leaning towards "no" at the moment?
time limit is not supported, but we should not (maybe cannot) do this in a subprocess since we'd have to parse the text. Instead, I can open a PR in PySAT. In the meantime, I'd say we can leave the time limit as unsupported for this release, and fix it in the next release when that PR is merged.

hbierlee · 2025-12-16T16:39:49Z

I've added a PR for the missing interrupt feature (required for timeouts) in RC2 pysathq/pysat#211. As above, the question is whether we wait for that to merge this PR, or if we merge RC2 w/o time limits

hbierlee · 2025-12-18T14:00:57Z

Seems good to wait for the upstream PR, since the release is not imminent.

On the other hand, one outstanding TODO is supporting atmost constraints. Working on that now.

hbierlee · 2025-12-18T16:44:01Z

Ready for review!

I've added native support for AtMostK constraints for RC2 (in case the solver supports it - otherwise these AtMostK are encoded in solve).
This keeps all configuration in solve, like most CPMpy solvers (except e.g. Exact).

One other (arguable) change is that I replaced the RC2 solver arguments which are added explicitly in RC2solve(..) by just **kwargs, which is in line with the other solvers; additional kwargs are for the solver.
I kept the competition defaults if no kwargs are given.
Happy to revert it.

One side note is that RC2 does not allow the user currently to pass arguments for its oracle sub-solver. That might be worth an issue. For instance, currently, even though Cadical has native AtMostK support, we cannot actually enable it when using RC2. This might be worth a PySAT issue.

tests/test_solvers.py

hbierlee · 2025-12-22T11:36:57Z

Currently, two small issues preventing merge when implementing timeouts:

It seems the compute call does not distinguish between unsat/unknown (I believe it is intended to, though; added issue Distinguish between unknown and unsat in RC2 pysathq/pysat#213)
A new failing test which was added recently

tias

the native handling seems to create technical debt, not a fan... to discuss

cpmpy/solvers/pysat.py

tias · 2025-12-19T16:50:10Z

cpmpy/solvers/rc2.py

+            atmosts = []
+            if isinstance(cnf, list):
+                clauses = cnf
+            elif isinstance(cnf, tuple):


euh... what?
so somebody will use 'append_formula' somewhere, and it will give it a tuple, and they will know what this tuple should be, and elsewhere we should know that any tuples is an atmost?

this is is too implicit...

in pysat itself we do not support native atmostk? then I find it weird that we hack it in here, and especially in this way...

the reason that it's more complicated here with the overriding of append_formula is that we collect the encoding in WCNFPlus and then instantiate the solver in solve from the WCNFPlus. This is so that we can give the solver args there as in most solvers (Exact being the only exception). The implementation may be simplified if we do require the RC2 solve args to be given to init so we don't have this WCNFPlus in-between.

in pysat, we do support native atmost k's (https://github.com/CPMpy/cpmpy/blob/master/cpmpy/solvers/pysat.py#L547)

Side note: nobody is supposed to use append_formula, it's a method of a "private" field (although I suppose they could get it through the native_model).

tias · 2025-12-19T16:54:44Z

cpmpy/solvers/rc2.py

+        if time_limit is not None:
+            raise NotImplementedError("CPM_rc2: time limit not yet supported")
+
+        # hack to support decision problems


I don't think we should? we can just raise that the solver is not for that?

I'm also fine with that, it just seemed a very easy extension + allows us to more easily test RC2

tias · 2025-12-19T16:55:47Z

cpmpy/solvers/rc2.py

+
+        # determine subsolver
+        default_kwargs = {"solver": "glucose3", "adapt": True, "exhaust": True, "minz": True}
+        stratified = kwargs.get("stratified", True)


why handle stratified differently? Can just be in default_kwargs as true too?

Because stratified is not an RC2 argument, you use it by using the different class. I can add it to default_kwargs, but then I need to remove it again when I pass the args to compute

tias · 2025-12-19T16:57:43Z

cpmpy/solvers/rc2.py

+        if sub_solver and not Solver(name=sub_solver).supports_atmost():
+            # encode AtMostK constraints since they are unsupported by sub-solver oracle
+            atmosts = self.pysat_solver.atms
+            self.pysat_solver.__class__ = WCNF


a line like this is black magic and to be avoided

yeah.. there's no official way to convert WCNFPlus to WCNF, and this avoids copying. I've made a change which avoids the downclass though.

cpmpy/transformations/linearize.py

tests/test_rc2_obj.py

hbierlee · 2025-12-22T14:13:47Z

Small comments are resolved, I think there are two knots to cut:

Simple one: should we keep in the slight hack to enable solving decision problems with RC2? To me it seems useful, and the hack is theoretically sound
See comment near WCNFPlus/AtMostK stuff about the implementation, but I believe the main reason it's made complicated is because of the in-between WCNFPlus object required to keep solve arguments in solve rather than in __init__. I see 3 options:
1. Keep AtMostK stuff as implemented, so that we support all features and sub-solvers for RC2 (note that pysat does support atmostk).
2. Pass encoded constraints directly to RC2 without the WCNF[Plus] in-between, this may simplify the implementation, and keeps the AtMostK native feature, however, we have to move (some) solver args to __init__ (like in Exact), and other features like process will be lost as they only work if RC2 is bootstrapped from a formula.
3. Omit AtMostK support, just always encode everything into a WCNF object, passed to RC2 at solve time (which keeps solve arguments there)

hbierlee · 2025-12-22T16:05:11Z

Fixed the new failing test, and have a pretty good workaround for the time limit issue. [edit; the workaround is the intended method]

I think all that remains are the two points above, if @tias can decide between the options then this PR should still be made mergeable in pretty short order.

The CI is taking a bit long recently, not sure why (although adding RC2 as another solver probably doesn't help of course). [edit: seems that's just 8 more minutes from adding RC2]

hbierlee · 2025-12-23T12:21:40Z

@tias I still can't add you as reviewer since you're the author of the PR, but if you could make some executive decisions on #729 (comment), and have a look at whatever comments are unresolved, then that'd be great

tias requested a review from hbierlee September 10, 2025 16:34

hbierlee reviewed Sep 16, 2025

View reviewed changes

cpmpy/solvers/rc2.py Outdated Show resolved Hide resolved

tests/test_constraints.py Outdated Show resolved Hide resolved

tests/test_rc2_obj.py Outdated Show resolved Hide resolved

tests/test_solvers.py Outdated Show resolved Hide resolved

tests/test_rc2_obj.py Show resolved Hide resolved

tias added this to the v.0.9.28 milestone Oct 6, 2025

tias assigned hbierlee Oct 6, 2025

hbierlee force-pushed the rc2 branch from 52dcc82 to 1954e92 Compare December 12, 2025 09:53

hbierlee force-pushed the rc2 branch from d731cfc to d92f13e Compare December 15, 2025 14:21

hbierlee mentioned this pull request Dec 16, 2025

Add interrupts to RC2 pysathq/pysat#211

Merged

hbierlee marked this pull request as draft December 18, 2025 14:00

hbierlee marked this pull request as ready for review December 18, 2025 16:44

hbierlee reviewed Dec 19, 2025

View reviewed changes

tests/test_solvers.py Outdated Show resolved Hide resolved

hbierlee force-pushed the rc2 branch from 0df0658 to 5bb7888 Compare December 22, 2025 11:22

hbierlee marked this pull request as draft December 22, 2025 11:23

tias commented Dec 22, 2025

View reviewed changes

tias and others added 9 commits December 22, 2025 15:53

initial rc2 impl, not very well tested

cb22efc

more rc2

61a14f8

add rc2 tests, obj

c5a7c5e

direct encoding 0 weight softlit bug

987a673

also negative offset direct encodings need a shift

9934503

based on discussion with alexey (stratified does not work yet)

d356db6

work around rc2 stratified bug, actually nicer to have params in solve

d6b2e16

fix bug, put back regular example testers

d37046f

back to original tsp

ac8c629

hbierlee and others added 25 commits December 22, 2025 15:53

fix tests

b1f7d06

more uniform handling of 0's and negative weights

2655e06

add rc2 to index page

1f913eb

add docs api rc2

310b7c0

add rc2 to setup

e29633a

rc2: activate cse map for flatten obj

192f5f1

Refactor some duplicate int2bool code, fix tests

eb756c5

Support decision problems for RC2

3341b37

Refactor flatten objective

02fedd8

Fix remaining tests

cb5de42

Clarify in which way rc2 is and is not incremental

c1070e1

Clean up

8665761

Support native AtMostK for RC2

7032006

Add tests and use proper AtMostK supporting solver (MC)

d812705

Implement RC2 timeouts + small clean-up

e5e597b

Enable time limit tests for RC2

a7aeba7

Sync to main branch

1a7ae24

Remove time limit unsupported error

0761bec

Distinguish between unsat and unknown

1018aef

Avoid downcast

a6b2591

Fix docstring

39ca8cb

Fix test obj value

46283ee

Add docstring _process_solution

e422237

Rename get_user_vars

5eede41

Properly transform objective

804cc1d

hbierlee force-pushed the rc2 branch from 1563f64 to 804cc1d Compare December 22, 2025 15:58

Add consistent time limit for test

dd1532f

hbierlee marked this pull request as ready for review December 23, 2025 12:20

Rc2 maxsat solver #729

Are you sure you want to change the base?

Rc2 maxsat solver #729

Uh oh!

Conversation

tias commented Sep 10, 2025

Uh oh!

hbierlee left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hbierlee commented Nov 3, 2025

Uh oh!

hbierlee commented Dec 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hbierlee commented Dec 15, 2025

Uh oh!

hbierlee commented Dec 16, 2025

Uh oh!

hbierlee commented Dec 18, 2025

Uh oh!

hbierlee commented Dec 18, 2025

Uh oh!

Uh oh!

hbierlee commented Dec 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tias left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

hbierlee commented Dec 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hbierlee commented Dec 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hbierlee commented Dec 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

hbierlee commented Dec 12, 2025 •

edited

Loading

hbierlee commented Dec 22, 2025 •

edited

Loading

hbierlee commented Dec 22, 2025 •

edited

Loading

hbierlee commented Dec 22, 2025 •

edited

Loading

hbierlee commented Dec 23, 2025 •

edited

Loading