pg2455
pg2455

Reputation: 5148

Making C++ to use output from Python functions

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?

Upvotes: 1

Views: 91

Answers (1)

danny
danny

Reputation: 5270

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.

Upvotes: 2

Related Questions