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

[Robbie Morrison]

------------------------------------------------------------
To:           Robbie Morrison <address@hidden>
Subject:      Re: GLPK wikibook update for CNF-SAT
Message-ID:  <address@hidden>
From:         Andrew Makhorin <address@hidden>
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) : address@hidden
Webmail (preferred)           : address@hidden
[from Webmail client]