Rc2 maxsat solver #729
Rc2 maxsat solver #729
Conversation
hbierlee
left a comment
hbierlee
left a comment
There was a problem hiding this comment.
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.
| else: | ||
| raise NotImplementedError(f"CPM_rc2: Non supported term {w,x} in objective {flat_obj} (yet?)") | ||
|
|
||
| # positive weights only, flip negative |
There was a problem hiding this comment.
don't we have only_positive_coefficients for this? Or are you not using that because it's a Comparison?
| # make sure that `SolverLookup.get(solver)` works | ||
| # also add exclusions to the 3 EXCLUDE_* below as needed | ||
| SOLVERNAMES = [name for name, solver in SolverLookup.base_solvers() if solver.supported()] | ||
| SOLVERNAMES = [n for n in SOLVERNAMES if n not in ["rc2"]] # only supports optimisation |
There was a problem hiding this comment.
on or the other line should be removed?
| self.assertTrue(solved) | ||
| self.assertIsNotNone(solver.objective_value()) | ||
| # The optimal solution should have x[0]=True, x[1]=True, x[2]=True for objective value 3 | ||
| # But RC2 might find a different solution due to the constraints |
There was a problem hiding this comment.
sorry, what? Why won't it just find the optimal solution where all vars are assigned true?
|
|
||
| def test_incremental(self, solver): | ||
| if solver == "rc2": | ||
| pytest.skip("not incremental") |
There was a problem hiding this comment.
I thought rc2 was incremental?
| self.assertTrue(solved) | ||
| self.assertEqual(solver.objective_value(), 3) | ||
| self.assertEqual(list(x.value()), [False, True]) | ||
|
|
There was a problem hiding this comment.
perhaps we can have a test for incrementally updating the objective (ie adding additional soft clauses)? Or do we not expose this yet?
|
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. |
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?