公开(公告)号：US20240202545A1

公开(公告)日：2024-06-20

申请号：US18066881

申请日：2022-12-15

Applicant: Amazon Technologies, Inc.

Inventor： Kevin LOTZ ,  Bruno DUTERTRE ,  John Byron COOK ,  Amit GOEL ,  Robert JONES ,  Benjamin KIESL-REITER ,  Soon Ho KONG ,  Rupak MAJUMDAR

IPC: G06N5/01 ,  G06N5/04

CPC classification number: G06N5/013 ,  G06N5/04

Abstract: Techniques are described for providing a SAT-based solver for a quantifier-free theory of strings and bit vectors. The solver can be used by an automated reasoning service of a cloud provider network to analyze policies and the consequences of policies. The solver reduces an input formula to a Boolean satisfiability problem by encoding the input formula into an equisatisfiable propositional formula, where the satisfiability of the equisatisfiable propositional formula is determined by a SAT solver. Rather than using a traditional DPLL(T) style algorithm, the solver described herein bounds the length of variables in an input formula and reduces the problem to a single formula, which can then be solved using incremental SAT solving. The solver can be used independently or as part of a portfolio of solvers used to determine the satisfiability or unsatisfiability of certain formula corresponding, e.g., to questions about users' policies within a cloud provider network.