Documentation

Formula type

The makeFormula function constructs a formula from a list of clauses. Duplicate clauses are removed.

>>> makeFormula []
[]
>>> makeFormula [[1], [2,3]]
	[[1],[2,3]]
>>> makeFormula [[1], [2,3], [3,2], [1]]
[[1],[2,3]]

The isEmpty function return True if the formula is empty.

>>> isEmpty $ makeFormula []
	True
>>> isEmpty $ makeFormula [[1,2], [3]]
False

The isSatisfied function return True if the formula is empty. (See isEmpty.)

The unitClauses function takes a formula and returns a new formula made of those unit clauses.

>>> unitClauses $ makeFormula [[1], [-2,3], [4], [5,6,7]]
[[1],[4]]

The mostFrequentLiteral function takes a formula and returns one literal that occurs more frequently.

>>> mostFrequentLiteral $ makeFormula [[1], [-1,-2], [1,2,-3], [2,3]]
2

The hasUnsatisfiedClause function takes a formula and returns True if it contains at least one empty clause.

The makeExampleFormula returns an example formula using both makeClause and makeFormula.

>>> makeExampleFormula
[[-3,1],[-5,1,4],[2,3,4],[-5,-3,-1],[4,5],[-4,-3,5],[2],[-2,1]]