Safe Haskell | None |
---|---|
Language | Haskell2010 |
Control.Monad.SAT
Description
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
Satisfiability monad.
runSATMaybe :: (forall s. SAT s a) -> Maybe a Source #
Run SAT
computation.
Literals
Literal.
To negate literate use neg
.
boostScore :: Lit s -> SAT s () Source #
Boost score of the literal
Negation
Clauses
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 \]
assertAllEqual :: [Lit s] -> SAT s () Source #
Assert that all literals in the list are equal.
Propositional formulas
Propositional formula.
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
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.
Simplification
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.