Mailinglist Archive: zypp-devel (62 mails)

< Previous Next >
Re: [zypp-devel] dq.count <= 1
  • From: Michael Schroeder <mls@xxxxxxx>
  • Date: Mon, 22 Dec 2008 13:36:49 +0100
  • Message-id: <20081222123649.GA2995@xxxxxxx>
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@xxxxxxx
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@xxxxxxxxxxxx
For additional commands, e-mail: zypp-devel+help@xxxxxxxxxxxx

< Previous Next >
List Navigation
Follow Ups
References