SatSolver
selectLiteral
reduceFormula
reduceClause
solve