Hello Andrew 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:
--- http://en.wikibooks.org/wiki/GLPK/Mixing_GLPK_with_other_solver_packages#MiniSat CNF-SAT solver NEW SECTION (INTERNAL AND EXTERNAL LINKS TO BE ADDED) As from version 4.46, GLPK bundles the MiniSat CNF-SAT (conjunctive normal form satisfiability problem) solver developed by Niklas Eén and Niklas Sörensson at Chalmers University of Technology, Sweden. MiniSat's permissive MIT license allows it to be distributed as part of GLPK. A satisfiability (SAT) problem involves determining if a given boolean formula can evaluate TRUE through a suitable assignment of its variables. The conjunctive normal form (CNF) indicates restrictions on the way the boolean formula is expressed. Boolean formulas expressed in other ways are convertible to CNF. The official GLPK documentation file doc/cnfstat.pdf contains a full reference for the use of CNF-SAT problems. That material is therefore not repeated here. See obtaining GLPK. GLPK reads and writes CNF satisfiability problems in DIMACS format. Certain restrictions are placed on the problem specification so that it remains a valid CNF-SAT problem. These restrictions can be explicitly checked with the 'glp_check_cnfsat' public call and are automatically checked when the --minisat option is deployed. --- http://en.wikibooks.org/wiki/GLPK/Literature#Official_GLPK_documentation UPDATE DOCUMENTATION TABLE ACCORDINGLY doc/cnfsat.pdf --- http://en.wikibooks.org/wiki/GLPK/Using_GLPSOL ADD NEW OPTIONS --cnf filename read CNF-SAT problem instance in DIMACS format from filename and translate it to MIP --wcnf filename write CNF-SAT problem instance in DIMACS format to filename --minisat solve CNF-SAT problem instance with MiniSat solver --- http://en.wikibooks.org/wiki/GLPK/Using_the_GLPK_callable_library#Recently_added_GLPK_APIs ADD THE NEW APIS 4.46 glp_read_cnfsat read CNF-SAT problem data in DIMACS format glp_check_cnfsat check for CNF-SAT problem instance glp_write_cnfsat write CNF-SAT problem data in DIMACS format glp_minisat1 solve CNF-SAT problem instance with MiniSat --- http://en.wikibooks.org/wiki/GLPK/Reviews_and_benchmarks#Solver_capabilities ADD FEATURE + inclusion of the MiniSat solver for CNF satisfiability problems --- http://en.wikibooks.org/wiki/GLPK/GLPK_file_extensions NO CHANGES REQUIRED --- with best wishes 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
