Name
Abstract | ||
|---|---|---|
We show a reduction to propositional logic from a Boolean combination of inequalities of the form vi 驴 vj + c and vi vj + c, where c is a constant and vi, vj are variables of type real or integer. Equalities and uninterpreted functions can be expressed in this logic as well. We discuss the advantages of using this reduction as compared to competing methods, and present experimental results that support our claims. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1007/3-540-45657-0_16 | CAV |
Keywords | Field | DocType |
boolean combination,present experimental result,separation formulas,uninterpreted function,form vi,vi vj,propositional logic | Graph theory,Constraint satisfaction,Computer science,Chordal graph,Automated theorem proving,Propositional calculus,Algorithm,Disjunctive normal form,Boolean algebra,Boolean data type | Conference |
ISBN | Citations | PageRank |
3-540-43997-8 | 48 | 3.05 |
References | Authors | |
7 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ofer Strichman | 1 | 1071 | 63.61 |
| Sanjit A. Seshia | 2 | 2226 | 168.09 |
| Randal E. Bryant | 3 | 9204 | 1194.64 |