Dear Manuel, I’d like to come back to your offer. End of July, when I wrote to you the last time, clasp was just fine to solve our maxsat problems, our analysis took a total of 7 minutes. But for the last two days, it seems to be unable to come to an end, not even after a few hours, while the non-free msuncore solver solves it within seconds. Nothing radical has changed in the input, as far as I know. It seems that clasp’s performance depends on factors likely to change from one day to another. My code now preprocesses the SAT problem and eliminates variables whose value is forced by a one-variable clause. Hence the problem becomes much smaller in size, so you might not need to have adapt your code too much. You can fetch the problem in WCNF format here: http://git.nomeata.de/?p=sat-britney.git;a=blob_plain;f=problems/relaxation-2011-08-04.wcnf;h=ddeafff8e80ef7f27362930752d7aa2a862c38b9;hb=HEAD If your solver can handle this in reasonable time, please let us know. Thanks, Joachim Am Freitag, den 29.07.2011, 16:58 +0200 schrieb Joachim Breitner: > Dear Manuel, > > thanks for your offer. I was pointed to clasp, which seems to be > something else but can solve MAX-SAT instances as a side effect, and > that even faster than the ones I was using before. Also, I found that > preprocessing the instances in my code, e.g. removing all variables that > are fixed (by clauses with only and exactly that variable) makes the > problems much smaller so that speed and size are not too big of a > problem any more. > > So for the moment, it seems that I’m set. If it turns out that clasp > does not work for me after all, I’ll come back to you. > > Thanks again, I’m glad to see that Free Software is not totally unknown > in Academia, > Joachim > > > Am Freitag, den 29.07.2011, 16:51 +0200 schrieb Manuel López-Ibáñez: > > Hi Joachim, > > > > We have a Weighted-SAT solver based on Tabu Search. It is pretty fast but it > > has an initialization phase that requires 6GB because it is hard-coded for not > > so many but very long clauses, while your example is many but very short > > clauses. I think I can modify it to not require that absurd amount of memory > > but it may take a few weeks to do it and test it (and summer holidays are coming). > > > > The code is C and not too complex, and in total > > (main+input+output+timing+rng+comments) is about 1500 lines. > > > > We are happy to release the source code as GPL2, but I don't want to invest the > > effort if you already found a solution or you don't think you can wait until > > September. > > > > We also would be interested in having more instances to play with, and tuning > > the algorithm for the kind of problem that Debian needs to solve. > > > > Please, let me know your thoughts about this. > > > > Sincerely, > > > > Manuel López-Ibáñez. > > > > > > > > > > > > > > > -- 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