Are there any usable SAT solvers implemented in Sage?

[Zoresvit]

So I've found the CryptoMiniSat solver implementation (optional package) and managed to install it, but can't find any documentation on its' usage. Also I happend to find some mentions about different SAT solvers interfaces integrated into Sage but had problems with figuring out what is actually ready for use and how it can be used. I would appreciate any help and hints on using SAT solvers in Sage.

Thanks.