Patent ID: 11861409
Assignee: AMAZON TECHNOLOGIES, INC.
Field: Computer technology (Electrical engineering)
Classification: CPC G | IPC G

Claim 3:
4. A computer-implemented method comprising:
receiving, by a coordinator process running on a first computing resource, a request to determine whether a formula expressed in propositional logic is satisfiable;
identifying a set of predicates in the formula based on a type of theory associated with the set of predicates, wherein each predicate of the set of predicates is a binary-valued function of at least one theory variable contained in the formula;
partitioning a search space associated with the formula into a plurality of sub-formulas, wherein each sub-formula of the plurality of sub-formulas includes the formula under an assumption that a respective predicate of the set of predicates is either true or false;
sending, to a satisfiability modulo theories (SMT) solver running on each of a respective plurality of computing resources, a respective sub-formula of the plurality of sub-formulas;
receiving, from the SMT solver running on a computing resource of the plurality of computing resources, an indication that the formula is satisfiable;
transmitting a message indicating that the formula is satisfiable, wherein satisfiability of the formula determines a property of a policy defining permissions applicable to a computing resource associated with a cloud provider network; and
controlling access to the computing resource according to the policy defining permissions applicable to the computing resource associated with the cloud provider network.