-------- Forwarded Message -------- From: Martin Lester <[email protected]> Reply-to: [email protected] To: [email protected] 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. _______________________________________________ Help-glpk mailing list [email protected] https://lists.gnu.org/mailman/listinfo/help-glpk
