1

This is more of an engineering design question. MiniSAT is the base library to solve SAT problems. It has lots of optimizations already built-in. I am currently working on speeding up a part of that code. However, my code is written in Python, and I want C++ code to use the output from my code to use in its execution.

I have been thinking of writing a wrapper of C++ code in MiniSAT to be called from within python.

Here is the code that I am concerned with: https://github.com/niklasso/minisat/blob/master/minisat/core/Solver.cc

Lit Solver::pickBranchLit()
{
Var next = var_Undef;

// Random decision:
if (drand(random_seed) < random_var_freq && !order_heap.empty()){
    next = order_heap[irand(random_seed,order_heap.size())];
    if (value(next) == l_Undef && decision[next])
        rnd_decisions++; }

// Activity based decision:
while (next == var_Undef || value(next) != l_Undef || !decision[next])
    if (order_heap.empty()){
        next = var_Undef;
        break;
    }else
        next = order_heap.removeMin();

// Choose polarity based on different polarity modes (global or per-variable):
if (next == var_Undef)
    return lit_Undef;
else if (user_pol[next] != l_Undef)
    return mkLit(next, user_pol[next] == l_True);
else if (rnd_pol)
    return mkLit(next, drand(random_seed) < 0.5);
else
    return mkLit(next, polarity[next]);
}

I want the Python function to be used in C++ whenever pickBranchLit() in C++ is called. I also want Python to get return from C++ code about the current state of variables. I want to test the performance of the solver when the heuristics that I designed in Python are used.

This is my first time dealing with Python wrappers around C++, so I am not confident about my solution. Here is what I have been thinking:

C++ Function:

Lit Solver::pickBranchLit()
{
 // wait for python to return (variable, value) to assign
 // update the order_heap
 // return mkLit(variable, value)
}

Python fucntion:

CNF = get_cnf(filename)
c_solver.solve(filename) # loads up CNF in C++
while True:
  # python function to decide variable and the value to assign
  variable, value = python_decide_variable(CNF) 

  # this one calls C++ pickBranchLit 
  result, new_variables, values = python_sat_solver.assign_value(variable, value) 

  if result == "SATISFIABLE":
     break

I am a c++ noob, however, I have a good hold of Python. Is my design correct? How can I change the C++ pickBranchLit code to listen to Python?

1
  • I don't really follow which bit of your C++ function obtains/uses variable and value. It is certainly possible to call Python functions from C++ and this is likely to be better approach than running a continuous loop and watching for global variables to update Commented Jan 18, 2018 at 17:47

1 Answer 1

2

It is not really possible to use Python variables in C++, they need to be converted to an appropriate C++ type. For native types, Cython does this automatically by copying the value.

In your case, you want a C++ function to accept Python arguments. That means modifying Solver::pickBranchLit to accept arguments for the variables it uses.

The other option is to implement pickBranchLit in Python and return a Lit C++ structure as returned by the C++ pickBranchLit. This can then be used in the rest of C++ functions as-is.

This option is likely the easiest - as you are already using Python to generate values used by pickBranchLit, modifying its C++ code to accept those values as arguments will not yield any performance benefit.

To be able to return Lit structures from Python, will need to write a Cython wrapper for the structure, eg:

cdef extern from "SolverTypes.h" namespace "Minisat":
    ctypedef int Var
    struct Lit:
        int     x
        # Use this as a constructor:
        Lit mkLit(Var, bool)

Then in Cython code can use mkLit(int_from_py, <True/False>) to create a Lit structure that can be used to call C++ code.

What C++ functions you will need to call from Cython code also need wrappers written - see Wrapping C++ documentation for examples.

Sign up to request clarification or add additional context in comments.

2 Comments

Thanks a lot for your advice!! I have been working on implementing those functions. Meanwhile, I heard someone talking about usng ZMQ type libraries to do message passing between C++ and Python. Do you happen to have some idea about it?
Passing messages is mostly useful for distributed systems. For calling a library on the same machine they would incur a lot more overhead than simple C-API wrappers like what Cython produces. Depends on the use case.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.