Determining satisfiability of a function with arbitrary domain constraints
View Patent ↗A function can be represented as a canonical decision diagram structure. Each vertex of the diagram is associated with a respective function variable. The vertices include at least one vertex that represents a domain of more than two values for the variable associated with the vertex. The decision diagram is used to evaluate the function to determine whether the function is satisfiable or unsatisfiable for given values of the variables.
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.
2. The method of claim 1 wherein said decision diagram structure is a directed acyclic graph (DAG).
3. The method of claim 1 wherein said function is represented in a form in which each of said variables has a finite domain.
4. The method of claim 1 wherein said function is represented using Boolean expressions of said variables before said function is transformed into said decision diagram structure.
5. The method of claim 4 further comprising:
mapping said Boolean expressions to respective if-then-else forms; and
transforming said if-then-else forms into said vertices.
6. The method of claim 1 further comprising evaluating said vertices for given values of said variables.
7. The method of claim 1 wherein said decision diagram structure is used to derive a normal form of said function, wherein said normal form is a conjunctive normal form or a disjunctive normal form.
8. A computer-readable medium having computer-executable components comprising:
a function comprising a plurality of variables; and
a canonical decision diagram structure representing said function and having a plurality of vertices, 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, and wherein said decision diagram structure is useful for determining satisfiability of said function.
9. The computer-readable medium of claim 8 wherein said function is satisfiable for values of said variables that resolve to a first sink node of said decision diagram structure and is unsatisfiable for values of said variables that resolve to a second sink node of said decision diagram structure.
10. The computer-readable medium of claim 8 wherein said decision diagram structure is a directed acyclic graph (DAG).
11. The computer-readable medium of claim 8 wherein said function is represented in a form in which each of said variables has a finite domain.
12. The computer-readable medium of claim 8 wherein said function is represented using Boolean expressions of said variables before said function is transformed into said decision diagram structure.
13. The computer-readable medium of claim 12 wherein said computer-executable components further comprise a table that maps Boolean expressions to respective if-then-else forms, wherein said if-then-else forms are transformed into said vertices.
14. The computer-readable medium of claim 8 wherein said computer-executable components further comprise a normal form of said function derived from said decision diagram structure, wherein said normal form is a conjunctive normal form or a disjunctive normal form.
15. A computer system comprising:
a central processing unit (CPU); and
a computer-readable medium having computer-readable instructions stored therein that are executable by said CPU, said instructions being executable to represent a function as a directed acyclic graph (DAG) 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; said instructions also executable to evaluate said function variables using said DAG, wherein said function is satisfiable for values of variables that evaluate to true using said DAG and is unsatisfiable for values of variables that evaluate to false using said DAG.
16. The computer system of claim 15 wherein said function is represented in a form in which each variable has a finite domain.
17. The computer system of claim 15 wherein said function is represented using Boolean expressions of said variables before said function is transformed into said DAG.
18. The computer system of claim 17 wherein said instructions are also executable to map said Boolean expressions to respective if-then-else forms and to transform said if-then-else forms into said vertices.
19. The computer system of claim 15 wherein said instructions are also executable to evaluate said vertices for given values of said variables.
20. The computer system of claim 15 wherein said decision diagram structure is used to derive a normal form of said function, wherein said normal form is a conjunctive normal form or a disjunctive normal form.