Problems with Solver::implies

99 views
Skip to first unread message

sascha...@gmail.com

unread,
Sep 24, 2018, 6:09:12 AM9/24/18
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.

sascha...@gmail.com

unread,
Feb 9, 2019, 12:24:33 PM2/9/19
to MiniSat
(Not much activity here...)

After putting it away for some time, i just tried the above toy-example with PyMiniSolvers (https://github.com/liffiton/PyMiniSolvers) which is a python-based wrapper.

This one works as expected, which means (although i did not analyze it yet), that i made some mistakes in the basic initialization/wrapping of variables/clauses in the C++ part. The function is not broken!

Example:

import minisolvers

S = minisolvers.MinisatSolver()

for i in range(4):
    S.new_var()

for clause in [1, 2], [3, 4], [-1, -2], [-3, -4]:
    S.add_clause(clause)

test1 = S.implies([1])
print(test1)

test2 = S.implies([1, 3])
print(test2)

which outputs:

array('i', [1, -2])
array('i', [1, 3, -2, -4])
Reply all
Reply to author
Forward
0 new messages