3-SAT P34165


Statement
 

pdf   zip

Feu un programa que compti totes les solucions d’un conjunt d’mm clàusules c1,…,cmc_1, \dots, c_m de tres literals en forma normal conjuntiva.

Per exemple, considereu les tres clàusules a∨b∨c,¬a∨b∨c,b∨¬c∨d.a \lor b \lor c, \enspace \neg a \lor b \lor c, \enspace b \lor \neg c \lor d \enspace . (Aquest és el primer exemple de l’entrada.) Hi ha 10 solucions possibles, una de les quals és {a=cert,b=fals,c=cert,d=cert}\{a = \mbox{cert}, b = \mbox{fals}, c = \mbox{cert}, d = \mbox{cert}\}

Entrada

L’entrada consisteix en diversos casos, cadascun amb el nombre de variables nn i el nombre de clàusules mm, seguides de les mm clàusules. Cada clàusula es defineix amb una paraula amb tres lletres diferents d’entre les nn primeres de l’alfabet. Les lletres majúscules indiquen variables tal qual, i les minúscules variables negades.

Podeu suposar 3≤n≤263 \le n \le 26, 1≤m≤1001 \le m \le 100, que les lletres dins de cada clàusula estan ordenades entre si, que no hi ha clàusules repetides, que cada variable apareix en almenys una clàusula, i que sempre hi haurà alguna solució.

Sortida

Per a cada cas, escriviu el nombre de solucions del conjunt de clàusules.

Pista

La solució esperada per a aquest problema és un backtracking conceptualment simple.

Public test cases

  • Input

    4 3 ABC aBC BcD
3 1 aBC
3 3 ABC aBc Abc
4 6 acD aCd bcD ABd Abc BCD

    Output

    10
7
5
6
    • Information
    Author
    Salvador Roura
    Language
    Catalan
    Official solutions
    C++
    User solutions
    C++