Home
Download
Compilation
Usage
DIMACS format
ISCAS/RTL format

Welcome to the BASolver homepage! This page is devoted to the boolean satisfiability solver that we have designed in the Laboratory of Mathematical Logic of the St.Petersburg Department of Steklov Institute of Mathematics of Russian Academy of Sciences.

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).

This project was supported by Intel Corporation (via the U.S. Civilian Research & Development Foundation grant CRDF GAP 1373).