SAT.Mios.Types

Basic data types used throughout mios.

Documentation

module SAT.Mios.Vec

Variable

type Var = Int

represents Var.

bottomVar :: Var

Special constant in Var (p.7)

int2var :: Int -> Int

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

Internal encoded Literal

type Lit = Int

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).

lit2int :: Lit -> Int

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

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

int2lit :: Int -> Lit

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

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

bottomLit :: Lit

Special constant in Lit (p.7)

positiveLit :: Lit -> Bool

returns True if the literal is positive

lit2var :: Lit -> Var

converts Lit into Var.

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

var2lit :: Var -> Bool -> Lit

converts a Var to the corresponing literal.

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

negateLit :: Lit -> Lit

negates literal

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

Assignment on the lifted Bool domain

lFalse :: Int

FALSE on the Lifted Bool domain

lTrue :: Int

TRUE on the Lifted Bool domain

lBottom :: Int

UNDEFINED on the Lifted Bool domain

class VarOrder o where

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.

Methods

update :: o -> Var -> IO ()

should be called when a variable has increased in activity.

undo :: o -> Var -> IO ()

should be called when a variable becomes unbound (may be selected again).

select :: o -> IO Var

returns a new, unassigned var as the next decision.

Instances

VarOrder Solver

Interfate to select a decision var based on variable activity.

Methods

update :: Solver -> Var -> IO ()

undo :: Solver -> Var -> IO ()

select :: Solver -> IO Var

CNF

data CNFDescription

Misc information on a CNF

Constructors

CNFDescription

Fields

• _numberOfVariables :: !Int

  the number of variables

• _numberOfClauses :: !Int

  the number of clauses

• _pathname :: Maybe FilePath

  given filename

Instances

Eq CNFDescription

Methods

(==) :: CNFDescription -> CNFDescription -> Bool

(/=) :: CNFDescription -> CNFDescription -> Bool

Ord CNFDescription

Methods

compare :: CNFDescription -> CNFDescription -> Ordering

(<) :: CNFDescription -> CNFDescription -> Bool

(<=) :: CNFDescription -> CNFDescription -> Bool

(>) :: CNFDescription -> CNFDescription -> Bool

(>=) :: CNFDescription -> CNFDescription -> Bool

max :: CNFDescription -> CNFDescription -> CNFDescription

min :: CNFDescription -> CNFDescription -> CNFDescription

Show CNFDescription

Methods

showsPrec :: Int -> CNFDescription -> ShowS

show :: CNFDescription -> String

showList :: [CNFDescription] -> ShowS

Solver Configuration

data MiosConfiguration

Solver's parameters; random decision rate was dropped.

Constructors

MiosConfiguration

Fields

• variableDecayRate :: !Double

  decay rate for variable activity , clauseDecayRate :: !Double -- ^ decay rate for clause activity

defaultConfiguration :: MiosConfiguration

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).