Documentation

The selectLiteral function return a literal in the clause. If the clause contains contains at least one unit clause, the function returns a literal in a unit clause. Otherwise it returns a literal that occurs the most frequently.

>>> selectLiteral $ F.makeFormula [[1,2], [3], [1,2], [4]]
3
>>> selectLiteral $ F.makeFormula [[1,2], [3,4], [1,3]]
3

This function should not be part of the public interface of the module.

The reduceFormula function reduce a formula according to a literal. Occurrences of the opposite literal are removed and clauses containing this literal are removed.

>>> reduceFormula 1 $ F.makeFormula [[1,2],[-1,-2],[2,3],[1,-2]]
[[-2],[2,3]]

This function should not be part of the public interface of the module.

The reduceClause function reduces a clause according to a given literal: it removes the opposite occurrence (if any) of the literal.

>>> reduceClause 1 $ C.makeClause []
[]
>>> reduceClause 1 $ C.makeClause [1, 2, 3]
[1,2,3]
>>> reduceClause 1 $ C.makeClause [-1, 2, 3]
[2,3]

This function should not be part of the public interface of the module.

The solve function returns Nothing if the formula is not satisfiable. Ohherwise it returns a satisfying assignment (possibly incomplete) in the form of a map.

>>> solve $ F.makeFormula [[1,2], [-1,-2], [2,3], [1,-2], [-2,4]]
Just (fromList [(1,True),(2,False),(3,True)])
>>> solve $ F.makeFormula [[1,2], [-1,2], [1,-2], [-1,-2]]
Nothing

This function should not be part of the public interface of the module.