puresat-0.1: Pure Haskell SAT-solver
Safe HaskellNone
LanguageHaskell2010

Control.Monad.SAT

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

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.