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.
"soft": [<formula>, <formula>, ...]
The syntax for <formula> is described in the SAT solver documentation.
"model": <var-to-bool mapping>
"satSoft": <indices of satisfied soft formulas>