Control.Monad.SAT

A monadic interface to the SAT (minisat) solver.

The interface is inspired by ST monad. SAT and Lit are indexed by a "state" token, so you cannot mixup literals from different SAT computations.

SAT Monad

data SAT s a

Satisfiability monad.

Instances

MonadIO (SAT s)

Defined in Control.Monad.SAT

Methods

liftIO :: IO a -> SAT s a

Applicative (SAT s)

Defined in Control.Monad.SAT

Methods

pure :: a -> SAT s a

(<*>) :: SAT s (a -> b) -> SAT s a -> SAT s b

liftA2 :: (a -> b -> c) -> SAT s a -> SAT s b -> SAT s c

(*>) :: SAT s a -> SAT s b -> SAT s b

(<*) :: SAT s a -> SAT s b -> SAT s a

Functor (SAT s)

Defined in Control.Monad.SAT

Methods

fmap :: (a -> b) -> SAT s a -> SAT s b

(<$) :: a -> SAT s b -> SAT s a

Monad (SAT s)

Defined in Control.Monad.SAT

Methods

(>>=) :: SAT s a -> (a -> SAT s b) -> SAT s b

(>>) :: SAT s a -> SAT s b -> SAT s b

return :: a -> SAT s a

MonadUnliftIO (SAT s)

Defined in Control.Monad.SAT

Methods

withRunInIO :: ((forall a. SAT s a -> IO a) -> IO b) -> SAT s b

runSAT :: (forall s. SAT s a) -> IO a

Run SAT computation.

runSATMaybe :: (forall s. SAT s a) -> IO (Maybe a)

Run SAT computation. Return Nothing if UnsatException is thrown.

data UnsatException

Unsatisfiable exception.

It may be thrown by various functions: in particular solve and solve_, but also addClause, simplify.

The reason to use an exception is because after unsatisfiable state is reached the underlying solver instance is unusable. You may use runSATMaybe to catch it.

Constructors

UnsatException

Instances

Exception UnsatException

Defined in Control.Monad.SAT

Methods

toException :: UnsatException -> SomeException

fromException :: SomeException -> Maybe UnsatException

displayException :: UnsatException -> String

Show UnsatException

Defined in Control.Monad.SAT

Methods

showsPrec :: Int -> UnsatException -> ShowS

show :: UnsatException -> String

showList :: [UnsatException] -> ShowS

Literals

data Lit s

Literal.

To negate literate use neg.

Instances

Show (Lit s)

Defined in Control.Monad.SAT

Methods

showsPrec :: Int -> Lit s -> ShowS

show :: Lit s -> String

showList :: [Lit s] -> ShowS

Eq (Lit s)

Defined in Control.Monad.SAT

Methods

(==) :: Lit s -> Lit s -> Bool

(/=) :: Lit s -> Lit s -> Bool

Ord (Lit s)

Defined in Control.Monad.SAT

Methods

compare :: Lit s -> Lit s -> Ordering

(<) :: Lit s -> Lit s -> Bool

(<=) :: Lit s -> Lit s -> Bool

(>) :: Lit s -> Lit s -> Bool

(>=) :: Lit s -> Lit s -> Bool

max :: Lit s -> Lit s -> Lit s

min :: Lit s -> Lit s -> Lit s

Neg (Lit s)

Negate literal.

Defined in Control.Monad.SAT

Methods

neg :: Lit s -> Lit s

newLit :: SAT s (Lit s)

Create fresh literal.

Negation

class Neg a where

Methods

neg :: a -> a

Instances

Neg (Lit s)

Negate literal.

Defined in Control.Monad.SAT

Methods

neg :: Lit s -> Lit s

Neg (Prop s)

Negation of propositional formulas.

Defined in Control.Monad.SAT

Methods

neg :: Prop s -> Prop s

Clauses

addClause :: [Lit s] -> SAT s ()

Add a clause to the solver.

assertAtLeastOne :: [Lit s] -> SAT s ()

At least one -constraint.

Alias to addClause.

assertAtMostOne :: [Lit s] -> SAT s ()

At most one -constraint.

Uses atMostOnePairwise for lists of length 2 to 5 and atMostOneSequential for longer lists.

The cutoff is chosen by picking encoding with least clauses: For 5 literals, atMostOnePairwise needs 10 clauses and assertAtMostOneSequential needs 11 (and 4 new variables). For 6 literals, atMostOnePairwise needs 15 clauses and assertAtMostOneSequential needs 14.

assertAtMostOnePairwise :: [Lit s] -> SAT s ()

At most one -constraint using pairwise encoding.

