Made a Rage-Comic about D

Tobias Pankrath tobias at pankrath.net
Sat Jun 23 11:23:11 PDT 2012


On Saturday, 23 June 2012 at 17:47:04 UTC, d coder wrote:
> On Sat, Jun 23, 2012 at 10:58 PM, Tobias Pankrath 
> <tobias at pankrath.net>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.




More information about the Digitalmars-d mailing list