Meeting at the Open Source Summit

[Patrick Franz]

Hello,

I'm a computer science student at the University of Gothenburg and planning to write my master thesis about this implementing a SAT-solver in the kernel configurator. The thesis will be supervised by Thorsten Berger and Sarah Nadi.

Since the exact direction and details of the thesis are not finalised yet, I was wondering if any of the interested developers will be attending the Open Source Summit in Edinburgh and if a meeting could be organised to discuss ideas, tools and possible collaboration.

Greetings, Patrick

[Josh Triplett]

On Sun, Oct 07, 2018 at 02:43:36PM -0700, Patrick Franz wrote:
> Since the exact direction and details of the thesis are not finalised yet,
> I was wondering if any of the interested developers will be attending the
> Open Source Summit in Edinburgh and if a meeting could be organised to
> discuss ideas, tools and possible collaboration.

I'll be at ELCE, and I'd be happy to talk with folks interested in
kconfig.

[Mate Soos]

Hey,

On 07/10/18 23:43, Patrick Franz wrote:

I'm a computer science student at the University of Gothenburg and planning to write my master thesis about this implementing a SAT-solver in the kernel configurator. The thesis will be supervised by Thorsten Berger and Sarah Nadi.

So this will be a Masters Thesis? I am a bit concerned about writing a new SAT solver from scratch -- and especially one that is somehow tuned to the kernel. There are plenty of very performant SAT solvers out there and making them tuned to the problem at kconfig would probably be a lot more fun and also a lot more useful in the general sense. Beating current SAT solvers at the top of the range is extremely difficult. I have burned over 100k of CPU hours and got 4th place this year at the competition. Unless you have similar amount of resources (note: everyone in the top ~20 do), it might be very difficult to get the to same speed. Besides, writing a new SAT solver from scratch is pretty complicated (I must confess, I could never do it). I think tuning a well-performing SAT solver to the kernel would be very interesting, though. Nowadays the MapleSAT* solvers seem to be doing pretty well, though I prefer CaDiCal (or my own solver, CryptoMiniSat, but really, CaDiCaL is amazing).

Anyway, just my 2 cents. It's your baby :) Good luck,

Mate

[Thorsten Berger]

Hi Mate,

No, that's not the plan, rather extending/adapting our conflict-resolution algorithms that rely on existing SAT solvers (replace 'implementing' with 'integrating' in his email). A large task will already be coming up with a sound and stable transformation of kconfig models to propositional logics. We were just wondering whether we it makes sense to send Patrick to the summit -- that is, whether there could be a dedicated meeting with relevant developers who can provide requirements and help guiding this effort (or even help with some implementation).

Best, Thorsten

--
Project details:
 
http://kernelnewbies.org/KernelProjects/kconfig-sat
---
You received this message because you are subscribed to the Google Groups "kconfig-sat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to kconfig-sat...@googlegroups.com.
Visit this group at https://groups.google.com/group/kconfig-sat.
To view this discussion on the web visit https://groups.google.com/d/msgid/kconfig-sat/a89c0960-2262-42e0-68e6-d35399a99b43%40gmail.com.
For more options, visit https://groups.google.com/d/optout.

-- 
Thorsten Berger
Associate Professor

Department of Computer Science and Engineering
Chalmers | University of Gothenburg, Sweden
http://www.cse.chalmers.se/~bergert
Tel.: +46 (0) 31 772 6075
Mob.: +46 (0) 729 746 246
Skype: tberger.work

[Patrick Franz]

Hi Josh,

Do you have any concrete ideas or suggestions ?

And do you happen to know others, who might be interested and who will be in Edinburgh ? 

/Patrick

[Mauro Carvalho Chehab]

Em Sun, 7 Oct 2018 14:43:36 -0700 (PDT)
Patrick Franz <patf...@gmail.com> escreveu:

I should be in Edinburgh, but my interest on it as only as a possible
user.

Btw, who admins this group? I need to replace my email there, as it
seems it is still pointing to an old email that will be de-comissioned
this week.

Regards,
Mauro