Compter les modèles satisfaisant une formule booléenne

Question

J'essaye d'implémenter l'algorithme n ° 2-SAT du papier "Compter les affectations satisfaisantes en 2 et 3 à 3"(Dahllöf, Jonsson et Wahlström, Théorie. Comput. Sci. 332 (1–3): 265–291, 2005). Quelques lignes dans l'algorithme Description Les auteurs indiquent un sous-algorithme et revendique "la fonction $ C_e $ calcule # 2-SAT par une recherche exhaustive. Il ne sera appliqué qu'aux formules de taille ≤ 4 et peut donc être supposée en toute sécurité pour fonctionner en O (1) temps ". La taille des formules est référée au nombre de clauses.

J'ai essayé de trouver cet algorithme de recherche exhaustif qui calcule une instance n ° 2 avec le nombre de clauses inférieures à 4. Mais les résultats ne renvoient que des algorithmes pour résoudre / compter généralement les modèles pour # 2 ou # 3-SAT et ne fait pas Parlez d'un cas spécial lorsque la taille ≤ 4. Tout d'abord, cette affirmation est-elle vraie? Depuis que l'article a été publié par une revue bien connue, je suppose que c'est le cas. Mais si oui, quelqu'un connaît-il ce cas spécial?