úÎ$Å"t     Sebastian FischerBSD3/Sebastian Fischer (sebf@informatik.uni-kiel.de) experimentalportableSafe 7Conjunctive normalforms are lists of lists of literals.BLiterals are variables that occur either positively or negatively.3Boolean formulas are represented as values of type Boolean.Variables are labeled with an Int,Yes represents true,No represents false,Not constructs negated formulas,"and finally we provide conjunction$and disjunction of boolean formulas.<This function returns the name of the variable in a literal. This function negates a literal.<This predicate checks whether the given literal is positive.ŽWe convert boolean formulas to conjunctive normal form by pushing negations down to variables and repeatedly applying the distributive laws.Sebastian FischerBSD3/Sebastian Fischer (sebf@informatik.uni-kiel.de) experimentalportableSafe A  SatSolver' can be used to solve boolean formulas.,A new SAT solver without stored constraints. 8This predicate tells whether all constraints are solved. ƒWe can lookup the binding of a variable according to the currently stored constraints. If the variable is unbound, the result is Nothing. +We can assert boolean formulas to update a  SatSolverI. The assertion may fail if the resulting constraints are unsatisfiable. ³This function guesses a value for the given variable, if it is currently unbound. As this is a non-deterministic operation, the resulting solvers are returned in an instance of  MonadPlus. OWe select a variable from the shortest clause hoping to produce a unit clause.«This function guesses values for variables such that the stored constraints are satisfied. The result may be non-deterministic and is, hence, returned in an instance of  MonadPlus.¶This predicate tells whether the stored constraints are solvable. Use with care! This might be an inefficient operation. It tries to find a solution using backtracking and returns True if and only if that fails. !" #$%&'()*+,   !" #$%&'()*+,-      !" #$%&'()*+,-./3incremental-sat-solver-0.1.8-9h6a2hWiWqe1ki9dk1UwlYData.Boolean.SatSolver Data.BooleanBooleanVarYesNoNot:&&::||: SatSolver newSatSolverisSolved lookupVar assertTrue branchOnVarselectBranchVarsolve isSolvable$fShowSatSolverCNFLiteral literalVar invLiteralisPositiveLiteral booleanToCNFClausePosNeg simpleClause conjunction disjunctionasLongAsPossible everywhere atChildrenclausesbindings addClause addUnbound updateSolver insertBindingsimplifysimplifyClauses propagatebranchOnUnboundguessshorter