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.

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

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.

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

The default polarity of a variable.

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

set callback function for receiving messages.

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

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

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

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