# Abacus: Un nouvel encodage pour SAT

Vasconcellos Claudia, Vincent Barichard, Lardeux Frédéric

► To cite this version:

Vasconcellos Claudia, Vincent Barichard, Lardeux Frédéric. Abacus: Un nouvel encodage pour SAT. Seizièmes Journées Francophone de Programmation par Contraintes (JFPC'21), Jun 2021, Nice, France. hal-04031129

HAL Id: hal-04031129

https://univ-angers.hal.science/hal-04031129

Submitted on 17 Mar 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Abacus : Un nouvel encodage pour SAT

Claudia Vasconcellos

Vincent Barichard

Frédéric Lardeux

Laboratoire d'Etude et de Recherche en Informatique d'Angers, LERIA,
EA 2645, SFR MathSTIC, Université d'Angers,
Faculté des Sciences, 2 Bd Lavoisier, 49045 Angers, FRANCE
{claudia.vasconcellos,vincent.barichard,frederic.lardeux}@univ-angers.fr

## Résumé

Cet article résume le travail publié dans [7]. 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.

## 1 Introduction

Dans les dernières années, la modélisation en CSP est devenue assez intuitive grâce aux outils et langages comme [6, 5] bien que la résolution de certaines contraintes reste encore problématique. De son côté, l'approche SAT est reconnue pour la puissance de ses solveurs mais aussi pour la complexité de sa modélisation.

L'encodage d'un modèle CSP en SAT implique la modélisation de chaque variable entière et des contraintes en utilisant les variables booléennes créées sans perdre le sens de chacune des contraintes CSP dans le problème. Les encodages CSP vers SAT « standard » (Direct [3], Log [4], Support et Order [2]) se concentrent généralement sur certains aspects tels que la simplificité, la compacité ou les bonnes performances pour des contraintes spécifiques, la puissance de propagation. Les encodages « hybrides » (Direct-Support, Direct-Order, Log-Support et Compact order) combinent des encodages pour obtenir le meilleur de chacun d'entre eux (Figure 1).

<figure><img src="image_2.png" /><figcaption>FIGURE 1 – L'encodage Abacus représente un compromis entre la taille de l'instance et la puissance de propagation</figcaption></figure>

## 2 L'encodage Abacus

Nous proposons l'Abacus, un nouvel encodage basé sur l'idée du boulier, le célèbre outil de calcul chinois lié au système de numération décimal. Cet encodage décompose la valeur des entiers en unités et dizaines. Les unités sont traitées avec l'encodage Log et les dizaines avec l'encodage Order.

<figure><img src="image_3.png" /></figure>

Le nombre d'unités et de dizaines est déterminé par la base d'encodage B. Ce nombre correspond à une puissance de 2 afin de garder la consistance avec l'encodage Log utilisé pour les unités.

### 2.1 Définition de l'encodage

Pour une variable entière X définie sur le domaine $Dom(X) = [lb..ub]$, l'encodage Abacus est :

$$ 
\begin{gathered}
x^{b^{+}} \dots x^{b^{-}} \quad x_{u-1} \dots x_0 \qquad (1) \\
b^{+} = \lfloor \frac{ub}{B} \rfloor, \quad b^{-} = \lfloor \frac{lb}{B} \rfloor, \quad u = \log_2 B
\end{gathered}
$$
## 2.2 L'offset

Pour éviter la sur-représentation des valeurs, on introduit le concept d'offset, un paramètre qui prend différentes valeurs selon le domaine de chacune des variables. Pour une variable entière X définie sur le domaine $Dom(X) = [lb..ub]$, l'offset est :

$$o^X = lb - lb \mod B \quad (2)$$

## 2.3 L'encodage de l'addition

Pour une addition entière $X + Y = Z$, l'encodage se fait en deux étapes : les unités sont d'abord traitées avec des additionneurs complets et, ensuite, les dizaines sont traités selon quatre règles qui prennent en compte la retenue venant des unités. Ces règles sont :

**R1** : Si les dizaines de X et Y sont vraies, alors la dizaine correspondant a Z doit être vraie aussi.

**R2** : Idem que R1, mais en considérant le déborde-ment généré au niveau de l'addition des unités.

**R3** : Si les dizaines de X et Y sont fausses, alors la dizaine correspondant à Z doit être fausse aussi.

**R4** : Idem que R3, mais en considérant le déborde-ment généré au niveau de l'addition des unités.

## 2.4 Évaluation de l'encodage : La puissance de propagation

L'un des critères d'évaluation des codages est la puissance de la propagation unitaire. Cette métrique correspond à la quantité d'information propagée, c'est-à-dire au nombre de variables de décision affectées par chaque décision fait par le solveur.

Sur la base de l'algorithme de Brain et al. [1] pour générer automatiquement des codages complets de propagation (PCE), nous en avons développé une version simplifiée (voir l'article original). L'encodage Abacus est PCE dans le sens où il infère le maximum d'informations possible en utilisant la propagation unitaire.

