search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

MaxSAT in SBV (or assert-soft) #512

Closed arrowd closed 4 years ago

arrowd commented 4 years ago

It seems that problem I'm solving is "MaxSAT" one, as suggested in https://stackoverflow.com/a/61227096/637669

Can SBV be used to solve such problems? I'd also appreciate general feedback on my SO question.

LeventErkok commented 4 years ago

Yes, optimization and assert-soft are both supported by SBV.

Assert-soft is called softConstrain in SBV. Defined here: http://hackage.haskell.org/package/sbv-8.6/docs/Data-SBV.html#v:softConstrain

Here's an example: http://hackage.haskell.org/package/sbv-8.6/docs/Documentation-SBV-Examples-Misc-SoftConstrain.html

In general, MaxSAT is done through optimization in SBV: http://hackage.haskell.org/package/sbv-8.6/docs/Data-SBV.html#g:45

One thing to keep in mind that you cannot mix query mode and optimization in SBV. (That is, if you want optimization goals, then calls to query will be rejected. There are technical reasons for this.)

But looks like all you need are softConstrain calls, which should work fine with queries. If you need actual optimization (i.e., minimizing/maximizing a measure), then you'll have to formulate it without using the query feature.

arrowd commented 4 years ago

I was reading SBV's documentation so many times and was missing softConstrain all the time ._.

Sorry for the noise and thanks again.