Hi again, Am Freitag, den 05.08.2011, 22:05 +0200 schrieb Joachim Breitner: > 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. He replied, saying that he’ll look into it near the end of August. I managed to instrument the sat4j MAX-SAT solver. Unfortunately, the MAX-SAT part of sat4j is not packaged, but can be downloaded here: http://forge.ow2.org/project/showfiles.php?group_id=228 Using this, I manage to run SAT-Britney on today’s input files. If you are curious, here is the output: # easy apparmor/2.6.1-4 easy azureus/4.3.0.6-4 swt-gtk/3.7-2 # easy bugzilla/3.6.3.0-2 # easy connectomeviewer/2.0.0-1 easy flightgear/2.0.0-4 openscenegraph/3.0.0-2 fgrun/1.5.2-1/amd64 fgrun/1.5.2-1/armel fgrun/1.5.2-1/i386 fgrun/1.5.2-1/ia64 fgrun/1.5.2-1/mips fgrun/1.5.2-1/mipsel fgrun/1.5.2-1/powerpc fgrun/1.5.2-1/s390 fgrun/1.5.2-1/sparc ossim/1.7.21-3/amd64 ossim/1.7.21-3/armel ossim/1.7.21-3/i386 ossim/1.7.21-3/ia64 ossim/1.7.21-3/mips ossim/1.7.21-3/mipsel ossim/1.7.21-3/powerpc ossim/1.7.21-3/s390 ossim/1.7.21-3/sparc easy gammu/1.30.0-2 libdbi/0.8.4-5.1 icinga/1.4.2-1/amd64 icinga/1.4.2-1/armel icinga/1.4.2-1/i386 icinga/1.4.2-1/ia64 icinga/1.4.2-1/mips icinga/1.4.2-1/mipsel icinga/1.4.2-1/powerpc icinga/1.4.2-1/s390 icinga/1.4.2-1/sparc rrdtool/1.4.3-3.1/kfreebsd-i386 rrdtool/1.4.3-3.1/sparc syslog-ng/3.2.4-1/amd64 syslog-ng/3.2.4-1/armel syslog-ng/3.2.4-1/i386 syslog-ng/3.2.4-1/ia64 syslog-ng/3.2.4-1/kfreebsd-i386 syslog-ng/3.2.4-1/mips syslog-ng/3.2.4-1/mipsel syslog-ng/3.2.4-1/powerpc syslog-ng/3.2.4-1/s390 syslog-ng/3.2.4-1/sparc # easy geogebra/3.2.47.0+dfsg1-1 # easy hurd/20110519-3 easy libcitygml/0.1.3+r114-2+3p0p0 openscenegraph/3.0.0-2 fgrun/1.5.2-1/amd64 fgrun/1.5.2-1/armel fgrun/1.5.2-1/i386 fgrun/1.5.2-1/ia64 fgrun/1.5.2-1/mips fgrun/1.5.2-1/mipsel fgrun/1.5.2-1/powerpc fgrun/1.5.2-1/s390 fgrun/1.5.2-1/sparc ossim/1.7.21-3/armel ossim/1.7.21-3/i386 ossim/1.7.21-3/ia64 ossim/1.7.21-3/mips ossim/1.7.21-3/mipsel ossim/1.7.21-3/powerpc ossim/1.7.21-3/s390 ossim/1.7.21-3/sparc # easy libgcrypt11/1.4.6-8 easy swt-paperclips/1.0.4-1 swt-gtk/3.7-2 easy opensaml2/2.4.3-1 xml-security-c/1.6.1-1 xmltooling/1.4.2-1 easy sipwitch/1.0.3-1 ucommon/5.0.4-2 easy swt-gtk/3.7-2 swtcalendar/0.5-1 easy swt-gtk/3.7-2 trident/1.3+dfsg-5 # easy pd-hid/0.7-1 # easy python-chaco/4.0.0-1 # easy python-enable/4.0.0-1 # easy python-gearman/2.0.2-2 # easy psyco-doc/1.6-2 # easy xfonts-terminus/4.35-1 easy swt-gtk/3.7-2 zekr/1.0.0+repack-5 Unfortunately, it does not work here wihtout swapping. If my mahcine starts to swap, then the memory holding the font data gets corrupted, so I can hardly read the above text (or any typos in this mail), and I need to reboot to fix this. Since it is late, I’ll just shut down and call it a day. Maybe sat4j is the right way, given tat it is most likely the most industry-proven solver. Also, it supports a timeout option which would abort after a certain number of seconds or minutes _and_ output the best solution found so far. Since optimality is not as important for us as reliable termination, this sounds attractive. And it would probably makes the release team with the most diverse programming language zoo in within their tools :-) 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