Re: [Toss-devel] F-First Normal Form
Status: Beta
Brought to you by:
lukaszkaiser
From: Lukasz K. <luk...@gm...> - 2010-07-22 16:59:02
|
Hi. > I've had a couple of days break :( , a couple of bugs I've worked out > and an overlooked idea I'll start working on after a nap. I'm > convinced now that TNF is too weak even for the solver -- I invite you > to look at "our new" normal form once I commit (it will be in Games > folder, Heuristic.ml/.mli, but if you so decide we can adapt it and > move it to the Solver folder). I'm not committing because there are > several failing Game tests which I want to look at first -- should I > commit? In which sense do you mean that TNF is too weak - for correctness (which would be a strong problem) or just for efficiency? Can you think of some examples? Anyway - operating on formulas is always complex, but it is worth to do it good. I will certainly consider it for the solver, but I'm in a middle of some other stuff (also sat-solver related) and it would be hard for me to look into it today or tomorrow. So perhaps try to make the tests work first in the next days and commit then, what do you think? It would be also nice if your code contained some nicely written paper-like comments (e.g. with lemmas) at the hard places, so that I can hope to understand it at least in the basic way. But this is for sure a very nice work, I hope it will work as nice :). Best! Lukasz |