1. A computer-implemented method for determining satisfiability of a function, said method comprising: accessing a function comprising a plurality of variables; and representing said function as a canonical decision diagram structure having a plurality of vertices and a plurality of sink nodes, each of said vertices associated with a respective variable of said function, wherein said vertices include a vertex that represents a domain of more than two values for a variable associated with said vertex; wherein said function is satisfiable for values of said variables that resolve to true within said decision diagram structure and is unsatisfiable for values of said variables that resolve to false within said decision diagram structure.