satd.cnf

Undocumented in source.

Members

Aliases

Literal
alias Literal = long

0 は \overline \Lambda (conflict node) を表す。 \cdots, -3, -2, -1, 1, 2, 3, \cdots を通常のリテラルのために利用する。 x > 0 であるとき、 正の整数 x は、x を意味する。 負の整数 -x は、\lnot x を意味する。

Set
alias Set(T) = RedBlackTree!T
Undocumented in source.

Functions

negate
Literal negate(Literal lit)

与えられた Literal を否定したものを返す。

Structs

CNF
struct CNF
Undocumented in source.
Clause
struct Clause

Meta