toysolver-0.1.0: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Copyright(c) Masahiro Sakai 2012-2014
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable (BangPatterns, ScopedTypeVariables, CPP, DeriveDataTypeable, RecursiveDo)
Safe HaskellNone
LanguageHaskell2010

ToySolver.SAT

Contents

Description

A CDCL SAT solver.

It follows the design of MiniSat and SAT4J.

See also:

Synopsis

The Solver type

data Solver Source

Solver instance

newSolver :: IO Solver Source

Create a new Solver instance.

Basic data structures

type Var = Int Source

Variable is represented as positive integers (DIMACS format).

type Lit = Int Source

Positive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).

literal Source

Arguments

:: Var

variable

-> Bool

polarity

-> Lit 

Construct a literal from a variable and its polarity. True (resp False) means positive (resp. negative) literal.

litNot :: Lit -> Lit Source

Negation of the Lit.

litVar :: Lit -> Var Source

Underlying variable of the Lit

litPolarity :: Lit -> Bool Source

Polarity of the Lit. True means positive literal and False means negative literal.

type Clause = [Lit] Source

Disjunction of Lit.

Problem specification

newVar :: Solver -> IO Var Source

Add a new variable

newVars :: Solver -> Int -> IO [Var] Source

Add variables. newVars solver n = replicateM n (newVar solver)

newVars_ :: Solver -> Int -> IO () Source

Add variables. newVars_ solver n = newVars solver n >> return ()

resizeVarCapacity :: Solver -> Int -> IO () Source

Pre-allocate internal buffer for n variables.

addClause :: Solver -> Clause -> IO () Source

Add a clause to the solver.

addAtLeast Source

Arguments

:: Solver

The Solver argument.

-> [Lit]

set of literals {l1,l2,..} (duplicated elements are ignored)

-> Int

n.

-> IO () 

Add a cardinality constraints atleast({l1,l2,..},n).

addAtMost Source

Arguments

:: Solver

The Solver argument

-> [Lit]

set of literals {l1,l2,..} (duplicated elements are ignored)

-> Int

n

-> IO () 

Add a cardinality constraints atmost({l1,l2,..},n).

addExactly Source

Arguments

:: Solver

The Solver argument

-> [Lit]

set of literals {l1,l2,..} (duplicated elements are ignored)

-> Int

n

-> IO () 

Add a cardinality constraints exactly({l1,l2,..},n).

addPBAtLeast Source

Arguments

:: Solver

The Solver argument.

-> [(Integer, Lit)]

set of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO () 

Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≥ n.

addPBAtMost Source

Arguments

:: Solver

The Solver argument.

-> [(Integer, Lit)]

