search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
819 stars 181 forks source link

How to solve a minimization problem with this solver #451

Closed reza-2018 closed 6 years ago

reza-2018 commented 6 years ago

Hello I have a question, how to solve a minimization problem with this solver, in other words, is it essentially possible to do this with CMS? I've been able to model the optimization problem with cnf equations(pseudo boolean). And I have defined all the constraints as a cnf equation. Now I have a Cnf formula and I want to get the least possible answer. What do you have a suggestion for me?

Thank you Reza

msoos commented 6 years ago

You need to look at the literature, there is quite an extensive literature on this. I recommend using Google Scholar. CMS can do this, it needs to be used as a library, please see the README file, there is quite a bit of explanation on this. Please also see the cryptominisat5.h file, which has some more explanations. I would of course be happy if you could give your feedback here of your progress. However, I cannot help with writing this.

Good luck!