Function Problem Solvers

Function problem solvers are applicable beyond decision problems. For example, in the Maximum Satisfiability (MaxSAT) problem, the goal is to find an assignment that maximizes the number of satisfied clauses of a CNF, instead of just deciding whether the CNF is satisfiable. Moreover, in the Minimum Unsatisfiable Subformula (MUS) problem, given an unsatisfiable CNF, the goal is to find a minimal set of clauses that is inconsistent (i.e., explains the unsatisfiability of the CNF). Another problem, related to MaxSAT and MUS, is the problem of finding the Minimal Correction Subset (MCS) of an unsatisfiable CNF. An MCS is a minimal set of clauses that, if removed, would allow the CNF to be satisfiable.


MaxSAT Solvers

EvaSolver
Based on core-guided MasSAT resolution.
link binary only

MaxHS
Extension of SAT and MIP solvers.
link open source

MiFuMaX
Unsat-based MaxSAT solver.
link open source

MSCG
Implements different core-guided algorithms.
link binary only

MSUnCore
Based on iterative identification of unsatisfiable cores.
link binary only


MUS Solvers

MoUsSaka
MUS extractor, extension of SApperloT.
link open source

MUSer2
Hybrid MUS extractor.
link open source

PicoMUS
Based on PicoSAT.
link open source


MCS Solvers

MCSls
A tool for computing and enumerating MCSes.
link binary only 

PicoMCS
Based on PicoSAT.
link open source