Some interesting maxSAT solvers and interfaces have been presented at FLoC '26. One question I had is the following: If we want to add a new maxSAT solver (let's say paramita, for which we have a PR now) would it not be best to actually use herMAX to do most of the transformations, i.e. CPMpy exprs -> herMAX (-> internally to maxsat) -> some final transform to paramita. This could be a lot more efficient than using our own pipeline for maxSAT solvers, but it does add an extra dependency for using paramita. We could perhaps make the dependency optional and if hermax is not installed we throw a warning an just transform the CPMpy exprs ourselves. Thoughts?
Some interesting maxSAT solvers and interfaces have been presented at FLoC '26. One question I had is the following: If we want to add a new maxSAT solver (let's say paramita, for which we have a PR now) would it not be best to actually use herMAX to do most of the transformations, i.e.
CPMpy exprs -> herMAX (-> internally to maxsat) -> some final transform to paramita. This could be a lot more efficient than using our own pipeline for maxSAT solvers, but it does add an extra dependency for using paramita. We could perhaps make the dependency optional and if hermax is not installed we throw a warning an just transform the CPMpy exprs ourselves. Thoughts?