list of [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO () 

Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≤ n.

addPBExactly Source

Arguments

:: Solver

The Solver argument.

-> [(Integer, Lit)]

list of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO () 

Add a pseudo boolean constraints c1*l1 + c2*l2 + … = n.

addPBAtLeastSoft Source

Arguments

:: Solver

The Solver argument.

-> Lit

indicator lit

-> [(Integer, Lit)]

set of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO () 

Add a soft pseudo boolean constraints lit ⇒ c1*l1 + c2*l2 + … ≥ n.

addPBAtMostSoft Source

Arguments

:: Solver

The Solver argument.

-> Lit

indicator lit

-> [(Integer, Lit)]

set of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO () 

Add a soft pseudo boolean constraints lit ⇒ c1*l1 + c2*l2 + … ≤ n.

addPBExactlySoft Source

Arguments

:: Solver

The Solver argument.

-> Lit

indicator lit

-> [(Integer, Lit)]

set of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO () 

Add a soft pseudo boolean constraints lit ⇒ c1*l1 + c2*l2 + … = n.

Solving

solve :: Solver -> IO Bool Source

Solve constraints. Returns True if the problem is SATISFIABLE. Returns False if the problem is UNSATISFIABLE.

solveWith Source

Arguments

:: Solver 
-> [Lit]

Assumptions

-> IO Bool 

Solve constraints under assuptions. Returns True if the problem is SATISFIABLE. Returns False if the problem is UNSATISFIABLE.

data BudgetExceeded Source

Constructors

BudgetExceeded 

Instances

Extract results

type Model = UArray Var Bool Source

A model is represented as a mapping from variables to its values.

model :: Solver -> IO Model Source

After solve returns True, it returns the model.

failedAssumptions :: Solver -> IO [Lit] Source

After solveWith returns False, it returns a set of assumptions that leads to contradiction. In particular, if it returns an empty set, the problem is unsatisiable without any assumptions.

Solver configulation

data RestartStrategy Source

Constructors

MiniSATRestarts 
ArminRestarts 
LubyRestarts 

Instances

setRestartStrategy :: Solver -> RestartStrategy -> IO () Source

defaultRestartStrategy :: RestartStrategy Source

default value for RestartStrategy.

setRestartFirst :: Solver -> Int -> IO () Source

The initial restart limit. (default 100) Negative value is used to disable restart.

defaultRestartFirst :: Int Source

default value for RestartFirst.

setRestartInc :: Solver -> Double -> IO () Source

The factor with which the restart limit is multiplied in each restart. (default 1.5)

defaultRestartInc :: Double Source

default value for RestartInc.

setLearntSizeFirst :: Solver -> Int -> IO () Source

The initial limit for learnt clauses.

defaultLearntSizeFirst :: Int Source

default value for LearntSizeFirst.

setLearntSizeInc :: Solver -> Double -> IO () Source

The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)

defaultLearntSizeInc :: Double Source

default value for LearntSizeInc.

setCCMin :: Solver -> Int -> IO () Source

The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)

defaultCCMin :: Int Source

default value for CCMin.

data LearningStrategy Source

Constructors

LearningClause 
LearningHybrid 

setLearningStrategy :: Solver -> LearningStrategy -> IO () Source

defaultLearningStrategy :: LearningStrategy Source

setEnablePhaseSaving :: Solver -> Bool -> IO () Source

getEnablePhaseSaving :: Solver -> IO Bool Source

defaultEnablePhaseSaving :: Bool Source

setEnableForwardSubsumptionRemoval :: Solver -> Bool -> IO () Source

getEnableForwardSubsumptionRemoval :: Solver -> IO Bool Source

defaultEnableForwardSubsumptionRemoval :: Bool Source

setEnableBackwardSubsumptionRemoval :: Solver -> Bool -> IO () Source

getEnableBackwardSubsumptionRemoval :: Solver -> IO Bool Source

defaultEnableBackwardSubsumptionRemoval :: Bool Source

setVarPolarity :: Solver -> Var -> Bool -> IO () Source

The default polarity of a variable.

setLogger :: Solver -> (String -> IO ()) -> IO () Source

set callback function for receiving messages.

setCheckModel :: Solver -> Bool -> IO () Source

setRandomFreq :: Solver -> Double -> IO () Source

The frequency with which the decision heuristic tries to choose a random variable

defaultRandomFreq :: Double Source

setRandomGen :: Solver -> StdGen -> IO () Source

Set random generator used by the random variable selection

getRandomGen :: Solver -> IO StdGen Source

Get random generator used by the random variable selection

setConfBudget :: Solver -> Maybe Int -> IO () Source

data PBHandlerType Source

Constructors

PBHandlerTypeCounter 
PBHandlerTypePueblo 

Instances

setPBHandlerType :: Solver -> PBHandlerType -> IO () Source

defaultPBHandlerType :: PBHandlerType Source

Read state

nVars :: Solver -> IO Int Source

number of variables of the problem.

nAssigns :: Solver -> IO Int Source

number of assigned variables.

nConstraints :: Solver -> IO Int Source

number of constraints.

nLearnt :: Solver -> IO Int Source

number of learnt constrints.

Internal API

varBumpActivity :: Solver -> Var -> IO () Source

varDecayActivity :: Solver -> IO () Source