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?
variableandvalue. 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