On Saturday, 23 June 2012 at 17:47:04 UTC, d coder wrote:
On Sat, Jun 23, 2012 at 10:58 PM, Tobias Pankrath
<[email protected]>wrote:
I am currently writing a sat solver for educational purposes
How mature is the sat solver yet? Do you plan to release it at
some point
of time?
Regards
- Puneet
It was a DPLL with simple BCP yesterday and is a non functional
blob today :-).
I don't think I will push this to the state of the art. I plan
for a conflict driver clause learning solver, that chooses
variables like chaff and does non-chronological backtracking plus
2-watched-literal BCP.
IF I have enough time to do this. I'm new to sat and need to
understand all of the above first :-).
If you need a mature one, it seems that minisat can be easily
made available or ported to D. I'd do this, if it weren't for
educational purposes.
