# BASolver

The acronym BASolver refers to our mixed boolean-algebraic approach. Namely, the objects of our proof system are equalities rather than clauses; this allows to generate polynomial-size proofs for several families of verification benchmarks (this was the main purpose of our project).