Monday, January 16, 2012

Gasca (yet another CDCL sat solver)

I have release today another sat solver. Gasca is a pure CDCL (Conflict-Driven Clause-Learning) SAT solver written in Go. It was written before I joined Google in Oct. 2011 as a very short project to understand some alternatives to the ideas in my master thesis. Some pieces of code are inspired from Minisat or Cryptominisat, though Gasca is not a port to Go of neither of them.

Go ahead, clone my repository and try it out:

$ hg clone ssh://

I must say that I found Go very refreshing after writing my master thesis in Java. Go is not comparable to C when it comes to controlling every little aspect of the performance, so Gasca will never stand a chance against top SAT solvers. However, I felt that writing programs in Go is a breeze.