Documentation

( literal2Pol l )is the pair (p,v), where p is the polynomial and v is the variable that corresponds (if it does) to the literal lit (in DIMACS format). For example,

>>> literal2Pol "0"
(0,0)
>>> literal2Pol "1"
(x1,x1)
>>> literal2Pol "-1"
(x1+1,x1)

(clause2pol cs) is a pair (p,vs), where p is the polynomial that corresponds to the clause cs (which is written in DIMACS format) and vs is the set of its variables. For example,

>>> clause2Pol ["1"]
(x1,fromList [x1])
>>> clause2Pol ["1","-2"]
(x1x2+x2+1,fromList [x1,x2])

(dimacs2pols f) is the pair (ps,vs) where ps is the set of polynomials wich corresponds to the formula in DIMACS format writed in the file f and vs is the list of variables wich occurs in any polynomial. For example,

>>> dimacs2Pols "exDIMACS/easy/example1.txt"
(fromList [x1x2+x1+x2,1],[x1,x2])
>>> dimacs2Pols "exDIMACS/easy/example4.txt"
(fromList [x1x2+x1+x2,x1x2+x1+1,x1x2+x2+1,x1x2+1,1],[x1,x2])

(formulas2Pols f) is the pair (ps,vs) where ps is the set of polynomials wich corresponds to the formula in FORMULAS format writed in the file f and vs is the list of variables wich occurs in any polynomial. For example,