Contare i modelli che soddisfano una formula booleana

Question

Sto cercando di implementare l'algoritmo #2-Sat dal documento "Contare gli incarichi soddisfacenti in 2-Sat e 3-Sat"(Dahllöf, Jonsson e Wahlström, Teoria. Calcolo. Sci. 332 (1–3): 265–291, 2005). Alcune righe nella descrizione dell'algoritmo Gli autori indicano un sottogoritmo e rivendicano "la funzione $ C_e $ Calcola #2-Sat per ricerca esaustiva. Sarà applicato solo alle formule di dimensioni ≤ 4 e si può quindi presumere in modo sicuro funzionare in O (1) tempo ". La dimensione delle formule è riferita al numero di clausole.

Ho cercato di trovare questo algoritmo di ricerca esaustivo che calcola un'istanza #2-sat con numero di clausole inferiori a 4. ma i risultati restituiscono solo gli algoritmi per la risoluzione di modelli in generale per la risoluzione/il conteggio per #2 o #3 Parla di un caso speciale quando le dimensioni ≤ 4. Prima di tutto, questa affermazione è vera? Da quando il documento è stato pubblicato da una rivista ben nota, immagino che lo sia. Ma se è così, qualcuno sa di questo caso speciale?