Re: SAT based britney
Hi,
On Thu, 26 May 2011 14:03:17 +0200, Raphael Hertzog <hertzog@debian.org>
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
Reply to: