Hi, 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 http://git.nomeata.de/?p=sat-britney.git;a=tree;f=problems;hb=HEAD 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