Re: [Help-glpk] [Fwd: Using a SAT solver other than MiniSAT]

[Andrew Makhorin]

> I have a problem (an encoding of the social golfers problem) that's 
> significantly faster in gplsol with MiniSAT than in glpsol with the 
> standard solver. But it's still slow on large instances and I'd like to 
> try it with some other SAT solvers.
> 
> I thought I'd use the --wcnf option to dump it to a file, then run that 
> manually in another SAT solver. But I get this error:
> 
> ---
> 
> $ glpsol --math socialgolf.ampl --wcnf sg.sat
> GLPSOL: GLPK LP/MIP Solver, v4.47
> Parameter(s) specified in the command line:
>   --math socialgolf.ampl --wcnf sg.sat
> Reading model section from socialgolf.ampl...
> 43 lines were read
> Generating OF...
> Generating FP...
> Generating LMP...
> Generating MO...
> Generating X...
> Generating Y...
> Model has been successfully generated
> glp_write_cnfsat: problem object does not encode CNF-SAT instance
> Unable to write problem in DIMACS CNF-SAT format
> 
> ---
> 
> It seems odd to me that I can solve it using the internal MiniSAT solver, 
> but not write it as a CNF-SAT instance. My reading of the documentation is 
> that there is some intermediate conversion step that turns the problem 
> into a SAT instance. 

Yes, your original instance is not cnf-sat, and to convert it to cnf-sat
glpsol performs some preprocessing.

> (The problem encoding uses integer arithmetic.) Is 
> there a glpsol option that will dump the problem after conversion to 
> CNF-SAT? If not, could one be added?

It would be meaningless to do that, because even you would have obtained
a solution to that transformed instance, you would not be able to
recover corresponding solution to the original instance not having
recovering information provided by the preprocessor.

Nevertheless, see the module glpk/src/glpapi19.c (a driver to minisat).
Problem object P passed to the routine glp_minisat1 is the internal
cnf-sat instance generated by the preprocessor--in principle, you can
write it to a text file in Dimacs format with the routine
glp_write_cnfsat and then try to solve it with an external solver.

> 
> Relatedly, if such an option were available, would it be easy for me to 
> interpret the result of the SAT solver in the context of the original 
> problem?
>