cloncaric

cloncaric / maxsat / 0.1.0

README.md

This algorithm solves the unweighted partial maximum satisfiability problem by invoking a fast SAT solver repeatedly. The input consists of a hard formula which MUST be satisfied, and some soft formulas which MAY be satisfied. The output is a model which maximizes the number of satisfied soft formulas.

Input format:

{
"hard": <formula>
"soft": [<formula>, <formula>, ...]
}

The syntax for <formula> is described in the SAT solver documentation.

Output format:

{
"model": <var-to-bool mapping>
"satSoft": <indices of satisfied soft formulas>
}