On Sun, Dec 21, 2008 at 10:56:57AM +0100, Matt Barringer wrote:
I am running into a problem where the satsolver is triggering an abort call in assert(dq.count > 1) in run_solver(). The comment above the call doesn't explain it:
/* dq.count < 2 cannot happen as this means that * the rule is unit */
What does a dq.count <= 1 mean, and what does that comment mean?
"dq" is a queue containing unresolved literals. dq.count is the number of elements on this queue. A rule is "unit" if all literals but one are False, and the last literal is undecided (see SAT solver theory). All "unit" rule should already be handled in the propagate() step, so they shouldn't turn up here. Please change the debug level so that the output includes SAT_DEBUG_PROPAGATE. The solver code will then dump the rule before aborting. Cheers, Michael. -- Michael Schroeder mls@suse.de SUSE LINUX Products GmbH, GF Markus Rex, HRB 16746 AG Nuernberg main(_){while(_=~getchar())putchar(~_-1/(~(_|32)/13*2-11)*13);} -- To unsubscribe, e-mail: zypp-devel+unsubscribe@opensuse.org For additional commands, e-mail: zypp-devel+help@opensuse.org