| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Algorithm.TwoSat
Synopsis
- twoSat :: Int -> Int -> (forall s. CNFBuilder s () -> ST s ()) -> Maybe (Vector Bool)
- type CNFBuilder s w = SparseGraphBuilder s w
- addClauseCNF :: PrimMonad m => CNFBuilder (PrimState m) () -> (Int, Bool) -> (Int, Bool) -> m ()
Documentation
Arguments
| :: Int | the number of variables |
| -> Int | upper bound on the number of clauses |
| -> (forall s. CNFBuilder s () -> ST s ()) | CNF(Conjunctive Normal Form) |
| -> Maybe (Vector Bool) |
2-SAT
(a0 \/ a1) /\ not a0
>>>twoSat 2 2 (\b -> addClauseCNF b (0, True) (1, True) >> addClauseCNF b (0, False) (0, False))Just [False,True]
a0 /\ not a1 /\ (not a0 \/ a1)
>>>print $ twoSat 2 3 (\b -> addClauseCNF b (0, True) (0, True) >> addClauseCNF b (1, False) (1, False) >> addClauseCNF b (0, False) (1, True))Nothing
a0 \/ not a0
>>>twoSat 1 1 (\b -> addClauseCNF b (0, True) (0, False))Just [True]
type CNFBuilder s w = SparseGraphBuilder s w Source #
addClauseCNF :: PrimMonad m => CNFBuilder (PrimState m) () -> (Int, Bool) -> (Int, Bool) -> m () Source #