Reputation: 5148
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
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