sascha...@gmail.com
unread,Sep 24, 2018, 6:09:12 AM9/24/18Sign in to reply to author
Sign in to forward
You do not have permission to delete messages in this group
Sign in to report message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to MiniSat
Greetings!
I'm trying to experiment with the general idea of `Bacchus, Fahiem. "GAC via unit propagation` (with the goal of using Minisat as propagator within some Constraint-Programming solver).
After finding another post in this group, `On how to sub-utilize Minisat as a dumb, efficient, complete propagator` i was happy to find `Solver::implies` with the same definition as proposed in the discussion. Remark: I'm using core/Solver.cc and not simp/SimpSolver.cc.
Now, based on the paper above, i'm trying to use UP to prune some Integer-Domains. But implies does not work as (I) expected.
A simple example would be something like the following. Keep in mind, that this is somewhat wrapper-based usage of Minisat and therefore i got 1-indexing and different types. This part should work as expected.
SATSolver sat;
// 2 variables with domains {0, 1}
sat.newVar(); // var0 = 0
sat.newVar(); // var0 = 1
sat.newVar(); // var1 = 0
sat.newVar(); // var1 = 1
// at least 1
sat.addClause(std::vector<int> {1, 2});
sat.addClause(std::vector<int> {3, 4});
// at most 1
sat.addClause(std::vector<int> {-1, -2});
sat.addClause(std::vector<int> {-3, -4});
Calling sat.solve() works as expected and gives me (again: wrapped usage):
restarts : 1
conflicts : 0 (0 /sec)
decisions : 2 (0.00 % random) (602 /sec)
propagations : 4 (1204 /sec)
conflict literals : 0 (-nan % deleted)
Memory used : 20.07 MB
CPU time : 0.003321 s
solve status: 1
sol
1 | 0 | 1 | 0 |
Now, when trying to use Solver::implies, pretty much nothing is done. Starting from a fresh model (not after solve()):
std::vector<int> out;
sat.implies(std::vector<int> {1}, out);
always returns FALSE and an empty vector, where, i expected TRUE and [-2].
When adding some debug-prints to Minisat, i'm seeing, that the following code-part of Solver::implies leads to some early-stopping:
if (value(a) == l_False){
cancelUntil(0);
return false;
So it seems, some of my variables have a value of FALSE. Debugging further, the following:
std::cout << " MINISAT: implies called" << std::endl;
std::cout << " MINISAT: nFreeVars: " << nFreeVars() << std::endl;
std::cout << " MINISAT: nAssigns: " << nAssigns() << std::endl;
results in:
MINISAT: implies called
MINISAT: nFreeVars: 2
MINISAT: nAssigns: 2
which i don't understand. This is a fresh model obtained after only calling: newVar, addClause and then implies. Calling simplify before implies does not make a difference.
So i'm trying to understand here, if i somehow invalidated some invariants or did something else wrong. I'm not sure what Minisat expects here and why a fresh model has already assigned variables. I can't tell if Minisat did already some hidden work (it should not be possible to achieve anything without doing decisions) or if this is due to uninitialized memory (although the behavior looks deterministic). I wanted to add a new dummy decisionLevel() (without very much understanding the consequences), but it looks like it's not an API-call / protected and so i was not able to do so.
Any ideas on how i should proceed?
Thank you!
- Sascha
PS: If someone has experimented with this usage-idea (SAT as Propagator) and has some input/code i would be very interested.