In a workflow system

a business process is decomposed into orderly steps

and then human resources are allocated to execute them.The process of resource allocation is constrained by access control and influenced by resource exceptions

so there exist the issues of satisfiability and robustness.Especially

the verification of its robustness relies on the judgment of its satisfiability

which is currently realized via finding one of the satisfiability solutions.This paper proposes another approach

in which the total number of all the solutions is counted to make a satisfiability judgment.Especially

the satisfiability counting under exclusion() and binding(=) constraints is reduced to the problem of #SAT with solvers available by a polynomial-time counting reduction.Experiments show that

compared to the existing lowest-time satisfiability solving algorithm

our satisfiability counting algorithm achieves remarkable improvement in judgment efficiency and applicable scale.