# Bica

##### (Boolean simplifier for non-clausal formulae)

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