MiniSat getting intermediate assignments

[pg2...@columbia.edu]

Hi,

Note: A complete C++ noob here!!

I have been stuck for last 2 weeks in getting the desired behaviour from MiniSat. I want to use my own variable selection heuristics ( my understanding is that I need to alter Solver::pickBranchLit).

The variable selection heuristics algorithm is in Python. I want C++ code to read the variable-value pair to branch from a text file where the Python code writes. I want C++ code to run everything normally until it needs to decide a new variable for branching (i.e progress to a new decision level). At this point, I want the C++ code to write newly assigned variables in a separate text file which will be read by Python code. The python code then decides new variable to branch.

I have been trying to get C++ code to write the variables assigned so far, but I am unable to wrap my head around the current state of variables.

I have tried (at several code points in Solver.c):

for(int i = 0; i < nVars(); i++){
std::cout << i << toInt(model[i]) << std::endl;
std::cout << i << toInt(assumptions[i]) << std::endl;
}

Both the model and assumptions variable have a size of 0 everywhere in the code. I am out of ideas regarding where the code is storing its current state of assigned variables. Can anyone help me with this? I might not be able to get the correct idea of how the code is working.

I hope I am clear in my explanation.

[Norbert Manthey]

Dear  Prateek,

from your code snippet and your description, you want to pick a decision literal based on the current model, correct? For this, writing only the trail (the current partial assignment) should be sufficient, e.g.
for(int i = 0 ; i < trail.size(); ++i) cout << (trail[i] == l_True ? var(trail[i]) + 1 : - var(trail[i]) - 1) << endl;

I wonder how you want to return the decision from python to the SAT solver, via cin? As an alternative (which might require you learning some more C/C++) I suggest you add a function to the IPASIR[0] interface (similarly to the function to share learned clauses), whose package supports Minisat, and then make use of thy pyIPASIR[1] package to get the solver linked against your python project. While the former should work, the latter would considerably improve the performance you would get out of that approach. For a proof of concept I would stick to the former.

I hope this brings you a little forward.
Best,
Norbert

[0]:https://github.com/biotomas/ipasir
[1]:https://github.com/marcogario/ipasir

[pg2...@columbia.edu]

Hi Norbert,

Thanks a lot for your reply. I am currently thinking of using a text file to use as an input, but if the POC works I will switch to IPASIR. Thanks for the suggestion!! I wouldn't have known otherwise.

Your code is giving an error since Lit (trail[i]) is being compared to lbool(l_True). I am still unclear about the way literals are represented in the code. I see that var(Lit) is right-shifting the bytes by 1 which is equivalent to multiplying the variable number by 2. Why is that necessary?

Thanks for suggesting to look into trail. I think I am starting to get hold od this code.

[Norbert Manthey]

Hi,

I mixed up trail and assignment. It has to be sign(trail[i])? -var(trail[i])-1 : ..., as the trail stores literals Lit, and not lbool.

The shifting is done because minisat represents literals like this. External literal e for a variable v is stored as variable v-1. If e is positive, the internal literal value is 2×v, if e is negative, the internal representation holds 2×e+1. The least significant bit holds the sign of the literal. Reading through the SolverTypes.h file should help to understand the details.

Best,
Norbert