Bica is a Python prototype implementation of the formula simplification approach proposed in [*]. Given a Boolean formula in an arbitrary form, it is able to compute a smallest size prime cover of the formula, i.e. to construct a smallest CNF/DNF representation comprising the formula's prime implicates/implicants, which is equivalent to the original formula. Being inspired by the well-known Quine-McCluskey procedure, this entirely SAT-based approach can deal with arbitrary Boolean formulae whereas the Quine-McCluskey procedure can minimize only DNF formulae. The word "bica" is Portuguese and means extremely strong and high-quality coffee (a synonym of espresso).

[*] A. Ignatiev, A. Previti, and J. Marques-Silva. SAT-Based Formula Simplification. In: Proc. SAT 2015, pp. 287–298.

Author: Alexey Ignatiev
Contributors: Joao Marques-Silva, Alessandro Previti

Download: Gzipped TAR archive