摘要：工作流将业务过程分解为有序的步骤并分配人力资源加以执行.资源分配受访问控制约束及资源异常干扰,存在可满足性和鲁棒性问题.而其鲁棒性验证又依赖于其可满足性判定,目前通过求可满足性的一个解来完成.本文提出另一种途径,通过统计解的个数来完成判定.特别地,通过多项式计数归约为有求解器可用的#SAT问题,给出了互斥和绑定约束下的可满足性计数算法.实验表明,相对目前时间复杂度最低的可满足性求解算法,该可满足性计数算法显著提高了实际判定效率和适用规模.

关键词：工作流 授权 约束 资源分配 可满足性 

单位：浙江科技学院信息与电子工程学院 浙江杭州310023 中国核电工程有限公司河北分公司民用工程研究设计所 河北石家庄050011