ac-library-hs-1.4.0.0: Data structures and algorithms
Safe HaskellNone
LanguageGHC2021

AtCoder.TwoSat

Description

Solves 2-SAT.

For variables \(x_0, x_1, \cdots, x_{N - 1}\) and clauses with form

  • \((x_i = f) \lor (x_j = g)\)

it decides whether there is a truth assignment that satisfies all clauses.

Example

Expand
>>> import AtCoder.TwoSat qualified as TS
>>> import Data.Bit (Bit(..))
>>> ts <- TS.new 1
>>> TS.addClause ts 0 False 0 False -- x_0 == False || x_0 == False
>>> TS.satisfiable ts
True

>>> TS.answer ts
[0]

Since: 1.0.0.0

Synopsis

TwoSat

data TwoSat s Source #

2-SAT state.

Since: 1.0.0.0

Constructor

new :: PrimMonad m => Int -> m (TwoSat (PrimState m)) Source #

Creates a 2-SAT of \(n\) variables and \(0\) clauses.

Constraints

  • \(0 \leq n\)

Complexity

  • \(O(n)\)

Since: 1.0.0.0

Clause building

addClause :: (HasCallStack, PrimMonad m) => TwoSat (PrimState m) -> Int -> Bool -> Int -> Bool -> m () Source #

Adds a clause \((x_i = f) \lor (x_j = g)\).

Constraints

  • \(0 \leq i \lt n\)
  • \(0 \leq j \lt n\)

Complexity

  • \(O(1)\) amortized.

Since: 1.0.0.0

Solvers

satisfiable :: PrimMonad m => TwoSat (PrimState m) -> m Bool Source #

If there is a truth assignment that satisfies all clauses, it returns True. Otherwise, it returns False.

Constraints

  • You may call it multiple times.

Complexity

  • \(O(n + m)\), where \(m\) is the number of added clauses.

Since: 1.0.0.0

answer :: PrimMonad m => TwoSat (PrimState m) -> m (Vector Bit) Source #

Returns a truth assignment that satisfies all clauses of the last call of satisfiable. If we call it before calling satisfiable or when the last call of satisfiable returns False, it returns the vector of length \(n\) with undefined elements.

Complexity

  • \(O(n)\)

Since: 1.0.0.0

unsafeAnswer :: PrimMonad m => TwoSat (PrimState m) -> m (Vector Bit) Source #

answer without making copy.

Complexity

  • \(O(1)\)

Since: 1.0.0.0