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

Re: SAT-Britney status and howto


Am Freitag, den 05.08.2011, 18:59 +0200 schrieb Philipp Kern:
> I beg to differ on calling darcs obscure.  I just said that we've
> already got infrastructure to handle git.  ;-)

Don’t worry, I was actually expecting to have to do that when I started
to hack on SAT-Britney, but for the initial hacking spree I waned the
least resistance. And darcs is nicer there :-)

> I tried running it on franck yesterday and it didn't get through the
> "relaxing testing to an installable state" step within two hours.  (No
> threading in clisp activated, plain SAT-Britney compiled on Debian
> unstable.)
> So I guess there's still some debugging needed?  Or is that a
> fundamental flaw of the used heuristics?

I don’t know what the problem is, just that it lies within the blackbox
MAX-SAT-solver. The SAT-Britney code did not change since the last days
of DebConf, and I doubt that testing has changed that radically. So the
sufficient performance of clasp seems to be an „accident“.

As you saw by CC, an author of a MAX-SAT solver has offered to GPL his
software if we need it, maybe he can handle the instance better. I am
also starting to collect interesting instances on


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: