[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Robbie Morrison
Subject: Re: [Help-glpk] GLPK wikibook update for CNF-SAT
Date: Thu, 18 Aug 2011 22:08:33 +1200 (NZST)
User-agent: SquirrelMail/1.4.17

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:

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 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]

reply via email to

[Prev in Thread] Current Thread [Next in Thread]