How to add a new solver to OptiLog
This framework provides a quick and easy way to make a wrapper for a new solver that allows its use from a Python environment.
To do it, three steps must be followed:
Implement the iSAT interface.
Provide the linking functions
Compile the solver as a library (a Linux shared object)
Implementing the iSAT interface
Please, checkout the OptiLogFrameworkInterface repository to download the interface.
The interface source code can be found in the FrameworkInterface
directory.
The most important files are isat.hpp
, parameter.hpp
and pyexceptions.hpp
.
First of all, you have to implement the iSAT interface.
You do not need to implement the whole interface; only the methods you need.
A method not implemented will throw a NotImplementedException
.
Let see an example of an implementation:
In this example we will see how to make a basic implementation of the the Cadical 1.0.3 solver.
The first thing we will do is declare a C++ class that will act as a wrapper of the Cadical SAT solver.
solver.hpp
#include <vector> #include "isat.hpp" #include "cadical/cadical.hpp" class CadicalWrapper : public iSAT { public: CadicalWrapper(); virtual ~CadicalWrapper(); void addClause(const std::vector<int>& literals) override; E_STATE solve(const std::vector<int>& assumptions) override; unsigned int getNumClauses() override; unsigned int getMaxVar() override; void getModel(std::vector<int> &model) override; private: CaDiCaL::Solver * solver = new CaDiCaL::Solver; };We will also provide an implementation for all the defined methods:
solver.cpp
#include "solver.hpp" CadicalWrapper::CadicalWrapper() { solver = new CaDiCaL::Solver; } CadicalWrapper::~CadicalWrapper() { delete solver; } void CadicalWrapper::addClause(const std::vector<int>& literals) { for (auto i = literals.begin(); i != literals.end(); ++i) { solver->add(*i); } solver->add(0); } E_STATE CadicalWrapper::solve(const std::vector<int>& assumptions) { for (auto i = assumptions.begin(); i != assumptions.end(); ++i) { solver->assume(*i); } return (solver->solve() == 10 ? E_STATE::SAT : E_STATE::UNSAT); } unsigned int CadicalWrapper::getNumClauses() { return solver->irredundant() + solver->redundant(); } unsigned int CadicalWrapper::getMaxVar() { return solver->vars(); } void CadicalWrapper::getModel(std::vector<int> &model) { int maxvar = solver->vars(); for(int i = 1; i <= maxvar; ++i) { int lit = solver->val(i) > 0 ? i : -i; model.push_back(lit); } }
The Linking Functions
The optilogcinterface.hpp
defines two macros that automatically define the linking functions for OptiLog.
First, we will tell OptiLog how to instantiate and destruct our newly created SAT solver.
We will do this by adding the following code at the end of the solver.cpp file:
#include "optilogcinterface.hpp" OPTILOG_C_INTERFACE(CadicalWrapper, "Cadical")
The first parameter to the OPTILOG_C_INTERFACE macro is the name of the class that implements the iSAT interface. The second parameter is the name of the SAT solver that is going to be exported to Python.
Optionally, you can provide a vector that specifies the configurable options of the SAT solver on the set
and get
method calls.
See:
#include "optilogcinterface.hpp" std::vector<OptilogConfigParameter> configurableParameters { OptilogConfigParameter("arena", 0, 1, 1), OptilogConfigParameter("arenacompact", 0, 1, 1), //... OptilogConfigParameter("walknonstable", 0, 1, 1), OptilogConfigParameter("walkredundant", 0, 1, 0), OptilogConfigParameter("walkreleff", 0, 1000, 20) }; OPTILOG_CONFIG_C_INTERFACE(configurableParameters)
The OptilogConfigParameter
objects expose a name
, lower_bound
, upper_bound
and default
parameters.
You can find the corresponding source code on configparameter.hpp
.
Compiling as a library
We will compile the Cadical solver with gcc
. The only requirements for this step are:
The solver must be compiled with position independent code (-fPIC flag)
The solver must be compiled as a shared library (-shared flag)
No symbols related to the iSAT interface must be undefined. Recommended: Compile with
-Wl,--no-undefined
to make sure that the solver includes the source files for for*.cpp
files of the FrameworkInterface.Include
-lm
,-lstdc++
and other libraries as necessary.
Here is a compilation example command:
> gcc -fPIC -shared -Wl--no-undefined -O2 -I ./<path/to/Cadical> -I ./<path/to/Cadical> -I /<path/to/FrameworkInterface> <! Every .cpp file in the cadical directory !> /<path/to/FrameworkInterface>/configparameter.cpp /<path/to/FrameworkInterface>/isat.cpp /<path/to/FrameworkInterface>/parameter.cpp /<path/to/FrameworkInterface>/pyexceptions.cpp -o ./build/libcadical.so -lstdc++ -lm
Note
You can copy the files in the FrameworkInterface into your working environment. However, these files should not be edited
Loading the solver
When imported, OptiLog will check for solver libraries in the following locations:
The solvers already distributed with OptiLog (
<optilog-installation/sat/solvers>
)The solvers on
~/.optilog_solvers
Each location on the environment variable OPTILOG_SOLVERS. The paths are separated like PATH environment variable (with ‘:’).
If you are developing a new SAT solver, simply copying the library to ~/.optilog_solvers
will work!
The solvers are imported when the optilog.solvers.sat
module is loaded. If you want to modify the environment variables with python code, make sure to do it before
actually importing your solvers.
1import os
2os.environ['OPTILOG_SOLVERS'] = '/path/to/new/sat/solver/'
3from optilog.solvers.sat import NewSatSolver