represents Var.

Special constant in Var (p.7)

converts a usual Int as literal to an internal Var presentation.

>>> int2var 1
1  -- the first literal is the first variable
>>> int2var 2
2  -- literal @2@ is variable 2
>>> int2var (-2)
2 -- literal @-2@ is corresponding to variable 2

The literal data has an index method which converts the literal to a "small" integer suitable for array indexing. The var method returns the underlying variable of the literal, and the sign method if the literal is signed (False for x and True for -x).

converts Lit into Int as int2lit . lit2int == id.

>>> lit2int 2
1
>>> lit2int 3
-1
>>> lit2int 4
2
>>> lit2int 5
-2

converts Int into Lit as lit2int . int2lit == id.

>>> int2lit 1
2
>>> int2lit (-1)
3
>>> int2lit 2
4
>>> int2lit (-2)
5

Special constant in Lit (p.7)

returns True if the literal is positive

converts Lit into Var.

>>> lit2var 2
1
>>> lit2var 3
1
>>> lit2var 4
2
>>> lit2var 5
2

converts a Var to the corresponing literal.

>>> var2lit 1 True
2
>>> var2lit 1 False
3
>>> var2lit 2 True
4
>>> var2lit 2 False
5

negates literal

>>> negateLit 2
3
>>> negateLit 3
2
>>> negateLit 4
5
>>> negateLit 5
4

FALSE on the Lifted Bool domain

TRUE on the Lifted Bool domain

UNDEFINED on the Lifted Bool domain

Assisting ADT for the dynamic variable ordering of the solver. The constructor takes references to the assignment vector and the activity vector of the solver. The method select will return the unassigned variable with the highest activity.

Misc information on a CNF

Solver's parameters; random decision rate was dropped.

dafault configuration

• Minisat-1.14 uses (0.95, 0.999, 0.2 = 20 / 1000).
• Minisat-2.20 uses (0.95, 0.999, 0).
• Gulcose-4.0 uses (0.8 , 0.999, 0).
• Mios-1.2 uses (0.95, 0.999, 0).