Accéder directement au contenu Accéder directement à la navigation
Nouvelle interface
Communication dans un congrès

Abacus: A New Hybrid Encoding for SAT Problems

Résumé : En général, un bon encodage doit viser à améliorer l'efficacité de la résolution (indépendamment du solveur choisi) et à produire une instance de taille raisonnable. Nous proposons l'encodage Abacus, un nouvel encodage hybride qui combine les encodages Log et Order pour offrir un bon compromis entre la taille de l'instance et l'efficacité de la résolution. Fondé sur l'idée du boulier chinois, l'Abacus décompose les valeurs entières en unités et dizaines. Les unités sont définies avec l'encodage Log et les dizaines avec l'encodage Order. Cette approche permet un bon compromis entre une représentation compacte des valeurs et l'efficacité de la résolution.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal.univ-angers.fr/hal-03385029
Contributeur : Claudia VASCONCELLOS-GAETE Connectez-vous pour contacter le contributeur
Soumis le : mardi 19 octobre 2021 - 12:10:14
Dernière modification le : lundi 14 novembre 2022 - 02:42:07
Archivage à long terme le : : jeudi 20 janvier 2022 - 18:53:07

Fichier

ictai2020.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Claudia Vasconcellos-Gaete, Vincent Barichard, Frédéric Lardeux. Abacus: A New Hybrid Encoding for SAT Problems. 2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI), Nov 2020, Baltimore, United States. pp.145-152, ⟨10.1109/ICTAI50040.2020.00033⟩. ⟨hal-03385029⟩

Partager

Métriques

Consultations de la notice

11

Téléchargements de fichiers

41