Name
Abstract | ||
|---|---|---|
In this paper, we proposed a novel interpolant generation algorithm without constructing the resolution graph of the unsatisfiability proof. Our algorithm generates the interpolant by building sub-interpolants from conflict analyses and then merges them based on the last decision conflict. The experimental results show that our algorithm has the advantages over the prior interpolant generation techniques in both memory usage and interpolation circuit size. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1145/1687399.1687402 | ICCAD |
Keywords | Field | DocType |
last decision conflict,interpolation circuit size,unsatisfiability proof,memory usage,conflict analysis,prior interpolant generation technique,interpolant generation,novel interpolant generation algorithm,resolution graph,analog,design automation,optimization,algorithm design and analysis,logic gates,interpolation,data mining,verification,circuit,graph theory,generic algorithm | Graph theory,Graph,Logic gate,Algorithm design,Computer science,Interpolation,Algorithm,Theoretical computer science,Electronic design automation | Conference |
Citations | PageRank | References |
2 | 0.40 | 7 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chih-Jen Hsu | 1 | 32 | 4.95 |
| Shao-Lun Huang | 2 | 56 | 23.09 |
| Chi-An Wu | 3 | 38 | 3.86 |
| Chung-Yang (Ric) Huang | 4 | 186 | 15.69 |