toysolver-0.3.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

Selector literal sel

-> [(Integer, Lit)]

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

-> Integer

n

-> IO () 

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

addPBAtMostSoft Source

Arguments

:: Solver

The Solver argument.

-> Lit

Selector literal sel

-> [(Integer, Lit)]

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

-> Integer

n

-> IO () 

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

addPBExactlySoft Source

Arguments

:: Solver

The Solver argument.

-> Lit

Selector literal sel

-> [(Integer, Lit)]

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

-> Integer

n

-> IO () 

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

addXORClause Source

Arguments

:: Solver

The Solver argument.

-> [Lit]

literals [l1, l2, …, ln]

-> Bool

rhs

-> IO () 

Add a parity constraint l1 ⊕ l2 ⊕ … ⊕ ln = rhs

addXORClauseSoft Source

Arguments

:: Solver

The Solver argument.

-> Lit

Selector literal sel

-> [Lit]

literals [l1, l2, …, ln]

-> Bool

rhs

-> IO () 

Add a soft parity constraint sel ⇒ l1 ⊕ l2 ⊕ … ⊕ ln = rhs

setTheory :: Solver -> TheorySolver -> IO () Source

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.

getModel :: Solver -> IO Model Source

After solve returns True, it returns an satisfying assignment.

getFailedAssumptions :: 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) Zero and negative values are 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)

This must be >1.

defaultRestartInc :: Double Source

default value for RestartInc.

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

The initial limit for learnt clauses.

Negative value means computing default value from problem instance.

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)

This must be >1.

defaultLearntSizeInc :: Double Source

default value for LearntSizeInc.

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

Controls conflict clause minimization (0=none, 1=basic, 2=deep)

defaultCCMin :: Int Source

default value for CCMin.

data LearningStrategy Source

Constructors

LearningClause 
LearningHybrid 

Instances

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

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

Split PB-constraints into a PB part and a clause part.

Example from minisat+ paper:

  • 4 x1 + 4 x2 + 4 x3 + 4 x4 + 2y1 + y2 + y3 ≥ 4

would be split into

  • x1 + x2 + x3 + x4 + ¬z ≥ 1 (clause part)
  • 2 y1 + y2 + y3 + 4 z ≥ 4 (PB part)

where z is a newly introduced variable, not present in any other constraint.

Reference:

  • N . Eéen and N. Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT 2:1–26, 2006.

getPBSplitClausePart :: Solver -> IO Bool Source

See documentation of setPBSplitClausePart.

defaultPBSplitClausePart :: Bool Source

See documentation of setPBSplitClausePart.

Read state

getNVars :: Solver -> IO Int Source

number of variables of the problem.

getNConstraints :: Solver -> IO Int Source

number of constraints.

getNLearntConstraints :: Solver -> IO Int Source

number of learnt constrints.

getVarFixed :: Solver -> Var -> IO LBool Source

getLitFixed :: Solver -> Var -> IO LBool Source

Read state (deprecated)

nVars :: Solver -> IO Int Source

Deprecated: Use getNVars instead

number of variables of the problem.

nAssigns :: Solver -> IO Int Source

Deprecated: nAssigns is deprecated

number of assigned variables.

nConstraints :: Solver -> IO Int Source

Deprecated: Use getNConstraints instead

number of constraints.

nLearnt :: Solver -> IO Int Source

Deprecated: Use getNLearntConstraints instead

number of learnt constrints.

Internal API

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

varDecayActivity :: Solver -> IO () Source