Other Projects

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.

Z3str2

Z3str2 is a constraint solver for the quantifier-free theory of string equations, the regular-expression membership predicates, and linear arithmetic over the length functions. Z3str2 is implemented as a string theory plug-in of the powerful Z3 SMT solver.