# 3 Résultats

L'évaluation de l'encodage Abacus a été menée sur des instances des problèmes du Carré Magique et des Règles de Golomb. La taille des instances (nombre de variables) et leur puissance de propagation (nombre des variables propagées par décision) ont été les deux critères observées. Pour chaque instance différentes valeurs de base d'encodage ($B$) ont été testées. Nous avons donc pu répliquer le comportement des encodages Log ($B = 1$) et Order ($B_{max}$) et les comparer à l'encodage Abacus.

L'encodage Log fournit toujours les instances les plus petites, mais il obtient de mauvais résultats en termes de puissance de propagation. Au contraire, l'encodage Order fournit des instances de grande taille, mais avec un meilleur pouvoir de propagation.

Les meilleurs résultats correspondent aux encodages fournissant le plus grand nombre de solutions dans le temps imparti, puis, lorsque toutes les solutions sont trouvées, à ceux dont le temps d'exécution est le plus court. Ils sont principalement obtenus pour les bases qui ne correspondent pas aux encodages Log ou Order. On constate que sur les petites instances, le pouvoir de propagation contrebalance largement le nombre de solutions. Lorsque les instances deviennent plus grandes, les bases élevées limitent l'explosion du nombre de variables et de clauses.

Finalement on peut dire que les résultats obtenus pour les deux classes de problèmes montrent que l'Abacus peut établir un bon compromis entre la taille des instances générées et l'efficacité de la résolution.

# Références

[1] M. BRAIN, L. HADAREAN, D. KROENING et R. MARTINS : Automatic generation of propagation complete SAT encodings. *In Verification, Model Checking, and Abstract Interpretation*, pages 536-556, 2016.

[2] J. CRAWFORD et A. BAKER : Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems. *In Proceedings of the 12th National Conference on Artificial Intelligence*, page 1092-1097, 1994.

[3] J. DE KLEER : A comparison of ATMS and CSP techniques. *In Proceedings of the 11th IJCAI (vol. 1)*, pages 290-296, 1989.

[4] K. IWAMA et S. MIYAZAKI : SAT-variable complexity of hard combinatorial problems. *In 13th IFIP World Computer Congress*, pages 253-258, 1994.

[5] N. NETHERCOTE, P. STUCKEY, R. BECKET, S. BRAND, G. DUCK et G. TACK : Minizinc : Towards a standard CP modelling language. *In CP 2007*, pages 529-543, 2007.

[6] C. SCHULTE : Programming Constraint Services : High-Level Programming of Standard and New Constraint Services. LNCS. Springer, 2002.

[7] C. VASCONCELLOS-GAETE, V. BARICHARD et F. LARDEUX : Abacus : A new hybrid encoding for sat problems. *In 2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI)*, pages 145-152. IEEE, 2020.