CM5

Question 1

Que signifie SMT ?

Answer 1

Satisfiability Modulo Theory, il s’agit determiner si des formules contenant des symboles de théories particulières sont satisfiables ou non

Question 2

Quelles théories peuvent être traités avec la SMT ?

Answer 2

Les théories décidables

Question 3

Principe de la SMT pour une formule φ

Answer 3

• Convertir φ en forme CNF
• Remplacer chaque littéral par une variable propositionnelle (*)
• Appeler un solveur SAT pour obtenir un modèle M de φ
• Convertir M en contraintes pour la théorie et le faire vérifier par la procédure de décision de la théorie
• Renvoyer φ est satisfiable si M l’est dans la théorie, sinon ajouter ¬M à Φ et reprendre à l’étape (*)

Question 4

Inconvénient de la méthode de la SMT avec n’importe quel solveur SAT

Answer 4

La recherche de modèle n’est pas guidée par la théorie, donc ce n’est pas aussi efficace que ça pourrait l’être

Question 5

Qu’est-ce que DPLL abstrait ?

Answer 5

Ce sont les règles de DPLL classiques mais où les littéraux sont des littéraux du premier ordre et plus de la logique propositionnelle

Question 6

Qu’est-ce que DPLL abstrait modulo théories (DPLL(T)) ?

Answer 6

Ce sont les règles de DPLL abstrait avec des règles permettant à la théorie d’injecter de nouvelles clauses (tautologies pour la théorie) dans l’ensemble des clauses

Question 7

Règles de DPPL abstrait

Answer 7

• unit prop
• decide
• unsat
• backjump

Question 8

unit prop (DPLL abstrait)

Answer 8

M || S, C ∨ l → M, l || S, C ∨ l si I !∈ M et M |= ¬C

Question 9

decide (DPLL abstrait)

Answer 9

M || S → M, l^d || S si I !∈ M et I ∈ S ou ¬I ∈ S

Question 10

unsat (DPLL abstrait)

Answer 10

M || S, C → unsat si M’ |= ¬C tel que M’ ⊆ M et il n’existe pas I^d ≤ l’ dans M pour tout I’ ∈ M’

Question 11

backjump (DPLL abstrait)

Answer 11

M, I^d, M’ || S, C → M, I’ || S, C si M, I^d, M’ |= ¬C, et il existe
une clause C’ ∨ l’ telle que : l’ !∈ M, et l’ ∈ S ou ¬l’ ∈ S ou l’ ∈ M, l^d, M’ ou
¬l’ ∈ M, l^d, M’, et S, C |= C’ ∨ l’, et M |= ¬C’

Question 12

Règles de DPPL abstrait modulo théories

Answer 12

• unit prop
• decide
• unsat
• backjump
• learn

Question 13

learn (DPLL modulo théorie)

Answer 13

M || S → M || S, S’ si |=_t S’ où T est une théorie

Question 14

Améliorations possibles de DPLL(T)

Answer 14

• Minimiser les clauses apprises
• Détecter les conflits plus tôt
• Faire de la propagation avec la théorie

Question 15

Comment minimiser les clauses apprises pour améliorer DPLL(T) ?

Answer 15

Quand on rencontre un conflit en appliquant la règle learn, plutôt qu’apprendre la négation de tout le modèle, on apprend seulement la négation du conflita

Question 16

Comment détecter les conflits plus tôt pour améliorer DPLL(T) ?

Answer 16

Plutôt qu’attendre d’avoir un modèle compler pour learn, on learn dès qu’on sait qu’on va trouver un conflit

Question 17

Comment faire de la propagation avec la théorie pour améliorer DPLL(T) ?

Answer 17

On ajoute la règle theory prop à DPLL(T) :
M || S → M, I || S si I !∈ M, et I ∈ S ou ¬I ∈ S, et M |=_T ¬I