[Top][All Lists]

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

Re: [Help-glpk] cnf-sat solver interface

From: Andrew Makhorin
Subject: Re: [Help-glpk] cnf-sat solver interface
Date: Thu, 25 May 2017 10:10:38 +0300

> > > I wouldn't like to include a C++ code in glpk. It seems to me that a
> > > better way would be to add an API routine that allows to set up an
> > > user-provided CNF-SAT solver (which is, for example, minisat by
> > > default).
> > 
> > My plan is to link with the library that provides a C interface.
> > However, when I looked at it a few months ago, the semantics of the
> > interface looked a bit different to those of the current code so this
> > was not so easy to test quickly.
> > 
> CNF-SAT is a very important class of combinatorial problems, so maybe it
> would be reasonable to include in glpk a program object, say, glp_cnf,
> available on api level, and use it as an interface to CNF-SAT solvers.
> Another way is to use glp_graph, since CNF-SAT can be represented as a
> bipartite graph.

BTW, you may look at glpk/src/glpspm.h. The internal program object SPM
(general sparse matrix) is suitable to represent CNF-SAT, where rows
represent clauses and columns represent Boolean variables. 

reply via email to

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