SAT-Pol-0.1.0.0

Safe HaskellNone
LanguageHaskell2010

Transformations

Synopsis

Documentation

tr :: FProp -> PolF2 Source #

For example,

>>> let [p1,p2] = [Atom "p1",Atom "p2"]
>>> tr p1
x1
>>> tr (p1 ∧ p2)
x1x2
>>> tr (p ∧ (q ∨ r))
qrx+qx+rx

phi :: PolF2 -> PolF2 Source #

(phi p) is the representative with lowest degree of the polynomial p in the quotient group F2[x_1,...,x_N]/(x_1+x_1^2,...,x_N+x_N^2). The main idea is to replace every ocurrence of x_i^M with x_i thus we obtain an identical polynomial without exponents greater than 1.

For example, >>> [x1,x2] = [var "x1", var "x2"] :: [PolF2] >>> phi (1+x1+x1^2*x2) x1x2+x1+1

theta :: PolF2 -> FProp Source #

For example,

>>> let [x1,x2] = [var "x1", var "x2"] :: [PolF2]
>>> theta 0
>>> theta (x1*x2)
(p1 ∧ p2)
>>> theta (x1 + x2 +1)
¬(p1 ↔ ¬(p2 ↔ ⊤))

projection :: FProp -> PolF2 Source #

For example, >>> [p1,p2] = [Atom "p1",Atom "p2"] >>> projection p1 x1 >>> tr (p1 → p1 ∧ p2) x1^2x2+x1+1 >>> projection (p1 → p1 ∧ p2) x1x2+x1+1

ideal :: PolF2 -> [PolF2] Source #

For example,

>>> [x1,x2] = [var "x1", var "x2"] :: [PolF2]
>>> ideal (1+x1+x1^2*x2)
[x1^2+x1,x2^2+x2]