Verification of(≠,=)Constrained Workflow Robustness Based on Satisfiability Counting

ZHAI Zhi-nian; WANG Gang; ZHENG Zhi-jun; PENG Yan-bing; PAN Zhi-gang; WANG Zhong-peng

doi:10.3969/j.issn.0372-2112.2015.11.024

您当前的位置：

首页 >

文章列表页 >

Verification of(≠,=)Constrained Workflow Robustness Based on Satisfiability Counting

更新时间：2025-07-16

- Verification of(≠,=)Constrained Workflow Robustness Based on Satisfiability Counting
- Acta Electronica Sinica Vol. 43, Issue 11, Pages: 2298-2304(2015)
- 作者机构：
  
  1. 浙江科技学院信息与电子工程学院,浙江,杭州,310023
  2. 中国核电工程有限公司河北分公司民用工程研究设计所,河北,石家庄,050011
- 作者简介：
- 基金信息：
- DOI：10.3969/j.issn.0372-2112.2015.11.024
  CLC： TP309
- Published：2015
- 稿件说明：
移动端阅览
ZHAI Zhi-nian, WANG Gang, ZHENG Zhi-jun, et al. Verification of(≠,=)Constrained Workflow Robustness Based on Satisfiability Counting[J]. Acta Electronica Sinica, 2015, 43(11): 2298-2304.
DOI：

ZHAI Zhi-nian, WANG Gang, ZHENG Zhi-jun, et al. Verification of(≠,=)Constrained Workflow Robustness Based on Satisfiability Counting[J]. Acta Electronica Sinica, 2015, 43(11): 2298-2304. DOI： 10.3969/j.issn.0372-2112.2015.11.024.

摘要

工作流将业务过程分解为有序的步骤并分配人力资源加以执行.资源分配受访问控制约束及资源异常干扰

存在可满足性和鲁棒性问题.而其鲁棒性验证又依赖于其可满足性判定

目前通过求可满足性的一个解来完成.本文提出另一种途径

通过统计解的个数来完成判定.特别地

通过多项式计数归约为有求解器可用的#SAT问题

给出了互斥和绑定约束下的可满足性计数算法.实验表明

相对目前时间复杂度最低的可满足性求解算法

该可满足性计数算法显著提高了实际判定效率和适用规模.

Abstract

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.

关键词

Keywords

references

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Counting Workflow Satisfiability(≠,=) and Its #P Completeness

Joint Optimization of Distributed Intelligent Content Caching and User Association for CF-mMIMO

Robust Resource Allocation Algorithm for Secure Communication in LEO-Based Satellite Communication Systems

Random User Characteristics-Oriented Joint UAV Deployment and Resource Allocation Algorithm

A Learning-Inspired Resource Allocation for Energy Harvesting-Powered Cognitive M2M Communications

Related Author

ZHAI Zhi-nian

LU Ya-hui

YU Fa-hong

ZHOU Wu-jie

XIANG Jian

WU Ming-wei

LI Yun

ZHANG Cheng-yu

Related Institution

School of Information and Electronic Engineering, Zhejiang University of Science and Technology

School of Computer, Shenzhen University

College of Mathematics Physics and Information, Jiaxing University

School of Information and Electronic Engineering Zhejiang University of Science and Technology Hangzhou Zhejiang China

School of Computer Shenzhen University Shenzhen Guangdong China

⁰