Safe Haskell	None
Language	Haskell2010

Control.Monad.SAT

Contents

SAT Monad
Literals
- Negation
Clauses
- Propositional formulas
- Clause definitions
Solving
Simplification
Statistics

Description

A monadic interface to the SAT (PureSAT) 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.

Synopsis

data SAT s a
runSATMaybe :: (forall s. SAT s a) -> Maybe a
data Lit s
newLit :: SAT s (Lit s)
boostScore :: Lit s -> SAT s ()
class Neg a where
- neg :: a -> a
addClause :: [Lit s] -> SAT s ()
assertAtLeastOne :: [Lit s] -> SAT s ()
assertAtMostOne :: [Lit s] -> SAT s ()
assertAtMostOnePairwise :: [Lit s] -> SAT s ()
assertAtMostOneSequential :: [Lit s] -> SAT s ()
assertEqual :: Lit s -> Lit s -> SAT s ()
assertAllEqual :: [Lit s] -> SAT s ()
data Prop s
true :: Prop s
false :: Prop s
lit :: Lit s -> Prop s
(\/) :: Prop s -> Prop s -> Prop s
(/\) :: Prop s -> Prop s -> Prop s
(<->) :: Prop s -> Prop s -> Prop s
(-->) :: Prop s -> Prop s -> Prop s
xor :: Prop s -> Prop s -> Prop s
ite :: Prop s -> Prop s -> Prop s -> Prop s
addDefinition :: Prop s -> SAT s (Lit s)
addProp :: Prop s -> SAT s ()
trueLit :: SAT s (Lit s)
falseLit :: SAT s (Lit s)
addConjDefinition :: Lit s -> [Lit s] -> SAT s ()
addDisjDefinition :: Lit s -> [Lit s] -> SAT s ()
solve :: Traversable model => model (Lit s) -> SAT s (model Bool)
solve_ :: SAT s ()
simplify :: SAT s ()
numberOfVariables :: SAT s Int
numberOfClauses :: SAT s Int
numberOfLearnts :: SAT s Int
numberOfLearntLiterals :: SAT s Int
numberOfConflicts :: SAT s Int
numberOfRestarts :: SAT s Int

SAT Monad

data SAT s a Source #

Satisfiability monad.

Instances

Instances details

Applicative (SAT s) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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

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

Run SAT computation.

Literals

data Lit s Source #

Literal.

To negate literate use neg.

Instances

Instances details

Show (Lit s) Source #
Instance details Defined in Control.Monad.SAT Methods showsPrec :: Int -> Lit s -> ShowS show :: Lit s -> String showList :: [Lit s] -> ShowS
Eq (Lit s) Source #
Instance details Defined in Control.Monad.SAT Methods (==) :: Lit s -> Lit s -> Bool (/=) :: Lit s -> Lit s -> Bool
Ord (Lit s) Source #
Instance details 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) Source #	Negate literal.
Instance details Defined in Control.Monad.SAT Methods neg :: Lit s -> Lit s Source #

newLit :: SAT s (Lit s) Source #

Create fresh literal.

boostScore :: Lit s -> SAT s () Source #

Boost score of the literal

Negation

class Neg a where Source #

Methods

neg :: a -> a Source #

Instances

Instances details

Neg (Lit s) Source #	Negate literal.
Instance details Defined in Control.Monad.SAT Methods neg :: Lit s -> Lit s Source #
Neg (Prop s) Source #	Negation of propositional formulas.
Instance details Defined in Control.Monad.SAT Methods neg :: Prop s -> Prop s Source #

Clauses

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

Add a clause to the solver.

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

At least one -constraint.

Alias to addClause.

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

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 () Source #

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 () Source #

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) 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 () Source #

Assert that two literals are equal.

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

Assert that all literals in the list are equal.

Propositional formulas

data Prop s Source #

Propositional formula.

Instances

Instances details

Show (Prop s) Source #
Instance details Defined in Control.Monad.SAT Methods showsPrec :: Int -> Prop s -> ShowS show :: Prop s -> String showList :: [Prop s] -> ShowS
Eq (Prop s) Source #
Instance details Defined in Control.Monad.SAT Methods (==) :: Prop s -> Prop s -> Bool (/=) :: Prop s -> Prop s -> Bool
Ord (Prop s) Source #
Instance details 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) Source #	Negation of propositional formulas.
Instance details Defined in Control.Monad.SAT Methods neg :: Prop s -> Prop s Source #

true :: Prop s Source #

True Prop.

false :: Prop s Source #

False Prop.

lit :: Lit s -> Prop s Source #

Make Prop from a literal.

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

Disjunction of propositional formulas, or.

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

Conjunction of propositional formulas, and.

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

Equivalence of propositional formulas.

(-->) :: Prop s -> Prop s -> Prop s Source #

Implication of propositional formulas.

xor :: Prop s -> Prop s -> Prop s Source #

Exclusive or, not equal of propositional formulas.

ite :: Prop s -> Prop s -> Prop s -> Prop s Source #

If-then-else.

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

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

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

addProp :: Prop s -> SAT s () Source #

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) Source #

True literal.

falseLit :: SAT s (Lit s) Source #

False literal

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

Add conjunction definition.

addConjDefinition x ys asserts that x ↔ ⋀ yᵢ

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

Add disjunction definition.

addDisjDefinition x ys asserts that x ↔ ⋁ yᵢ

Solving

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

Search and return a model.

solve_ :: SAT s () Source #

Search without returning a model.

Simplification

simplify :: SAT s () Source #

Removes already satisfied clauses.

Statistics

numberOfVariables :: SAT s Int Source #

The current number of variables.

numberOfClauses :: SAT s Int Source #

The current number of original clauses.

numberOfLearnts :: SAT s Int Source #

The current number of learnt clauses.

numberOfLearntLiterals :: SAT s Int Source #

The current number of learnt literals.

numberOfConflicts :: SAT s Int Source #

The current number of conflicts.

numberOfRestarts :: SAT s Int Source #

The current number of conflicts.