Back to Search
Start Over
Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions
- Source :
- SYNASC
- Publication Year :
- 2018
- Publisher :
- IEEE, 2018.
-
Abstract
- Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories. In this paper, we overview our recent approach called Incremental Linearization, which successfully tackles the problems of SMT over the theories of nonlinear arithmetic over the reals (NRA), nonlinear arithmetic over the integers (NIA) and their combination, and of NRA augmented with transcendental (exponential and trigonometric) functions (NTA). Moreover, we showcase some of the experimental results and outline interesting future directions.
- Subjects :
- Transcendental function
Modulo
0102 computer and information sciences
02 engineering and technology
01 natural sciences
Satisfiability
Exponential function
010201 computation theory & mathematics
Linearization
Satisfiability modulo theories
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
Transcendental number
Arithmetic
Trigonometry
Mathematics
Subjects
Details
- Database :
- OpenAIRE
- Journal :
- 2018 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
- Accession number :
- edsair.doi.dedup.....2e0912cec08ccd6ac7e7a396d0af6ee3