Copyright	(c) Masahiro Sakai 2012
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	ScopedTypeVariables BangPatterns TypeSynonymInstances FlexibleInstances ConstrainedClassMethods MultiParamTypeClasses FunctionalDependencies ExplicitForAll

ToySolver.SAT.Types

Contents

Variable
Model
Literal
Clause
Packed Clause
Cardinality Constraint
(Linear) Pseudo Boolean Constraint
Non-linear Pseudo Boolean constraint
XOR Clause
Type classes for solvers
Type-2 SOS constraints

Description

Synopsis

type Var = Int
type VarSet = IntSet
type VarMap = IntMap
validVar :: Var -> Bool
class IModel a where
- evalVar :: a -> Var -> Bool
type Model = UArray Var Bool
restrictModel :: Int -> Model -> Model
type Lit = Int
type LitSet = IntSet
type LitMap = IntMap
litUndef :: Lit
validLit :: Lit -> Bool
literal :: Var -> Bool -> Lit
litNot :: Lit -> Lit
litVar :: Lit -> Var
litPolarity :: Lit -> Bool
evalLit :: IModel m => m -> Lit -> Bool
type Clause = [Lit]
normalizeClause :: Clause -> Maybe Clause
instantiateClause :: forall m. Monad m => (Lit -> m LBool) -> Clause -> m (Maybe Clause)
clauseSubsume :: Clause -> Clause -> Bool
evalClause :: IModel m => m -> Clause -> Bool
clauseToPBLinAtLeast :: Clause -> PBLinAtLeast
type PackedVar = PackedLit
type PackedLit = Int32
packLit :: Lit -> PackedLit
unpackLit :: PackedLit -> Lit
type PackedClause = Vector PackedLit
packClause :: Clause -> PackedClause
unpackClause :: PackedClause -> Clause
type AtLeast = ([Lit], Int)
type Exactly = ([Lit], Int)
normalizeAtLeast :: AtLeast -> AtLeast
instantiateAtLeast :: forall m. Monad m => (Lit -> m LBool) -> AtLeast -> m AtLeast
evalAtLeast :: IModel m => m -> AtLeast -> Bool
evalExactly :: IModel m => m -> Exactly -> Bool
type PBLinTerm = (Integer, Lit)
type PBLinSum = [PBLinTerm]
type PBLinAtLeast = (PBLinSum, Integer)
type PBLinExactly = (PBLinSum, Integer)
normalizePBLinSum :: (PBLinSum, Integer) -> (PBLinSum, Integer)
normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
normalizePBLinExactly :: PBLinExactly -> PBLinExactly
instantiatePBLinAtLeast :: forall m. Monad m => (Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
instantiatePBLinExactly :: Monad m => (Lit -> m LBool) -> PBLinExactly -> m PBLinExactly
cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast
cardinalityReduction :: PBLinAtLeast -> AtLeast
negatePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
evalPBLinSum :: IModel m => m -> PBLinSum -> Integer
evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool
evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool
pbLinLowerBound :: PBLinSum -> Integer
pbLinUpperBound :: PBLinSum -> Integer
pbLinSubsume :: PBLinAtLeast -> PBLinAtLeast -> Bool
type PBTerm = (Integer, [Lit])
type PBSum = [PBTerm]
evalPBSum :: IModel m => m -> PBSum -> Integer
evalPBConstraint :: IModel m => m -> Constraint -> Bool
evalPBFormula :: IModel m => m -> Formula -> Maybe Integer
evalPBSoftFormula :: IModel m => m -> SoftFormula -> Maybe Integer
pbLowerBound :: PBSum -> Integer
pbUpperBound :: PBSum -> Integer
removeNegationFromPBSum :: PBSum -> PBSum
type XORClause = ([Lit], Bool)
normalizeXORClause :: XORClause -> XORClause
instantiateXORClause :: forall m. Monad m => (Lit -> m LBool) -> XORClause -> m XORClause
evalXORClause :: IModel m => m -> XORClause -> Bool
class Monad m => NewVar m a | a -> m where
- newVar :: a -> m Var
- newVars :: a -> Int -> m [Var]
- newVars_ :: a -> Int -> m ()
class NewVar m a => AddClause m a | a -> m where
- addClause :: a -> Clause -> m ()
class AddClause m a => AddCardinality m a | a -> m where
- addAtLeast :: a -> [Lit] -> Int -> m ()
- addAtMost :: a -> [Lit] -> Int -> m ()
- addExactly :: a -> [Lit] -> Int -> m ()
class AddCardinality m a => AddPBLin m a | a -> m where
- addPBAtLeast :: a -> PBLinSum -> Integer -> m ()
- addPBAtMost :: a -> PBLinSum -> Integer -> m ()
- addPBExactly :: a -> PBLinSum -> Integer -> m ()
- addPBAtLeastSoft :: a -> Lit -> PBLinSum -> Integer -> m ()
- addPBAtMostSoft :: a -> Lit -> PBLinSum -> Integer -> m ()
- addPBExactlySoft :: a -> Lit -> PBLinSum -> Integer -> m ()
class AddPBLin m a => AddPBNL m a | a -> m where
- addPBNLAtLeast :: a -> PBSum -> Integer -> m ()
- addPBNLAtMost :: a -> PBSum -> Integer -> m ()
- addPBNLExactly :: a -> PBSum -> Integer -> m ()
- addPBNLAtLeastSoft :: a -> Lit -> PBSum -> Integer -> m ()
- addPBNLAtMostSoft :: a -> Lit -> PBSum -> Integer -> m ()
- addPBNLExactlySoft :: a -> Lit -> PBSum -> Integer -> m ()
class AddClause m a => AddXORClause m a | a -> m where
- addXORClause :: a -> [Lit] -> Bool -> m ()
- addXORClauseSoft :: a -> Lit -> [Lit] -> Bool -> m ()
addSOS2 :: AddClause m a => a -> [Lit] -> m ()
evalSOS2 :: IModel m => m -> [Lit] -> Bool

Variable

type Var = Int Source #

Variable is represented as positive integers (DIMACS format).

type VarSet = IntSet Source #

type VarMap = IntMap Source #

validVar :: Var -> Bool Source #

Model

class IModel a where Source #

Methods

evalVar :: a -> Var -> Bool Source #

Instances

Instances details

IModel (UArray Var Bool) Source #
Instance details Defined in ToySolver.SAT.Types Methods evalVar :: UArray Var Bool -> Var -> Bool Source #
IModel (Array Var Bool) Source #
Instance details Defined in ToySolver.SAT.Types Methods evalVar :: Array Var Bool -> Var -> Bool Source #
IModel (Var -> Bool) Source #
Instance details Defined in ToySolver.SAT.Types Methods evalVar :: (Var -> Bool) -> Var -> Bool Source #

type Model = UArray Var Bool Source #

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

restrictModel :: Int -> Model -> Model Source #

Restrict model to first nv variables.

Literal

type Lit = Int Source #

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

type LitSet = IntSet Source #

type LitMap = IntMap Source #

litUndef :: Lit Source #

validLit :: Lit -> Bool Source #

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.

evalLit :: IModel m => m -> Lit -> Bool Source #

Clause

type Clause = [Lit] Source #

Disjunction of Lit.

normalizeClause :: Clause -> Maybe Clause Source #

Normalizing clause

Nothing if the clause is trivially true.

instantiateClause :: forall m. Monad m => (Lit -> m LBool) -> Clause -> m (Maybe Clause) Source #

clauseSubsume :: Clause -> Clause -> Bool Source #

evalClause :: IModel m => m -> Clause -> Bool Source #

clauseToPBLinAtLeast :: Clause -> PBLinAtLeast Source #

Packed Clause

type PackedVar = PackedLit Source #

type PackedLit = Int32 Source #

packLit :: Lit -> PackedLit Source #

unpackLit :: PackedLit -> Lit Source #

type PackedClause = Vector PackedLit Source #

packClause :: Clause -> PackedClause Source #

unpackClause :: PackedClause -> Clause Source #

Cardinality Constraint

type AtLeast = ([Lit], Int) Source #

type Exactly = ([Lit], Int) Source #

normalizeAtLeast :: AtLeast -> AtLeast Source #

instantiateAtLeast :: forall m. Monad m => (Lit -> m LBool) -> AtLeast -> m AtLeast Source #

evalAtLeast :: IModel m => m -> AtLeast -> Bool Source #

evalExactly :: IModel m => m -> Exactly -> Bool Source #

(Linear) Pseudo Boolean Constraint

type PBLinTerm = (Integer, Lit) Source #

type PBLinSum = [PBLinTerm] Source #

type PBLinAtLeast = (PBLinSum, Integer) Source #

type PBLinExactly = (PBLinSum, Integer) Source #

normalizePBLinSum :: (PBLinSum, Integer) -> (PBLinSum, Integer) Source #

normalizing PB term of the form c1 x1 + c2 x2 ... cn xn + c into d1 x1 + d2 x2 ... dm xm + d where d1,...,dm ≥ 1.

normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast Source #

normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn >= b.

normalizePBLinExactly :: PBLinExactly -> PBLinExactly Source #

normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn = b.

instantiatePBLinAtLeast :: forall m. Monad m => (Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast Source #

instantiatePBLinExactly :: Monad m => (Lit -> m LBool) -> PBLinExactly -> m PBLinExactly Source #

cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast Source #

cardinalityReduction :: PBLinAtLeast -> AtLeast Source #

negatePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast Source #

evalPBLinSum :: IModel m => m -> PBLinSum -> Integer Source #

evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool Source #

evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool Source #

pbLinLowerBound :: PBLinSum -> Integer Source #

pbLinUpperBound :: PBLinSum -> Integer Source #

pbLinSubsume :: PBLinAtLeast -> PBLinAtLeast -> Bool Source #

Non-linear Pseudo Boolean constraint

type PBTerm = (Integer, [Lit]) Source #

type PBSum = [PBTerm] Source #

evalPBSum :: IModel m => m -> PBSum -> Integer Source #

evalPBConstraint :: IModel m => m -> Constraint -> Bool Source #

evalPBFormula :: IModel m => m -> Formula -> Maybe Integer Source #

evalPBSoftFormula :: IModel m => m -> SoftFormula -> Maybe Integer Source #

pbLowerBound :: PBSum -> Integer Source #

pbUpperBound :: PBSum -> Integer Source #

removeNegationFromPBSum :: PBSum -> PBSum Source #

XOR Clause

type XORClause = ([Lit], Bool) Source #

XOR clause

'([l1,l2..ln], b)' means l1 ⊕ l2 ⊕ ⋯ ⊕ ln = b.

Note that:

True can be represented as ([], False)
False can be represented as ([], True)

normalizeXORClause :: XORClause -> XORClause Source #

Normalize XOR clause

instantiateXORClause :: forall m. Monad m => (Lit -> m LBool) -> XORClause -> m XORClause Source #

evalXORClause :: IModel m => m -> XORClause -> Bool Source #

Type classes for solvers

class Monad m => NewVar m a | a -> m where Source #

Minimal complete definition

newVar

Methods

newVar :: a -> m Var Source #

Add a new variable

newVars :: a -> Int -> m [Var] Source #

Add variables. newVars a n = replicateM n (newVar a), but maybe faster.

newVars_ :: a -> Int -> m () Source #

Add variables. newVars_ a n = newVars a n >> return (), but maybe faster.

Instances

Instances details

NewVar IO Solver Source #
Instance details Defined in ToySolver.SAT.Solver.CDCL Methods newVar :: Solver -> IO Var Source # newVars :: Solver -> Int -> IO [Var] Source # newVars_ :: Solver -> Int -> IO () Source #
Monad m => NewVar m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.Cardinality Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #
Monad m => NewVar m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #
Monad m => NewVar m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #
Monad m => NewVar m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #
Monad m => NewVar m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.Tseitin Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #
PrimMonad m => NewVar m (CNFStore m) Source #
Instance details Defined in ToySolver.SAT.Store.CNF Methods newVar :: CNFStore m -> m Var Source # newVars :: CNFStore m -> Int -> m [Var] Source # newVars_ :: CNFStore m -> Int -> m () Source #
PrimMonad m => NewVar m (PBStore m) Source #
Instance details Defined in ToySolver.SAT.Store.PB Methods newVar :: PBStore m -> m Var Source # newVars :: PBStore m -> Int -> m [Var] Source # newVars_ :: PBStore m -> Int -> m () Source #

class NewVar m a => AddClause m a | a -> m where Source #

Methods

addClause :: a -> Clause -> m () Source #

Instances

Instances details

AddClause IO Solver Source #
Instance details Defined in ToySolver.SAT.Solver.CDCL Methods addClause :: Solver -> Clause -> IO () Source #
Monad m => AddClause m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.Cardinality Methods addClause :: Encoder m -> Clause -> m () Source #
Monad m => AddClause m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer Methods addClause :: Encoder m -> Clause -> m () Source #
Monad m => AddClause m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods addClause :: Encoder m -> Clause -> m () Source #
Monad m => AddClause m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC Methods addClause :: Encoder m -> Clause -> m () Source #
Monad m => AddClause m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.Tseitin Methods addClause :: Encoder m -> Clause -> m () Source #
PrimMonad m => AddClause m (CNFStore m) Source #
Instance details Defined in ToySolver.SAT.Store.CNF Methods addClause :: CNFStore m -> Clause -> m () Source #
PrimMonad m => AddClause m (PBStore m) Source #
Instance details Defined in ToySolver.SAT.Store.PB Methods addClause :: PBStore m -> Clause -> m () Source #

class AddClause m a => AddCardinality m a | a -> m where Source #

Minimal complete definition

addAtLeast

Methods

addAtLeast Source #

Arguments

:: a
-> [Lit]	set of literals {l1,l2,..} (duplicated elements are ignored)
-> Int	n
-> m ()

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

addAtMost Source #

Arguments

:: a
-> [Lit]	set of literals {l1,l2,..} (duplicated elements are ignored)
-> Int	n
-> m ()

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

addExactly Source #

Arguments

:: a
-> [Lit]	set of literals {l1,l2,..} (duplicated elements are ignored)
-> Int	n
-> m ()

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

Instances

Instances details

AddCardinality IO Solver Source #
Instance details Defined in ToySolver.SAT.Solver.CDCL Methods addAtLeast :: Solver -> [Lit] -> Int -> IO () Source # addAtMost :: Solver -> [Lit] -> Int -> IO () Source # addExactly :: Solver -> [Lit] -> Int -> IO () Source #
PrimMonad m => AddCardinality m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.Cardinality Methods addAtLeast :: Encoder m -> [Lit] -> Int -> m () Source # addAtMost :: Encoder m -> [Lit] -> Int -> m () Source # addExactly :: Encoder m -> [Lit] -> Int -> m () Source #
PrimMonad m => AddCardinality m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods addAtLeast :: Encoder m -> [Lit] -> Int -> m () Source # addAtMost :: Encoder m -> [Lit] -> Int -> m () Source # addExactly :: Encoder m -> [Lit] -> Int -> m () Source #
Monad m => AddCardinality m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC Methods addAtLeast :: Encoder m -> [Lit] -> Int -> m () Source # addAtMost :: Encoder m -> [Lit] -> Int -> m () Source # addExactly :: Encoder m -> [Lit] -> Int -> m () Source #
PrimMonad m => AddCardinality m (PBStore m) Source #
Instance details Defined in ToySolver.SAT.Store.PB Methods addAtLeast :: PBStore m -> [Lit] -> Int -> m () Source # addAtMost :: PBStore m -> [Lit] -> Int -> m () Source # addExactly :: PBStore m -> [Lit] -> Int -> m () Source #

class AddCardinality m a => AddPBLin m a | a -> m where Source #

Minimal complete definition

addPBAtLeast

Methods

addPBAtLeast Source #

Arguments

:: a
-> PBLinSum	list of terms `[(c1,l1),(c2,l2),…]`
-> Integer	n
-> m ()

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

addPBAtMost Source #

Arguments

:: a
-> PBLinSum	list of `[(c1,l1),(c2,l2),…]`
-> Integer	n
-> m ()

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

addPBExactly Source #

Arguments

:: a
-> PBLinSum	list of terms `[(c1,l1),(c2,l2),…]`
-> Integer	n
-> m ()

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

addPBAtLeastSoft Source #

Arguments

:: a
-> Lit	Selector literal `sel`
-> PBLinSum	list of terms `[(c1,l1),(c2,l2),…]`
-> Integer	n
-> m ()

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

addPBAtMostSoft Source #

Arguments

:: a
-> Lit	Selector literal `sel`
-> PBLinSum	list of terms `[(c1,l1),(c2,l2),…]`
-> Integer	n
-> m ()

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

addPBExactlySoft Source #

Arguments

:: a
-> Lit	Selector literal `sel`
-> PBLinSum	list of terms `[(c1,l1),(c2,l2),…]`
-> Integer	n
-> m ()

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

Instances

Instances details

AddPBLin IO Solver Source #
Instance details Defined in ToySolver.SAT.Solver.CDCL Methods addPBAtLeast :: Solver -> PBLinSum -> Integer -> IO () Source # addPBAtMost :: Solver -> PBLinSum -> Integer -> IO () Source # addPBExactly :: Solver -> PBLinSum -> Integer -> IO () Source # addPBAtLeastSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO () Source # addPBAtMostSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO () Source # addPBExactlySoft :: Solver -> Lit -> PBLinSum -> Integer -> IO () Source #
PrimMonad m => AddPBLin m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtMost :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBExactly :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtLeastSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBAtMostSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBExactlySoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source #
Monad m => AddPBLin m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC Methods addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtMost :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBExactly :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtLeastSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBAtMostSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBExactlySoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source #
PrimMonad m => AddPBLin m (PBStore m) Source #
Instance details Defined in ToySolver.SAT.Store.PB Methods addPBAtLeast :: PBStore m -> PBLinSum -> Integer -> m () Source # addPBAtMost :: PBStore m -> PBLinSum -> Integer -> m () Source # addPBExactly :: PBStore m -> PBLinSum -> Integer -> m () Source # addPBAtLeastSoft :: PBStore m -> Lit -> PBLinSum -> Integer -> m () Source # addPBAtMostSoft :: PBStore m -> Lit -> PBLinSum -> Integer -> m () Source # addPBExactlySoft :: PBStore m -> Lit -> PBLinSum -> Integer -> m () Source #

class AddPBLin m a => AddPBNL m a | a -> m where Source #

Minimal complete definition

addPBNLAtLeast

Methods

addPBNLAtLeast Source #

Arguments

:: a
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … ≥ n.

addPBNLAtMost Source #

Arguments

:: a
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … ≥ n.

addPBNLExactly Source #

Arguments

:: a
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … = n.

addPBNLAtLeastSoft Source #

Arguments

:: a
-> Lit	Selector literal `sel`
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

Add a soft non-linear pseudo boolean constraints sel ⇒ c1*ls1 + c2*ls2 + … ≥ n.

addPBNLAtMostSoft Source #

Arguments

:: a
-> Lit	Selector literal `sel`
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

Add a soft non-linear pseudo boolean constraints sel ⇒ c1*ls1 + c2*ls2 + … ≤ n.

addPBNLExactlySoft Source #

Arguments

:: a
-> Lit	Selector literal `sel`
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

Add a soft non-linear pseudo boolean constraints lit ⇒ c1*ls1 + c2*ls2 + … = n.

Instances

Instances details

PrimMonad m => AddPBNL m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC Methods addPBNLAtLeast :: Encoder m -> PBSum -> Integer -> m () Source # addPBNLAtMost :: Encoder m -> PBSum -> Integer -> m () Source # addPBNLExactly :: Encoder m -> PBSum -> Integer -> m () Source # addPBNLAtLeastSoft :: Encoder m -> Lit -> PBSum -> Integer -> m () Source # addPBNLAtMostSoft :: Encoder m -> Lit -> PBSum -> Integer -> m () Source # addPBNLExactlySoft :: Encoder m -> Lit -> PBSum -> Integer -> m () Source #
PrimMonad m => AddPBNL m (PBStore m) Source #
Instance details Defined in ToySolver.SAT.Store.PB Methods addPBNLAtLeast :: PBStore m -> PBSum -> Integer -> m () Source # addPBNLAtMost :: PBStore m -> PBSum -> Integer -> m () Source # addPBNLExactly :: PBStore m -> PBSum -> Integer -> m () Source # addPBNLAtLeastSoft :: PBStore m -> Lit -> PBSum -> Integer -> m () Source # addPBNLAtMostSoft :: PBStore m -> Lit -> PBSum -> Integer -> m () Source # addPBNLExactlySoft :: PBStore m -> Lit -> PBSum -> Integer -> m () Source #

class AddClause m a => AddXORClause m a | a -> m where Source #

Minimal complete definition

addXORClause

Methods

addXORClause Source #

Arguments

:: a
-> [Lit]	literals `[l1, l2, …, ln]`
-> Bool	rhs
-> m ()

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

addXORClauseSoft Source #

Arguments

:: a
-> Lit	Selector literal `sel`
-> [Lit]	literals `[l1, l2, …, ln]`
-> Bool	rhs
-> m ()

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

Instances

Instances details

AddXORClause IO Solver Source #
Instance details Defined in ToySolver.SAT.Solver.CDCL Methods addXORClause :: Solver -> [Lit] -> Bool -> IO () Source # addXORClauseSoft :: Solver -> Lit -> [Lit] -> Bool -> IO () Source #

Type-2 SOS constraints

addSOS2 :: AddClause m a => a -> [Lit] -> m () Source #

Add a type-2 SOS constraint

At most two adjacnt literals can be true.

evalSOS2 :: IModel m => m -> [Lit] -> Bool Source #

Evaluate type-2 SOS constraint