We should implement the Linear/Double Partner Strategy, Quadratic Partner Substitution etc ideas by Jovanovic and Kreuzer

[msoos]

Paper here. "Algebraic Attacks using SAT-Solvers". Authors: Philipp Jovanovic and Martin Kreuzer. Implementation here.

These strategies look like they could be interesting to improve the translation. Some checking is needed to verify whether our espresso-based system covers these cases.