Skip to content

Hermax MaxSAT modeling library#1070

Open
IgnaceBleukx wants to merge 8 commits into
masterfrom
hermax
Open

Hermax MaxSAT modeling library#1070
IgnaceBleukx wants to merge 8 commits into
masterfrom
hermax

Conversation

@IgnaceBleukx

@IgnaceBleukx IgnaceBleukx commented Jul 24, 2026

Copy link
Copy Markdown
Collaborator

Interface to the HerMax MaxSAT library.

Supports CP-level constraints, so does not require linearize/int2bool.

Two open issues:

  1. __eq__ between two variables with disjoint domains raises a ValueError (see failing test). @josalhor I think it might be more natural to either return an empty clause instead, or return a specialized "trivial unsat" error or something. Then we can catch it at the CPMpy level and convert it to BoolVal(False) instead. I don' dare to catch ValueErrors as they can mean lots of things : )
  2. Time limits are not supported as far as I can tell; I can of course interrupt the process with a Python Timer (as we do in PySAT), but HerMax does not provide a feasible solution in that case

@josalhor

Copy link
Copy Markdown

Hello :D

eq between two variables with disjoint domains raises a ValueError (see failing test).

I think you mean between a variable and a constant, is that correct?
Also, I see no failing test (?)

Time limits are not supported as far as I can tell; I can of course interrupt the process with a Python Timer (as we do in PySAT), but HerMax does not provide a feasible solution in that case

After talking with other people in the community I think I know how to support this.
Would you be interested only in optimal solutions with time limit setting or also suboptimals?

I will do a review of the integration soon

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants