Skip to content

Pysat pb reification optimisation#783

Draft
OrestisLomis wants to merge 5 commits intomasterfrom
pysat-pb-reification
Draft

Pysat pb reification optimisation#783
OrestisLomis wants to merge 5 commits intomasterfrom
pysat-pb-reification

Conversation

@OrestisLomis
Copy link
Contributor

This PR is such that conditionals can natively be added when using pysat to translate PB constraints.
The PR depends on two other PRs, one in pysat itself pysathq/pysat#206 which adds this functionality within pysat and another one in PBLIB rjungbeck/pypblib#6, which cleans up some trivial constraints. The latter one is not a blocker, it's just a testcase that would need to be changed.

@OrestisLomis OrestisLomis requested a review from hbierlee October 31, 2025 16:16
Copy link
Contributor

@hbierlee hbierlee left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This can actually be made into a mergeable PR with the following trick: expect this assertion (using with pytest.raises(..), see doc) to raise an AssertionError (as it currently would). This passes. Once pypblib is updated and on our end upgraded, this test fails, and can be update the test. Maybe over-engineered, but avoids needing to remember this PR forever.

[edit: so that's only about the bit that tests the new expected output from pypblib. Indeed, the PySAT one is blocking for this PR, so we'll have to wait. The code looks good.]

@IgnaceBleukx
Copy link
Collaborator

So the PR is merged into PySAT master already, but I guess we are waiting for a pipy release?

@OrestisLomis
Copy link
Contributor Author

Yes, although the PBLIB PR is probably not gonna be updated anytime soon. So I should also change the testcase as @hbierlee suggested before merging. Either way, rjungbeck/pypblib#6 should probably not really happen that much because trivially sat/unsat constraints shouldn't occur too much..

@tias
Copy link
Collaborator

tias commented Feb 2, 2026

Can you move ahead with it @OrestisLomis ? when merging master in it, still one test failing

FAILED tests/test_pysat_wsum.py::TestEncodePseudoBooleanConstraint::test_encode_pb_reified - AssertionError: '[[3, -4], [1, -4], [2, -4], [-4]]' != '[[-4]]'

@OrestisLomis
Copy link
Contributor Author

So both external PRs are now merged in their respective code bases. The failing test specifically is related to the PBLib PR, but that should be released with v1.0.449 of PBLib. Does the CI have the most up to date version?

@tias
Copy link
Collaborator

tias commented Feb 4, 2026

Well... our pysat install file refers to the pip pypblib package, which is this one from 2019:
https://pypi.org/project/pypblib/#history

So... is there another pypblib we should be using, on pip?

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.

4 participants