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

[Andrew Makhorin]

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