Pysat wsum #114
Pysat wsum #114
Conversation
|
New version can be reviewed. |
|
I wanted to include it in the release I am about to make, so I made some quick cleanups (space changes, solver_vars instead of list of solver_var, a few one-line docs). But then I noticed:
If you could fix that, then it can be merged for the next release, it looks ready otherwise (but so there might be some subtle cases still in the new flatten code) |
|
After offline discussion, the question remains whether outputting a Boolean value from linearize is still optimal (since it's not a linear; if we go this route we should update linearize's spec). An alternative solution is to return actual linears |
There was a problem hiding this comment.
Nice! Seems like this acient PR is getting there : )
I fully agree with putting pysat directly after linearize, with the has_subexpr optimization that was merged recently, the overhead should be ok (maybe we do have to test that tho... see #512 ).
I'm not sure we need to full transformation stack however, see the comments in the files themselves.
You can also remove the old code instead of commenting it, that makes the review process (imho) a little easier
The inferrance of the p-line was not complete, so I just removed it. In general, it is better in terms of debugging and performance to enforce that DIMACS files are well-formed with contiguous literals and a matching number of variables/clauses.
- Removing unneeded transformations - Remove outdated (e.g. `mul`) and commented code - Improve testing - Refactor calls to PySAT's card/pb functions - Merge duplicated behaviour in linearize/only_positive_bv
|
@IgnaceBleukx I believe it's mergeable; tests seem stable and I think the code/docs are decent. |
|
Working out the last unit test. |
This removes the possibility of Boolean literals from the output of linearize, which is good b/c they are not linear constraints.
|
Approximately one minute later.. Now I'm a lot happier with the changes to linearize, because it is simplified by never returning Boolean literals (instead turning them into trivial constraint, linear or clausal, depending on the solver). An even better approach would be to simply fix them to their value (so they might propagate further), but I believe this is not usually done so should be left for another issue. |
Its decomposition outputs Integer variables it seems
|
[nevermind] |
| @@ -1292,7 +1292,7 @@ def test_among(self): | |||
| iv = cp.intvar(0,10, shape=3, name="x") | |||
|
|
|||
| for name, cls in cp.SolverLookup.base_solvers(): | |||
|
|
|||
| if name in ("pysat",): continue | |||
Weighted sum