[Help-glpk] GLPK wikibook update for CNF-SAT

[Robbie Morrison]

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) : address@hidden
Webmail (preferred)           : address@hidden
[from Webmail client]