## 4 Proposed Method
### Policy Optimization with Separation-of-Duty Constraints
#### 4.2.1 Construction of k-n SOAR Constraints from k-n SOD Constraints  
Given a constructed rule set \(AR\) and a specific SOD constraint \(<\){\(t_{1}\), \(t_{2}\),..., \(t_{n}\)}, \(k\)\(>\) under system status \(\gamma\), we convert the input instance (\(<\){\(t_{1}\), \(t_{2}\),..., \(t_{n}\)}, \(k\)\(>\), \(AR\)) into an intermediate form according to the following steps:  
**Step 1. ** For each access tuple \(t_{i}\) in the constraint, we identify set \(tuple\_rules_{\gamma}(t_{i})\) as a substitute for \(t_{i}\);  
**Step 2. ** Replace rule set \(AR\) with a union of different set of rules associated with each tuple in the constraint. Then, the corresponding intermediate form, which is denoted as \(CIF\), can be represented as \(CIF\) =\(<\){\(S_{1}\), \(S_{2}\),..., \(S_{n}\)}, \(AR\)'\(>\), where \(S_{i}\) = \(tuple\_rules_{\gamma}(t_{i})\), and \(AR^{\prime}=\bigcup\limits_{i=1}^{n}S_{i}\subseteq AR\). According to the conversion, two conclusions can be made:  
1. The process of the conversion does not take value \(k\) of the constraint into consideration because, for each \(k\)'-\(n\) SOAR constraint constructed, \(k\)' takes the value of \(k\) in the following process of constructions. 2. \(AR\)' in \(CIF\) does not contain the rules in (\(AR\backslash AR\)') because the rules not in \(AR\)' are not relevant to the construction of the SOAR constraints. A SAT solver takes the formula in CNF as the input parameter for solving the problem, which can identify the total number of different types of such assignments. For the given intermediate form \(CIF\) = \(<\){\(S_{1}\),\(S_{2}\),..., \(S_{n}\)},\(AR\)'\(>\), we next construct a CNF formula \(F\) corresponding to \(CIF\) through the following steps:  
**Step 1. ** For each rule \(ar_{i}\) in \(AR\)', create the corresponding literal variable \(\overline{ar_{i}}\);  
**Step 2. ** For each \(S_{i}\) and \(AR\)', create the corresponding clause using the disjunction of different literals, which is formalized as \(\overline{ar_{1}}\vee\overline{ar_{2}}\vee\ldots\);  
**Step 3. ** Construct a CNF formula using the conjunction of different clauses, which is represented as \(F=\left( \begin{smallmatrix}n\\ \Lambda\\ i=1\end{smallmatrix} \right)S_{i}clause\)\(\wedge\)\(AR^{\prime}clause\). Thus, a set of several different literals that can satisfy a truth assignment for \(F\) forms the SOAR constraint, and all sets of such literals form different types of SOAR constraints, where the value of \(k\) remains constant. **Example 4**. : _Consider a SOD constraint \(sod\) = \(<\){\(t_{1}\), \(t_{2}\), \(t_{3}\), \(t_{4}\)}, \(2\)\(>\) in the ABAC system status \(\gamma\). The corresponding rules associated with each tuple are given in Table 15._  
First, we convert \(sod\) into the intermediate form \(CIF\) = \(<\){\(\(ar_{4}\)), \(\(ar_{2}\)), \(\{ar_{1}\), \(ar_{3}\)}, \(\{ar_{2}\), \(ar_{3}\), \(ar_{4}\)}}, \(\{ar_{1}\), \(ar_{2}\), \(ar_{3}\), \(ar_{4}\)}\(>\). Next, we construct the Boolean formula \(F\) for \(CIF\) as \(F=\overline{ar_{4}}\wedge\overline{ar_{2}}\wedge(\overline{ar_{1}}\vee \overline{ar_{3}})\wedge(\overline{ar_{2}}\vee\overline{ar_{3}}\vee\overline{ ar_{4}})\wedge(\overline{ar_{1}}\vee\overline{ar_{2}}\vee\overline{ar_{3}}\vee \overline{ar_{4}})\). It is readily verified that {\(\overline{ar_{1}}\), \(\overline{ar_{2}}\), \(\overline{ar_{4}}\)} can satisfy a truth assignment for F, and \(<\){\(ar_{1}\), \(ar_{2}\), \(ar_{4}\)}, \(2\)\(>\) is regarded as a SOAR constraint. Moreover, {\(\overline{ar_{2}}\), \(\overline{ar_{3}}\), \(\overline{ar_{4}}\)}, \(\overline{ar_{2}}\),..., \(\overline{ar_{3}}\), \(\overline{ar_{4}}\)} can also satisfy such assignments, and \(<\){\(ar_{2}\), \(ar_{3}\), \(ar_{4}\)}, \(2\)\(>\), \(<\){\(ar_{1}\), \(ar_{2}\), \(ar_{3}\), \(ar_{4}\)}, \(2\)\(>\) are the other two SOAR constraints corresponding to \(sod\).