[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: SAT-Britney status and howto



Hi,

Am Mittwoch, den 10.08.2011, 01:17 +0200 schrieb Philipp Kern:
> On Mon, Aug 08, 2011 at 11:18:21PM +0200, Joachim Breitner wrote:
> > Yesterday and today I did some more optimization, mostly to get memory
> > consumption down. Now it does one processing run on my laptop easily
> > within the 6GB of RAM I have, and finishes in 3min18, even in the mode
> > that breaks down the transition into multiple small bits. I’m happy
> > about that :-)
> 
> On --migrate I got several duplicates in the rationale why some
> package cannot migrate.  Is that just presentation or are some clauses
> actually duplicated?

somewhere in between. One such clause can generate more than one CNF
line. The solver (actually, Picosat.hs) returns the unsatisfied CNF
disjunctions. For each of them, we print the clause. So if multiple
conjunctions of one clause were unsatisfiable, then it was printed
multiple times.

It is fixed in git now, thanks for spotting it.

Greetings,
Joachim

-- 
Joachim "nomeata" Breitner
Debian Developer
  nomeata@debian.org | ICQ# 74513189 | GPG-Keyid: 4743206C
  JID: nomeata@joachim-breitner.de | http://people.debian.org/~nomeata

Attachment: signature.asc
Description: This is a digitally signed message part


Reply to: