Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Vegard Nossum]

On 17 May 2010 14:13, Andi Kleen <andi@xxxxxxxxxxxxxx> wrote:
> Vegard Nossum <vegard.nossum@xxxxxxxxx> writes:
>
>> I just wanted to say that I've been accepted into this year's Google
>> Summer of Code program and will spend this summer working on improving
>> the kconfig system in a very particular direction: I want to integrate
>> a proper boolean constraint satisfiability solver into the
>> configuration editors (menuconfig, etc.) in order to allow
>> partial/incomplete configuration specifications. In short, this means
>> that the user can choose to not specify a particular value for some
>> config options, but let the system deduce their values. This will
>> hopefully improve usability and also solve the select problem once and
>> for all.
>
> Nice idea. I read your proposal and it looks good.
>
> I assume you got inspired by the libzypp use of a SAT solver
> for package dependencies? ÂOne problem that is visible there
> is that it can be hard to display conflicts in a nice and understandable
> way to the user, especially if there are lots of dependencies.
>
> It might be worth planning in some time to solve that nicely.

Thanks! I didn't actually get inspired by libzypp -- but somebody else
mentioned it too, so I guess I should take a look!

You bring up a valid point, and I admittedly haven't given it VERY
much thought yet, but I think that conflicts could be displayed in the
following way: If an instance is unsolvable, then it means that all
possible valuations/assignments make at least one clause (disjunction)
false. Each clause is usually generated by exactly one dependency
specification (the "depends on" directive), so we could print these
dependencies to the screen as suggestions for how to resolve the
conflict.


Vegard
--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/