Efficient algorithm for simple constraint satisfaction problem There are 


$k$ Boolean variables $x_1, x_2, \dots, x_k$.
$m$ arbitrary subsets of these variables such that sum of each set equals to $1$ (i.e., only one variable is $1$, the others are $0$). E.g., one of $m$ constraints may be $x_1 + x_3 + x_5 + x_6 = 1$.
$n$ arbitrary subsets of these variables such that sum of each set is at least $1$ (i.e., at least one of the variables should be $1$). E.g., one of $n$ constraints may be $x_1 + x_6 + x_8 \geq 1$.


The solutions are not necessary, but I want to know how many solutions exist.

What is an efficient way to calculate the number of solutions?
There is unlikely to be any efficient algorithm.

Your first class of constraints are monotone exactly-1 CNF clauses.  Your second class of constraints are monotone CNF clauses.  The monotone part indicates that negated literals aren't allowed (you can't have $x_1 - x_3 = 1$ or $x_1 - x_4 \ge 1$).

Thus, in the special case where you have only type-2 constraints, the problem becomes #monotone-SAT.  Unfortunately, this problem is known to be hard.  #SAT is #P-complete, and monotone #SAT is #P-complete as well: it is #P-complete even for monotone 2CNF clauses (i.e., type-2 constraints with only two variables).   It is also known that it is NP-hard to approximate the number of solutions.  As a result, there is unlikely to be any  efficient solution unless the number of variables and constraints is fairly small.  Of course, your problem (with a mixture of type-1 and type-2 constraints) is potentially even harder.

So what can you do, to make the best of the situation?

One approach is to code this as an instance of #SAT, and try applying some off-the-shelf #SAT solver.  You can encode type-1 constraints in SAT using the methods described at Encoding 1-out-of-n constraint for SAT solvers.

Or, you could express the constraints as a BDD and then apply model-counting methods for BDDs.  I expect this to perform worse than a #SAT solver, but you could try it.

Another approach is to use an approximation algorithm.  There are existing algorithms for approximate-#SAT, though they too will hit a limit if you have too many variables and/or clauses.