Coprocessor
From International Center for Computational Logic
Coprocessor
Formula simplifier for CNF, QBF, MaxSAT and MUS formulas
- Contact Sibylle Möhle
- http://tools.computational-logic.org
- Publication date July 1, 2012
Coprocessor is a standalone binary that can simplify formulas of different problems. Whereas most techniques are developed to work on CNF formulas, optimization problems like MaxSAT, as well as MUS and QBF are also supported. The implemented simplification techniques includes almost all published simplification techniques. The tool provides statistical output, as well as the opportunity to specify the order of the techniques and to exclude variables from the simplification. Hence, Coprocessor can also be used to simplify formulas partially -- which is especially useful if multiple solutions based on a set of variables should be found.
