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:

  1. Implement the iSAT interface.

  2. Provide the linking functions

  3. 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.

>>> import os
>>> os.environ['OPTILOG_SOLVERS'] = '/path/to/new/sat/solver/'
>>> from optilog.solvers.sat import NewSatSolver