search

FlorentAvellaneda / EvalMaxSAT

State-of-the-art MaxSAT Solver & Library Based on Unsat Core Guided Techniques
GNU General Public License v3.0
14 stars 4 forks source link

Is using specific SAT solver (ParaFROST) for EvalMaxSAT simple or nontrivial? #7

Closed realharryhero closed 1 month ago

realharryhero commented 2 months ago

(This "issue" is more of a question; sorry if it's not so well-phrased.)

Hello,

The ParaFROST SAT solver gains great speedups compared to other SAT solvers using GPUs; this solver takes in a .cnf file and outputs another, and can use both parallel CPUs and (one) GPU to gain large speedups. An idea would be to replace CaDiCaL with this new GPU solver, but the main issue is that ParaFROST does not "build" in the conventional sense but installs through an install.sh script, where one part of it is building the main solver.

Considering ParaFROST's "interface" is simple (it only takes in a .cnf file through its binary), is it simple to just place ParaFROST's binary where CaDiCaL is?

FlorentAvellaneda commented 2 months ago

Hello,

The SAT solver included in EvalMaxSAT is called numerous times and incrementally, and I am concerned that if the interface requires writing the formula to a file and then executing an external binary to solve the formula, it will take too much time (and the learned clauses from one call to another will also be lost). Additionally, it is not enough to know whether the formula is true or false; in the case where the formula is false, it is necessary to extract an unsat core.

Therefore, to use ParaFROST instead of CaDiCaL, it should be used as a library to benefit from its capability as an incremental solver, and the functionality to extract an unsatisfiable core when the formula is not SAT must be implemented (if this functionality is not already present in ParaFROST).

realharryhero commented 1 month ago

Sorry for the late reply; thank you for the explanation!