SatSolver

selectLiteral

reduceFormula

reduceClause

solve