Hi Robbie, > Version 4.46 introduced new APIs and new GLPSOL options > for CNF satisfiability problems. I would like to > update the GLPK wikibook accordingly and propose the > following changes -- please let me know if any of these > suggestions need revising: >
The following remark might be added: In glpk cnf-sat is considered as a special case of mip, where all variables are binary, and all constraints are covering inequalities. That is, a cnf-sat instance is stored in the problem object (glp_prob) as if it were mip instance. This, in particular, means that cnf-sat can be solved with glp_intopt, but glp_minisat1 being a problem-specific solver is much more efficient in this case. (I implemented a crude version of a 0-1 feasibility solver, which translates a mip to cnf-sat, calls the cnf-sat solver to find a feasible solution, and then transforms it to the solution of the original problem. This technique allows to attack hard combinatorial problems, which cannot be efficiently solved with the current version of glp_intopt. This was the main reason, for which I included the cnf-sat solver in glpk.) Best regards, Andrew Makhorin _______________________________________________ Help-glpk mailing list [email protected] https://lists.gnu.org/mailman/listinfo/help-glpk
