Role Mining as Boolean Satisfiability