LiveZilla Live Chat Software

Constellation, le dépôt institutionnel de l'Université du Québec à Chicoutimi

Reformulation of SAT into a polynomial box-constrained optimization problem

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.

[img] PDF - Version acceptée
Administrateurs seulement jusqu´à 12 Novembre 2021.

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:21 janv. 2021 01:35
Afficher les statistiques de telechargements

Éditer le document (administrateurs uniquement)

Creative Commons LicenseSauf indication contraire, les documents archivés dans Constellation sont rendus disponibles selon les termes de la licence Creative Commons "Paternité, pas d'utilisation commerciale, pas de modification" 2.5 Canada.

Bibliothèque Paul-Émile-Boulet, UQAC
555, boulevard de l'Université
Chicoutimi (Québec)  CANADA G7H 2B1
418 545-5011, poste 5630