Name
Abstract | ||
|---|---|---|
Recently, the satisfiability modulo theories (SMT) is concerned widely in both the industry and academia, it is different from the traditional Boolean satisfiability problem (SAT) because of its higher abstraction and stronger representation. However, the application is not limited to the satisfiablity, which also needs the quantity of the solution. At the same time, the solution space calculated by linear arithmetic is very common, which can map to the convex polyhedron constructed with the linear constraints. Therefore, the volume of the convex can reflect the quantity of the solution, which can estimate by some existing algorithms. Furthermore, considering the different distribution on the solution space, we estimate the mass of the convex polyhedron instead of the simple volume to describe the object tangible, using Monte Carlo integration, which have good correctness in low dimension and perform efficiently in high dimension. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1109/CCIS.2016.7790239 | 2016 4th International Conference on Cloud Computing and Intelligence Systems (CCIS) |
Keywords | Field | DocType |
SMT,Solution space,Linear arithmetic,Convex polyhedron,Volume,Mass,Monte Carlo integration | Mathematical optimization,Computer science,Convex combination,Boolean satisfiability problem,Convex set,Subderivative,Convex polytope,Convex analysis,Linear matrix inequality,Satisfiability modulo theories | Conference |
ISSN | ISBN | Citations |
2376-5933 | 978-1-5090-1257-2 | 0 |
PageRank | References | Authors |
0.34 | 9 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Zhenhui Xu | 1 | 0 | 0.34 |
| Yuting Yang | 2 | 44 | 10.79 |
| Nan Jiang | 3 | 0 | 0.34 |
| Chunxu Zhang | 4 | 0 | 1.01 |
| Pei Huang | 5 | 0 | 0.34 |