Constraint Count

Projet M1 et M2 Informatique 2017-18, création d'un solver en calcul propositionnel.

On dispose d'un ensemble $X = \{ x_1, ..., x_N \}$ de $N$ variables propositionnelles ($Card(X) = N$)) et $K$ contraintes de cardinalité.

Afin de simplifier les calculs pour la vectorisation on désire utiliser la modélisation suivante:

• pour les variables on crée un tableau de $N$ caractères qui peuvent être assignés à 0 (faux), 1(vrai), 2 (non assigné)
• pour les contraintes on crée un tableau de $K * N$ caractères affectés à 0 ($x_i$), 1 ($¬x_i$), 4 (non utilisé)

Ainsi le problème :

$p ∨ ¬q ∨ ¬r$

$q ∨ r ∨ ¬s ∨ ¬t$

sera modélisé en :

On désire connaître pour une contrainte donnée, le nombre de variables à vrai (nb_true) et le nombre de variables non assignées (nb_unset) :

int cpp_cstr_count_true(char * RESTRICT v, char * RESTRICT c, size_t size, int *unset) {
	int nb_true = 0;
	int nb_unset = 0;
	
	for (size_t i=0; i < size; ++i) {
		int s = v[i] ^ c[i];
		if (s < 2) {
			nb_true += s;
		} else if (s < 4) {
			++nb_unset;
		}
	}

	*unset = nb_unset; 
	return nb_true;
}

On donne 4 implantations de cette fonction :

• version 1: celle donnée en C++ ci-dessus et qui est traduite par le compilateur
• version 2 : version assembleur vectorisée
• version 3 : version intrinsics de la version 2
• version 4 : version assembleur utilisant l'AVX

Résultats

Exemple avec GNU 5.4

On compile avec g++ -std=c++11 -Wall -mavx2 -O3 -funroll-loops :

En fonction des compilateurs on peut obtenir des résultats très variables