Partial Maximum Boolean Satisfiability （Partial Max-SAT or PMSAT） is an optimization variant of Boolean satisfiability （SAT） problem, in which a variable assignment is required to satisfy all hard clauses and a ma...Partial Maximum Boolean Satisfiability （Partial Max-SAT or PMSAT） is an optimization variant of Boolean satisfiability （SAT） problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many reaHife problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis- Putnam-Logemann-Loveland （DPLL） procedure and Branch and Bound （B^B） algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007~2011 Max-SAT evaluations, emphasizing on the most promising research directions.展开更多
Role-Based Access Control(RBAC)policies are at the core of Cybersecurity as they ease the enforcement of basic security principles,e.g.,Least Privilege and Separation of Duties.As ICT systems and business processes ev...Role-Based Access Control(RBAC)policies are at the core of Cybersecurity as they ease the enforcement of basic security principles,e.g.,Least Privilege and Separation of Duties.As ICT systems and business processes evolve,RBAC policies have to be updated to prevent unauthorised access to resources by capturing errors and misalignments between the current policy and reality.However,such update process is a human-intensive activity and it is expected to meet specific constraints.This paper proposes a semi-automatic RBAC maintenance process to fix and refine an RBAC state when“exceptions”and“violations”are detected.Exceptions are permissions some users realise they miss that are instrumental to their job and should be granted as soon as possible,while violations are permissions that have to be revoked since they are no longer required by their current owners.We propose a formalisation for the maintenance process which fixes single and multiple exceptions and violations by balancing two conflicting objectives,i.e.,(i)optimising the current RBAC state,and(ii)reducing the transition cost.Our approach is based on a Max-SAT formalisation of the constraint-based optimisation problem,and on PDDL planning to define the transition strategy with minimum cost.Our implementation relies on incomplete Max-SAT solvers and satisficing PDDL planners which provide approximations of optimal solutions.Experiments along with a comparative evaluation show good performance on real-world benchmarks.展开更多
Role-Based Access Control(RBAC)policies are at the core of Cybersecurity as they ease the enforcement of basic security principles,e.g.,Least Privilege and Separation of Duties.As ICT systems and business processes ev...Role-Based Access Control(RBAC)policies are at the core of Cybersecurity as they ease the enforcement of basic security principles,e.g.,Least Privilege and Separation of Duties.As ICT systems and business processes evolve,RBAC policies have to be updated to prevent unauthorised access to resources by capturing errors and misalignments between the current policy and reality.However,such update process is a human-intensive activity and it is expected to meet specific constraints.This paper proposes a semi-automatic RBAC maintenance process to fix and refine an RBAC state when“exceptions”and“violations”are detected.Exceptions are permissions some users realise they miss that are instrumental to their job and should be granted as soon as possible,while violations are permissions that have to be revoked since they are no longer required by their current owners.We propose a formalisation for the maintenance process which fixes single and multiple exceptions and violations by balancing two conflicting objectives,i.e.,(i)optimising the current RBAC state,and(ii)reducing the transition cost.Our approach is based on a Max-SAT formalisation of the constraint-based optimisation problem,and on PDDL planning to define the transition strategy with minimum cost.Our implementation relies on incomplete Max-SAT solvers and satisficing PDDL planners which provide approximations of optimal solutions.Experiments along with a comparative evaluation show good performance on real-world benchmarks.展开更多
Maximum satisfiability (MAX SAT) problem is an optimization version of the satisfiability (SAT) problem. This problem arises in certain applications in expert systems and knowledge base revision. MAX SAT problem is NP...Maximum satisfiability (MAX SAT) problem is an optimization version of the satisfiability (SAT) problem. This problem arises in certain applications in expert systems and knowledge base revision. MAX SAT problem is NP-hard Some algorithms can solve this problem, but they are not adapted to the special cases where the number of variables is larger than the number of clauses. Usually, the number of variables has great impact on the efficiency of these algorithms. Thus, a polynomial-time algorithm is proposed to reduce the number of variables. Let T be any instance of the MAX SAT problem. The algorithm transforms T into another instance P of which the number of variables is smaller than the number of clauses of T. Using other algorithms, the optimal solution to P can be found, and it can be used to construct the optimal solution of T. Therefore, this algorithm is an efficient preprocessing step.展开更多
基金supported by the Research Center of College of Computer and Information Sciences at King Saud University, Saudi Arabia
文摘Partial Maximum Boolean Satisfiability （Partial Max-SAT or PMSAT） is an optimization variant of Boolean satisfiability （SAT） problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many reaHife problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis- Putnam-Logemann-Loveland （DPLL） procedure and Branch and Bound （B^B） algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007~2011 Max-SAT evaluations, emphasizing on the most promising research directions.
文摘Role-Based Access Control(RBAC)policies are at the core of Cybersecurity as they ease the enforcement of basic security principles,e.g.,Least Privilege and Separation of Duties.As ICT systems and business processes evolve,RBAC policies have to be updated to prevent unauthorised access to resources by capturing errors and misalignments between the current policy and reality.However,such update process is a human-intensive activity and it is expected to meet specific constraints.This paper proposes a semi-automatic RBAC maintenance process to fix and refine an RBAC state when“exceptions”and“violations”are detected.Exceptions are permissions some users realise they miss that are instrumental to their job and should be granted as soon as possible,while violations are permissions that have to be revoked since they are no longer required by their current owners.We propose a formalisation for the maintenance process which fixes single and multiple exceptions and violations by balancing two conflicting objectives,i.e.,(i)optimising the current RBAC state,and(ii)reducing the transition cost.Our approach is based on a Max-SAT formalisation of the constraint-based optimisation problem,and on PDDL planning to define the transition strategy with minimum cost.Our implementation relies on incomplete Max-SAT solvers and satisficing PDDL planners which provide approximations of optimal solutions.Experiments along with a comparative evaluation show good performance on real-world benchmarks.
文摘Role-Based Access Control(RBAC)policies are at the core of Cybersecurity as they ease the enforcement of basic security principles,e.g.,Least Privilege and Separation of Duties.As ICT systems and business processes evolve,RBAC policies have to be updated to prevent unauthorised access to resources by capturing errors and misalignments between the current policy and reality.However,such update process is a human-intensive activity and it is expected to meet specific constraints.This paper proposes a semi-automatic RBAC maintenance process to fix and refine an RBAC state when“exceptions”and“violations”are detected.Exceptions are permissions some users realise they miss that are instrumental to their job and should be granted as soon as possible,while violations are permissions that have to be revoked since they are no longer required by their current owners.We propose a formalisation for the maintenance process which fixes single and multiple exceptions and violations by balancing two conflicting objectives,i.e.,(i)optimising the current RBAC state,and(ii)reducing the transition cost.Our approach is based on a Max-SAT formalisation of the constraint-based optimisation problem,and on PDDL planning to define the transition strategy with minimum cost.Our implementation relies on incomplete Max-SAT solvers and satisficing PDDL planners which provide approximations of optimal solutions.Experiments along with a comparative evaluation show good performance on real-world benchmarks.
基金Porject supported by the National Natural Science Foundation of China and by the National "863" Hi-Tech Program.
文摘Maximum satisfiability (MAX SAT) problem is an optimization version of the satisfiability (SAT) problem. This problem arises in certain applications in expert systems and knowledge base revision. MAX SAT problem is NP-hard Some algorithms can solve this problem, but they are not adapted to the special cases where the number of variables is larger than the number of clauses. Usually, the number of variables has great impact on the efficiency of these algorithms. Thus, a polynomial-time algorithm is proposed to reduce the number of variables. Let T be any instance of the MAX SAT problem. The algorithm transforms T into another instance P of which the number of variables is smaller than the number of clauses of T. Using other algorithms, the optimal solution to P can be found, and it can be used to construct the optimal solution of T. Therefore, this algorithm is an efficient preprocessing step.
