Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Graph.TwoSat

Description

\(O(V + E)\) 2-satisfiability problem.

2-satisfiablity problem is about finding one possible assignment to boolean variables \(\{x_i\}_i\) under a conjunciton of or clauses: \(\vee_i \{x_{i,1} \wedge x_{i,2}\}_i\).

Example

Use twoSat for denoting and solving the problem:

let !nClauses = (2 * n * pred n)
let !res = twoSat n nClauses $ tsb -> do
      forM_ [0 .. n - 1] $ v1 -> do
        let (!x1, !y1) = xys U.! v1
        forM_ [v1 + 1 .. n - 1] $ v2 -> do
          let (!x2, !y2) = xys U.! v2
          when (abs (x1 - x2) < d) $ do
            addOrTSB tsb (F v1) (F v2)
          when (abs (x1 - y2) < d) $ do
            addOrTSB tsb (F v1) (T v2)
          when (abs (y1 - x2) < d) $ do
            addOrTSB tsb (T v1) (F v2)
          when (abs (y1 - y2) < d) $ do
            addOrTSB tsb (T v1) (T v2)

Typical problems

ALPC H - Two Sat. See also: https://drken1215.hatenablog.com/entry/2023/05/07/001800

Synopsis

data TF a
- = T !a
- | F !a
asTF :: a -> Bool -> TF a
data TwoSatBuilder s = TwoSatBuilder {
- nVarsTSB :: !Int
- bufTSB :: !(Buffer s (Int, Int))
}
newTSB :: PrimMonad m => Int -> Int -> m (TwoSatBuilder (PrimState m))
addOrTSB :: PrimMonad m => TwoSatBuilder (PrimState m) -> TF Int -> TF Int -> m ()
addOrTSB' :: PrimMonad m => TwoSatBuilder (PrimState m) -> Int -> Bool -> Int -> Bool -> m ()
solveTS :: Int -> Vector (Int, Int) -> Maybe (Vector Bool)
twoSat :: Int -> Int -> (forall s. TwoSatBuilder s -> ST s ()) -> Maybe (Vector Bool)

Documentation

data TF a #

Data with True | False tag.

Constructors

T !a
F !a

asTF :: a -> Bool -> TF a #

Converts the value and boolean pair into TF.

data TwoSatBuilder s #

2-satisfiability problem with constraints being added.

Constructors

TwoSatBuilder
Fields nVarsTSB :: !Int The number of variables. bufTSB :: !(Buffer s (Int, Int)) Implication graph edges.

newTSB :: PrimMonad m => Int -> Int -> m (TwoSatBuilder (PrimState m)) #

\(O(V+E)\) Creates a two-sat builder.

addOrTSB :: PrimMonad m => TwoSatBuilder (PrimState m) -> TF Int -> TF Int -> m () #

\(O(1)\) Adds an or clause: \(x1 = b1 || x2 = b2\).

addOrTSB' :: PrimMonad m => TwoSatBuilder (PrimState m) -> Int -> Bool -> Int -> Bool -> m () #

\(O(1)\) Adds an or clause: \(x1 = b1 || x2 = b2\).

solveTS :: Int -> Vector (Int, Int) -> Maybe (Vector Bool) #

\(O(V + E)\)

twoSat :: Int -> Int -> (forall s. TwoSatBuilder s -> ST s ()) -> Maybe (Vector Bool) #

\(O(V+E)\) The main interface of two-sat solve.