SMT-based verification applied to non-convex optimization problems
This paper presents a novel, complete, and flexible optimization algorithm, which relies on recursive executions that re-constrains a model-checking procedure based on Satisfiability Modulo Theories (SMT). This SMT-based optimization technique is able to optimize a wide range of functions, including...
| Hauptverfasser: | , , , |
|---|---|
| Format: | Conference item |
| Veröffentlicht: |
Institute of Electrical and Electronics Engineers
2017
|
| _version_ | 1826281389868187648 |
|---|---|
| author | Araujo, R Bessa, I Cordeiro, L Filho, J |
| author_facet | Araujo, R Bessa, I Cordeiro, L Filho, J |
| author_sort | Araujo, R |
| collection | OXFORD |
| description | This paper presents a novel, complete, and flexible optimization algorithm, which relies on recursive executions that re-constrains a model-checking procedure based on Satisfiability Modulo Theories (SMT). This SMT-based optimization technique is able to optimize a wide range of functions, including non-linear and non-convex problems using fixed-point arithmetic. Although SMT-based optimization is not a new technique, this work is the pioneer in solving non-linear and non-convex problems based on SMT; previous applications are only able to solve integer and rational linear problems. The proposed SMT-based optimization algorithm is compared to other traditional optimization techniques. Experimental results show the efficiency and effectiveness of the proposed algorithm, which finds the optimal solution in all evaluated benchmarks, while traditional techniques are usually trapped by local minima. |
| first_indexed | 2024-03-07T00:28:05Z |
| format | Conference item |
| id | oxford-uuid:7ecf104f-c9f4-4ee7-b84c-4b1e08ba57f2 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:28:05Z |
| publishDate | 2017 |
| publisher | Institute of Electrical and Electronics Engineers |
| record_format | dspace |
| spelling | oxford-uuid:7ecf104f-c9f4-4ee7-b84c-4b1e08ba57f22022-03-26T21:12:34ZSMT-based verification applied to non-convex optimization problemsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:7ecf104f-c9f4-4ee7-b84c-4b1e08ba57f2Symplectic Elements at OxfordInstitute of Electrical and Electronics Engineers2017Araujo, RBessa, ICordeiro, LFilho, JThis paper presents a novel, complete, and flexible optimization algorithm, which relies on recursive executions that re-constrains a model-checking procedure based on Satisfiability Modulo Theories (SMT). This SMT-based optimization technique is able to optimize a wide range of functions, including non-linear and non-convex problems using fixed-point arithmetic. Although SMT-based optimization is not a new technique, this work is the pioneer in solving non-linear and non-convex problems based on SMT; previous applications are only able to solve integer and rational linear problems. The proposed SMT-based optimization algorithm is compared to other traditional optimization techniques. Experimental results show the efficiency and effectiveness of the proposed algorithm, which finds the optimal solution in all evaluated benchmarks, while traditional techniques are usually trapped by local minima. |
| spellingShingle | Araujo, R Bessa, I Cordeiro, L Filho, J SMT-based verification applied to non-convex optimization problems |
| title | SMT-based verification applied to non-convex optimization problems |
| title_full | SMT-based verification applied to non-convex optimization problems |
| title_fullStr | SMT-based verification applied to non-convex optimization problems |
| title_full_unstemmed | SMT-based verification applied to non-convex optimization problems |
| title_short | SMT-based verification applied to non-convex optimization problems |
| title_sort | smt based verification applied to non convex optimization problems |
| work_keys_str_mv | AT araujor smtbasedverificationappliedtononconvexoptimizationproblems AT bessai smtbasedverificationappliedtononconvexoptimizationproblems AT cordeirol smtbasedverificationappliedtononconvexoptimizationproblems AT filhoj smtbasedverificationappliedtononconvexoptimizationproblems |