Averest


TwoSAT Type

Given a PU allocation, the SAT constraints (without switching Dup nodes) yields a 2SAT problem which is described by the following data type that offers facts for the node and buffer ordering as well as constraints which are equivalences between the latter.

Union cases

Union case Description

BufOrd(string, string)

Full Usage: BufOrd(string, string)

Parameters:
    Item1 : string
    Item2 : string

Item1 : string
Item2 : string

Equat(int * int, string * string)

Full Usage: Equat(int * int, string * string)

Parameters:
    Item1 : int * int
    Item2 : string * string

Item1 : int * int
Item2 : string * string

NodOrd(int, int)

Full Usage: NodOrd(int, int)

Parameters:
    Item1 : int
    Item2 : int

Item1 : int
Item2 : int