♯SAT
In computer science, the Sharp Satisfiability Problem (sometimes called Sharp-SAT, #SAT or model counting) is the problem of counting the number of interpretations that satisfy a given Boolean formula, introduced by Valiant in 1979. In other words, it asks in how many ways the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. For example, the formula a ∨ ¬ b {\displaystyle a\lor \neg b} is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments ( a {\displaystyle a} = TRUE, b {\displaystyle b} = FALSE), ( a {\displaystyle a} = FALSE, b {\displaystyle b} = FALSE), and ( a {\displaystyle a} = TRUE, b {\displaystyle b} = TRUE), we have a ∨ ¬ b = TRUE .