J'ai dû rater un truc, car si tu connais SAT, je ne comprends pas ta nécessité d'introduire un concept de branches.
Je veux dire, tu as ton problème représenté sous forme de formule de logique booléenne et tu cherches les modèles (= assignements de valeurs de vérités aux variables booléennes) qui la satisfont. Soit tu te bricoles ton algo qui le fait (tu te modifies un DPLL), soit il existe déjà des algos (implémentés) qui t'énumèrent tous les modèles possibles d'une formule booléenne (cherche AllSAT algorithm sur le net). Après, tu prends tous tes modèles trouvés, tu leur mets un score comme tu l'as décrit pour tes branches, et tu présente à l'utilisateur les modèles du meilleur au plus mauvais. Si tu regardes l'ultraclassique algorithme DPLL, sa règle "split" est une règle de branchement.
# les branches, c'est déjà dans SAT
Posté par geh . En réponse au journal Résolution des dépendances par système de branches. Évalué à 2.
Je veux dire, tu as ton problème représenté sous forme de formule de logique booléenne et tu cherches les modèles (= assignements de valeurs de vérités aux variables booléennes) qui la satisfont. Soit tu te bricoles ton algo qui le fait (tu te modifies un DPLL), soit il existe déjà des algos (implémentés) qui t'énumèrent tous les modèles possibles d'une formule booléenne (cherche AllSAT algorithm sur le net). Après, tu prends tous tes modèles trouvés, tu leur mets un score comme tu l'as décrit pour tes branches, et tu présente à l'utilisateur les modèles du meilleur au plus mauvais. Si tu regardes l'ultraclassique algorithme DPLL, sa règle "split" est une règle de branchement.
(Je n'ai pas lu ton code).