solution

Một công thức ở dạng chuẩn hội (CNF) là hội (AND) của nhiều mệnh đề (clause), mỗi mệnh đề là tuyển (OR) của các literal. Mỗi literal là một biến $x_i$ hoặc phủ định $\lnot x_i$.

Một phép gán giá trị cho $n$ biến thỏa công thức nếu mọi mệnh đề đều đúng (mỗi mệnh đề có ít nhất một literal đúng).

Cho $n$ biến và $m$ mệnh đề, hãy đếm số phép gán $0/1$ cho các biến làm công thức đúng.

Quy ước literal: số nguyên khác $0$; giá trị dương $i$ nghĩa là $x_i$, giá trị âm $-i$ nghĩa là $\lnot x_i$ (biến đánh số $1..n$).

Ví dụ: $n=2$, mệnh đề 1 2 ($x_1 \lor x_2$): có 3 phép gán thỏa trong 4.