Counting Satisfying Assignments for 1-DNF-SAT

Boolean satisfiability (SAT) is a classical hard problem in computer science. In this problem, you are given a Boolean formula in 1-DNF form and you need to count the number of ways to assign truth values to its variables such that the formula evaluates to true. A 1-DNF formula is defined as a disjunction (logical OR) of one or more clauses, where each clause consists of exactly one literal. A literal is either a variable or its negation.

The grammar for the formula is given as follows:

$$ \langle formula \rangle ::= \langle clause \rangle \;|\; \langle formula \rangle \lor \langle clause \rangle $$
$$ \langle clause \rangle ::= \langle literal \rangle $$
$$ \langle literal \rangle ::= \langle variable \rangle \;|\; \lnot \langle variable \rangle $$
$$ \langle variable \rangle ::= A\ldots Z \;|\; a\ldots z $$

Note that if any variable appears both as a positive literal and as a negated literal, the formula becomes a tautology (always true). In that case, every assignment of truth values to the variables will satisfy the formula.

Your task is to count the number of satisfying assignments over all distinct variables that occur in the formula.

inputFormat

The input consists of a single line containing a 1-DNF Boolean formula. The literals are separated by the '∨' character. A literal is either a variable (e.g. x) or its negation (denoted by ¬ immediately preceding the variable, e.g. ¬x).

Examples:

• x∨¬y∨z
• ¬x
• A∨B

outputFormat

Output a single integer representing the number of assignments that make the formula evaluate to true.

sample

x

1