MapleSAT
MapleSAT is the solver we used in our work on the Hadamard conjecture. The key innovation of the Maple series of solvers is the use of the learning rate branching heuristic (LRB), a departure from the VSIDS branching heuristic that has been the status quo for the past decade of SAT solving.
SAT for Cryptanalysis
The Crypto-SAT project uses the DPLL(T) paradigm to apply algebraic fault attacks on the SHA family of hash functions. The solver uses a programmatic interface, similar to SAT+CAS architecture, that performs SHA specific reasoning.
Z3str3
Z3str3 is a constraint solver for the quantifier-free theory of string equations, the regular-expression membership predicates, and linear arithmetic over the length functions. Z3str3 is implemented as a string theory plug-in of the powerful Z3 SMT solver.