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

[Andrew Makhorin]

-------- Forwarded Message --------
From: Martin Lester <address@hidden>
Reply-to: address@hidden
To: address@hidden
Subject: Using a SAT solver other than MiniSAT
Date: Wed, 5 Dec 2012 23:32:18 +0000 (GMT)

Hi.

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. (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?

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?

Yours,

Martin Lester.