Hi, On Thu, 26 May 2011 14:03:17 +0200, Raphael Hertzog <[email protected]> wrote: > On Thu, 26 May 2011, Joachim Breitner wrote: >> Am Donnerstag, den 26.05.2011, 11:58 +0200 schrieb Raphael Hertzog: >> The rationales for this separation: >> * Layer 1 needs to be fast, so eventually it is likely implemented in C >> using the picosat library. > > For now, I'm just calling the picosat executable. What improvement do you > expect by switching to the library?
Remember that to actually implement PMAX-SAT in the iterative way I suggested earlier, we'd need to run picosat repeatedly. Using the picosat library might save some time there, and possibly make it easier to start the search from the current assignments to the atoms, which also might speed things up. But this is a minor detail and can be postboned to when we actually have to worry about performance and after the interfaces are fixed. > I guess it might be more convenient (or even required) for the part where > you try to get an answer to "why did this package not migrate". But I fear > that switching to the library means we're loosing a clear interface for > people who want to provide an alternative layer 1. At least we must be > careful to keep a reasonable abstraction on top of it. The interface for layer 1 is a dimacs file with CNF clauses (just like for picosat) + the set of desired atoms -- whether it is implemented as a python script calling picosat, or a C program linking to picosat does not matter. (I guess we still need to clarify our layering more, as there seems to be some confusion). >> * Implementing the layer 1 interface might be interesting for >> non-Debian-related research parties whose result might be faster than >> anything we come up with. They will likely not want to worry about our >> human-readable syntax. > > Somehow this is already the case since we can use any SAT solver provided > we express our problem with a DIMACS file. Or do you expect them to work > specifically on the MAX-SAT problem that we want to implement on top of a > normal SAT solver? Correct. MAX-SAT (or, more precise, PMAX-SAT) is what we want to use. Our implementation based on SAT is just to get something working quickly, but I suspect that by tackling PMAX-SAT directly, better performance can be achieved. > Speaking of languages, I picked python because britney2 is in python, > because we have python-apt, and several members of the release team > seem to know/use/appreciate python. > > I know Perl & C too, but I'm afraid I don't know Ocaml & Haskell. > > I am aware that Ocaml could have been interesting due to its dose3 library. Of course there is no _right_ answer. One more reason for good layering: Assume layer 1 in C (due to speed), layer 2 in Haskell (due to the ease it manipulates expression trees andits good parsing libraries) and layer 3 in python (good debian-specific libraries and here is the code that the release team might want to modify if some constraints change, or additional suites are to be considered). Greetings, Joachim -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/06c6984bb27f34b3fd028c75bc9e8c73@localhost
