status (SAT/UNSAT) should not be set from exit code, but from contents of answer?

[jwaldmann]

I am trying to use solver PRS (https://github.com/shaowei-cai-group/PRS-sc24/) .

Their exit code is 0 always.

$ /opt/PRS/sc24/bin/PRS check.cnf 
s SATISFIABLE
v -1 2 0
$ echo $?
0

$ /opt/PRS/sc24/bin/PRS uns.cnf
s UNSATISFIABLE
$ echo $?
0

Ersatz currently has

...
    (exit, out, _err) <-
      readProcessWithExitCode path [problemPath] options
    let sol = parseSolution5 out
    return (resultOf exit, sol)

resultOf :: ExitCode -> Result
resultOf (ExitFailure 10) = Satisfied
resultOf (ExitFailure 20) = Unsatisfied
resultOf _                = Unsolved

This is redundant, the status also is in the output, and we have to parse it anyway, to get the assignment.

I have some code for that, in a different project https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/master/src/Ersatz/Solver/Satcomp.hs?ref_type=heads that I should extract and present as a pull request here.

[RyanGlScott]

Indeed, I suspect that this works for most QBF solvers due to an exit code requirement imposed by various QBF competitions (e.g., QBFEVAL). I can certainly believe that not all solvers adhere to this convention.

That being said, I'm not sure what exactly you are proposing. Each solver already has specific treatment in ersatz (e.g., see the code for handling Z3, which does not use resultOf). Couldn't we just add a specific case for PRS that avoids the use of resultOf, similarly to how Z3 is handled?

[jwaldmann]

[NB: for the moment, I am looking at SAT, not QBF, but the same principle should apply.]

I want to avoid solver-specific code altogether. If there is something specific, then it should refence the input/output format required by a competition, possibly qualified with a year. Because I usually want solvers that performed well in recent competitions. The only exemption I am willing to grant :-) is for minisat which does not print the s and v characters at start of lines - because it pre-dates the current competition spec.

Concrete proposal: copy modules File, Path, Presatcomp, Satcomp from https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/tree/master/src/Ersatz/Solver?ref_type=heads to Ersatz. Then I can write

import qualified Ersatz.Solver.File as ESF
import qualified Ersatz.Solver.Satcomp as ESS

solver = ESF.path_with ESS.decode "/opt/PRS/sc24/bin/PRS"
     [ "nThreads=16", "clause_sharing=1", "preprocessor=1" ]

Ersatz should continue to export names like kissat but now defined as ESF.pipe_with ESS.decode "kissat" [].

[RyanGlScott]

That makes sense! I would welcome making this code more standardized. Of course, we should make sure to test each solver to make sure that it continues to work with the new approach.