\[ \mathrm{AMO}(x_1, \ldots, x_n) = \bigwedge_{1 \le i < j \le n} \neg x_i \lor \neg x_j \]

\(n(n-1)/2\) clauses, zero auxiliary variables.

assertAtMostOneSequential :: [Lit s] -> SAT s ()

At most one -constraint using sequential counter encoding.

\[ \mathrm{AMO}(x_1, \ldots, x_n) = (\neg x_1 \lor s_1) \land (\neg x_n \lor \neg s_{n-1}) \land \bigwedge_{1 < i < n} (\neg x_i \lor a_i) \land (\neg a_{i-1} \lor a_i) \land (\neg x_i \lor \neg a_{i-1}) \]

Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints, Proceedings of Principles and Practice of Constraint Programming (CP), 827–831 (2005)

\(3n-4\) clauses, \(n-1\) auxiliary variables.

We optimize the two literal case immediately ([resolution](https:/en.wikipedia.orgwiki/Resolution_(logic)) on \(s_1\).

\[ (\neg x_1 \lor s_1) \land (\neg x_2 \lor \neg s_1) \Longrightarrow \neg x_1 \lor \neg x_2 \]

assertEqual :: Lit s -> Lit s -> SAT s ()

Assert that two literals are equal.

assertAllEqual :: [Lit s] -> SAT s ()

Assert that all literals in the list are equal.

Propositional formulas

data Prop s

Propositional formula.

Instances

Show (Prop s)

Defined in Control.Monad.SAT

Methods

showsPrec :: Int -> Prop s -> ShowS

show :: Prop s -> String

showList :: [Prop s] -> ShowS

Eq (Prop s)

Defined in Control.Monad.SAT

Methods

(==) :: Prop s -> Prop s -> Bool

(/=) :: Prop s -> Prop s -> Bool

Ord (Prop s)

Defined in Control.Monad.SAT

Methods

compare :: Prop s -> Prop s -> Ordering

(<) :: Prop s -> Prop s -> Bool

(<=) :: Prop s -> Prop s -> Bool

(>) :: Prop s -> Prop s -> Bool

(>=) :: Prop s -> Prop s -> Bool

max :: Prop s -> Prop s -> Prop s

min :: Prop s -> Prop s -> Prop s

Neg (Prop s)

Negation of propositional formulas.

Defined in Control.Monad.SAT

Methods

neg :: Prop s -> Prop s

true :: Prop s

True Prop.

false :: Prop s

False Prop.

lit :: Lit s -> Prop s

Make Prop from a literal.

(\/) :: Prop s -> Prop s -> Prop s infixr 5

Disjunction of propositional formulas, or.

(/\) :: Prop s -> Prop s -> Prop s infixr 6

Conjunction of propositional formulas, and.

(<->) :: Prop s -> Prop s -> Prop s

Equivalence of propositional formulas.

(-->) :: Prop s -> Prop s -> Prop s

Implication of propositional formulas.

xor :: Prop s -> Prop s -> Prop s

Exclusive or, not equal of propositional formulas.

ite :: Prop s -> Prop s -> Prop s -> Prop s

If-then-else.

Semantics of ite c t f are (c /\ t) \/ (neg c /\ f).

addDefinition :: Prop s -> SAT s (Lit s)

Add definition of Prop. The resulting literal is equivalent to the argument Prop.

addProp :: Prop s -> SAT s ()

Assert that given Prop is true.

This is equivalent to

addProp p = do
    l <- addDefinition p
    addClause l

but avoid creating the definition, asserting less clauses.

Clause definitions

trueLit :: SAT s (Lit s)

True literal.

falseLit :: SAT s (Lit s)

False literal

addConjDefinition :: Lit s -> [Lit s] -> SAT s ()

Add conjunction definition.

addConjDefinition x ys asserts that x ↔ ⋀ yᵢ

addDisjDefinition :: Lit s -> [Lit s] -> SAT s ()

Add disjunction definition.

addDisjDefinition x ys asserts that x ↔ ⋁ yᵢ

Solving

solve :: Traversable model => model (Lit s) -> SAT s (model Bool)

Search and return a model.

solve_ :: SAT s ()

Search without returning a model.

Simplification

simplify :: SAT s ()

Removes already satisfied clauses.

Statistics

numberOfVariables :: SAT s Int

The current number of variables.

numberOfClauses :: SAT s Int

The current number of original clauses.

numberOfLearnts :: SAT s Int

The current number of learnt clauses.

numberOfConflicts :: SAT s Int

The current number of conflicts.