Assert Failure in SimpSolver::relocAll(ClauseAllocator& to)
25 views
Skip to first unread message
Andreas Morgenstern
Jan 12, 2012, 6:08:14 AM1/12/12
to MiniSat
Hello,
I'm currently implementing the "Property Directed Reachability
Algorithm" as described by Niklas Een et al using the Minisat Sat-
Solver .
There, I have to use many different SAT-calls using activation
literals.
However, at some point, my algorithm crashes because an assertion
fails:
the assertion is in SimpSolver::relocAll :
assert(subsumption_queue.size()==0).
Does anyone have a suggestion?
P.S. : I'm using the Github version of minisat
I'm currently implementing the "Property Directed Reachability
Algorithm" as described by Niklas Een et al using the Minisat Sat-
Solver .
There, I have to use many different SAT-calls using activation
literals.
However, at some point, my algorithm crashes because an assertion
fails:
the assertion is in SimpSolver::relocAll :
assert(subsumption_queue.size()==0).
Does anyone have a suggestion?
P.S. : I'm using the Github version of minisat
Andreas Morgenstern
Jan 12, 2012, 6:24:29 AM1/12/12
to MiniSat
Hello,
I think that issue was discussed before. Sorry I've overlooked it.
So I think we can close this discussion.
Andreas.
I think that issue was discussed before. Sorry I've overlooked it.
So I think we can close this discussion.
Andreas.
Niklas Sörensson
Jan 16, 2012, 4:31:10 AM1/16/12
to min...@googlegroups.com
Hello Andreas,
I'm afraid I still have not fixed this issue. I'll try to remember to
investigate this next week. In the meantime, did you find a workaround
so far?
Regards,
/Niklas
Andreas Morgenstern
Jan 17, 2012, 4:00:17 AM1/17/12
to MiniSat
Hello Niklas,
unfortunately I have not found a workaround.
I was quite busy with teaching a lecture,
so I was not able to work more on my project.
If you could fix it that soon this would be really great.
Andreas
unfortunately I have not found a workaround.
I was quite busy with teaching a lecture,
so I was not able to work more on my project.
If you could fix it that soon this would be really great.
Andreas
Niklas Sörensson
Jan 17, 2012, 5:24:24 AM1/17/12
to min...@googlegroups.com
Hello Andreas,
Well I've known about it for some time so it's not really soon :)
Anyway, something I forgot to ask. Are you using minisat with
preprocessing enabled? That's probably not a good idea in that
algorithm since it can not be expected to do much after the initial
CNF has been simplified. In my implementation of IC3/PDR I turn off
preprocessing at that point. That might be why I'm not seeing this
problem myself.
Regards,
/Niklas
Andreas Morgenstern
Jan 18, 2012, 2:29:46 AM1/18/12
to MiniSat
Hello Niklas,
Perhaps this is a possible workaround.
Anyway, it might also be the case that the Garbage Collection
happens in my implementation very often since I use it inside
of Microsofts .Net. So it might be the case that I ran
out of memory more quickly than you.
Andreas
> Well I've known about it for some time so it's not really soon :)
> Anyway, something I forgot to ask. Are you using minisat with
> preprocessing enabled? That's probably not a good idea in that
> algorithm since it can not be expected to do much after the initial
> CNF has been simplified. In my implementation of IC3/PDR I turn off
> preprocessing at that point. That might be why I'm not seeing this
> problem myself.
>
this is a good point. I'm going to try that.
> Anyway, something I forgot to ask. Are you using minisat with
> preprocessing enabled? That's probably not a good idea in that
> algorithm since it can not be expected to do much after the initial
> CNF has been simplified. In my implementation of IC3/PDR I turn off
> preprocessing at that point. That might be why I'm not seeing this
> problem myself.
>
Perhaps this is a possible workaround.
Anyway, it might also be the case that the Garbage Collection
happens in my implementation very often since I use it inside
of Microsofts .Net. So it might be the case that I ran
out of memory more quickly than you.
Andreas
Reply all
Reply to author
Forward
0 new messages