------------------------------------------------------------ To: Robbie Morrison <[email protected]> Subject: Re: GLPK wikibook update for CNF-SAT Message-ID: <1313527060.3234.30.camel@corvax> From: Andrew Makhorin <[email protected]> Date: Wed, 17 Aug 2011 00:37:40 +0400 ------------------------------------------------------------
> 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 Hello Andrew, hi all The following wikibook sections have been added or amended: http://en.wikibooks.org/wiki/GLPK/Mixing_GLPK_with_other_solver_packages#MiniSat_CNF-SAT_solver http://en.wikibooks.org/wiki/GLPK/Literature#Official_GLPK_documentation http://en.wikibooks.org/wiki/GLPK/Using_GLPSOL#Options http://en.wikibooks.org/wiki/GLPK/Using_the_GLPK_callable_library#Recently_added_GLPK_APIs http://en.wikibooks.org/wiki/GLPK/Reviews_and_benchmarks#Solver_capabilities The first link above includes Andrew's suggested material on the interface between MIP and CNF-SAT. Subscribers to this list should feel free to check and improve the above additions! The GLPK wikibook and the GLPK wikipedia page now record 4.46 as the latest version. --- One small thing. The output from $ glpsol --help could probably be improved. I suggest the CNF-SAT options be accorded their own section at the end, as they are rather specialist. Also the mandatory argument "filename" is missing in some cases. If Andrew agrees, I will submit a patch within the next week or so. with best wishes Robbie --- Robbie Morrison PhD student -- policy-oriented energy system simulation Technical University of Berlin (TU-Berlin), Germany University email (redirected) : [email protected] Webmail (preferred) : [email protected] [from Webmail client] _______________________________________________ Help-glpk mailing list [email protected] https://lists.gnu.org/mailman/listinfo/help-glpk
