Boolector

News

Release 1.6.0.

BEEM benchmarks in BTOR format contributed by Jori Dubrovin.

Awards

  • SMT Competition 2012:
    1st place in both the bit vectors category (QF_BV, main track) and the bit vectors with array category (QF_AUFBV, main track).
     Competing version:  Boolector 1.5.110-agm

  • SMT Competition 2011:
    3rd place in the bit vectors category (QF_BV, main track) and 1st place in the bit vectors with array category (QF_AFBV, main track).
     Competing version:  Boolector 1.5.23-833

  • SMT Competition 2010:
     no participation

  • SMT Competition 2009:
    2nd place in the bit vectors category (QF_BV, main track) and 1st place in the bit vectors with array category (QF_AUFBV, main track).
     Competing version:  Boolector 1.2

  • SMT Competition 2008:
    1st place in both the bit vectors category (QF_BV, main track) and the bit vectors with array category (QF_AUFBV, main track).
     Competing version:  Boolector 0.4

Download

boolector-1.6.0-with-sat-solvers.tar.gz ]

Starting with version 1.6.0 we use a restricted license for non-commercial use.

By default it is also prohibited to use this version of Boolector as part of a competition without explicit written permission.

See the NEWS, README and COPYING files for more detailed information on Boolector and its license.

Please use our google group for any questions, bug reports, comments and information on new releases.

Older versions

The 3rd source code release of Boolector 1.4.1 fixes a rare bug in the simplifier by removing the unconstrained expression optimization.

The following versions are (still) available under the GNU General Public License Version 3:

boolector-1.5.118-6b56be4-121013.tar.gz ]
boolector-1.5.116-eeaf10b-121004.tar.gz ]
boolector-1.5.115-5d546c8-120922.tar.gz ]
boolector-1.4.1-376e6b0-110304.tar.gz ]
boolector-1.4-ffc2089-100608.tar.gz ]
boolector-1.3-e71a070-100601.tar.gz ]

Release 1.5.118 uses the 'simpdelay' feature of Lingeling for faster solving of simple instances. Further, the library now supports choosing the SAT solver via the API. This release only works with a newer Lingeling of Version ala and above.

Release 1.5.116 fixes an incorrect assertion and the examples provided (which were previously broken) compile again. This release uses the latest reentrant version 953 of PicoSAT, hence it does not work with previous versions of PicoSAT.

Release 1.5.115 of Boolector is close to the version used in the SMT Competition 2012. It is best used in combination with version al6 of Lingeling, but also works with PicoSAT and MiniSAT. The source code of these SAT solvers needs to be obtained separately with the archives listed above.

The following archives contain easier to compile versions of Boolector 1.5.115 packaged with Lingeling al6, and Boolector 1.5.116 and 1.5.118 packaged with Lingeling al6, PicoSAT 953, and MiniSAT 2.2.0.

boolector-1.5.118-with-sat-solvers.tar.gz ]
boolector-1.5.116-with-sat-solvers.tar.gz ]
boolector-1.5.115-with-lingeling-al6.tar.bz2 ]

These versions with Lingeling version al6 as back-end should be slightly faster than the competition version 1.5.110-agm on the plain bit vectors without arrays benchmarks from the SMT Competition 2012, and slightly slower on those with arrays. This is both mainly due to Lingeling. The competition version of Lingeling is not available publically.

The following releases are all 32-bit statically linked Linux-x86 binaries. For these versions, we do neither support other platforms nor do we plan a source release. Finally, the restrictions of the license section apply.

boolector-1.1-IA-32.tar.bz2 ]
boolector-1.0-IA-32.tar.bz2 ]
boolector-0.7.tar.bz2 ]
boolector-0.6.tar.bz2 ]
boolector-0.5.tar.bz2 ]
boolector-0.0.tar.bz2 ]

Publications related to Boolector

Slides related to Boolector

License

Newer versions, starting with release 1.6.0, use a restricted license for non-commercial use.

By default it is also prohibited to use these versions of Boolector as part of a competition without explicit written permission.

All source code releases prior to release 1.6.0 are still available under the GNU General Public License Version 3.

All binary releases (including Boolector 1.2) are available for research and evaluation purposes in an academic environment only. They can not be used in a commercial environment, particularly as part of a commercial product, without written permission.

In general, Boolector is provided as is, without any warranty.

Please contact Armin Biere for additional questions regarding licensing Boolector under a different license or to obtain more up-to-date versions.