From International Center for Computational Logic


Formula simplifier for CNF, QBF, MaxSAT and MUS formulas


  • Norbert Manthey, Kilian Gebhardt

Research Groups

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.