An ocaml implementation of variants of the simplex and branch&bound algorithms for satisfiability.