Jacquet Stéphane et Hallé Sylvain. (2020). Reformulation of SAT into a polynomial box-constrained optimization problem. Dans : International Conference on Integrated Formal Methods (IFM) , 16-20 November 2020, Lugano, Switzerland.
Prévisualisation |
PDF
- Version acceptée
308kB |
Résumé
In order to leverage the capacities of non-linear constraint solvers, we propose a reformulation of SAT into a box-constrained optimization problem where the objective function is polynomial. We prove that any optimal solution of the numerical problem corresponds to a solution of the Boolean formula, and demonstrate a stopping criterion that can be used with a numerical solver.
| Type de document: | Matériel de conférence (Non spécifié) |
|---|---|
| Date: | 13 Novembre 2020 |
| Sujets: | Sciences naturelles et génie > Sciences mathématiques > Mathématiques fondamentales |
| Département, module, service et unité de recherche: | Départements et modules > Département d'informatique et de mathématique Départements et modules > Département d'informatique et de mathématique > Module d'informatique et de mathématique |
| Liens connexes: | |
| Mots-clés: | Optimization, non-linear constraint solvers |
| Déposé le: | 21 janv. 2021 01:35 |
|---|---|
| Dernière modification: | 12 nov. 2021 05:10 |
Éditer le document (administrateurs uniquement)