This tool is a result of the work on smallest MUS (SMUS) extraction. It is based on MinUC, which is the previous best SMUS extractor originally published at SAT 2013, as well as efficient minimal hitting set dualization approach proposed in our CP 2015 paper. Given a CNF formula, forqes is able to compute one of its smallest MUSes if the formula is unsatisfiable, or one of its smallest MESes (SMESes, smallest minimal equivalent subformulae) if the formula is satisfiable.

Author: Alexey Ignatiev
Contributor: Joao Marques-Silva

Download: Linux x86-64 binary, MacOS Catalina x86-64 binary