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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Date:	Mon, 17 May 2010 15:09:13 +0200
From:	Vegard Nossum <vegard.nossum@...il.com>
To:	Andi Kleen <andi@...stfloor.org>
Cc:	linux-kernel@...r.kernel.org, linux-kbuild@...r.kernel.org,
	Bart Massey <bart@...pdx.edu>, Michal Marek <mmarek@...e.cz>,
	Greg Kroah-Hartman <greg@...ah.com>,
	Ingo Molnar <mingo@...e.hu>,
	James Bottomley <James.Bottomley@...senpartnership.com>
Subject: Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

On 17 May 2010 14:13, Andi Kleen <andi@...stfloor.org> wrote:
> Vegard Nossum <vegard.nossum@...il.com> 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@...r.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/