Prosecution Insights
Last updated: April 19, 2026
Application No. 18/066,881

AN EAGER SAT-BASED SOLVER FOR A QUANTIFIER-FREE THEORY OF STRINGS AND BIT VECTORS

Final Rejection §101
Filed
Dec 15, 2022
Examiner
KINSAUL, DANIEL W
Art Unit
2100
Tech Center
2100 — Computer Architecture & Software
Assignee
Amazon Technologies, Inc.
OA Round
2 (Final)
65%
Grant Probability
Favorable
3-4
OA Rounds
4y 2m
To Grant
99%
With Interview

Examiner Intelligence

Grants 65% — above average
65%
Career Allow Rate
144 granted / 221 resolved
+10.2% vs TC avg
Strong +44% interview lift
Without
With
+44.0%
Interview Lift
resolved cases with interview
Typical timeline
4y 2m
Avg Prosecution
7 currently pending
Career history
228
Total Applications
across all art units

Statute-Specific Performance

§101
15.3%
-24.7% vs TC avg
§103
51.5%
+11.5% vs TC avg
§102
14.4%
-25.6% vs TC avg
§112
13.6%
-26.4% vs TC avg
Black line = Tech Center average estimate • Based on career data from 221 resolved cases

Office Action

§101
DETAILED ACTION This Office Action is in response to the remarks on 11/12/2025. Claims 1- 4, 8, 10, 12, 15-20 are amended. Claim 21 is new. Claim 6 is cancelled. Claims 1-5, 7-21 are pending. Notice of Pre-AIA or AIA Status The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA . Response to Arguments Applicant's arguments filed 11/12/2025 have been fully considered. In reference to Applicant’s arguments: - Claim rejections under 35 USC 112(b). Examiner’s response: Rejections are withdrawn in view of amendments and applicant’s arguments. In reference to Applicant’s arguments: - Claim rejections under 35 USC 101. Examiner’s response: Examiner respectfully disagrees. After careful reconsideration, Examiner still understands that the claims are directed to a judicial exception without significantly more. Applicant submits that, under Step 2A, Prong 2 of the subject-matter eligibility analysis, amended claim 1 includes additional elements that cover a concrete technological improvement and integrate the alleged judicial exception into a practical application, in part: “generating... a first-order logic formula... based on a policy managed by an identity and access management service... and a rule, wherein the rule expresses a desired condition of the policy, and wherein the first-order logic formula includes one or more string variables; generating a Boolean abstraction of the first-order logic formula... determining, for each string variable of the one or more string variables, a respective length value indicating a bounded length of possible string assignments to the string variable; bounding the possible string assignments to the string variables according to the respective length values indicating the bounded length; generating a propositional encoding... of the first-order logic formula based on the respective length values indicating the bounded length for each string variable; [and] invoking a satisfiability problem (SAT) solver on the Boolean abstraction of the first-order logic formula and the propositional encoding... of the first-order logic formula to obtain a result value indicating whether the first-order logic formula, with respect to the respective length values indicating the bounded length for each string variable, is satisfiable or unsatisfiable”. Applicant further asserts that these limitations provide an improvement to a technical field and further points to several paragraphs in the specification, however, Examiner would like to explain that all these limitations above are considered under Step 2A Prong 1, not under Prong 2, as all these limitations are directed to judicial exceptions without significantly more. All these limitations, as explained below in the updated rejection, mainly recite mathematical concepts and mental processes, as explained below in the updated rejection. Examiner would like to point to MPEP 2106.05 (a) which states the following: “It is important to note, the judicial exception alone cannot provide the improvement. The improvement can be provided by one or more additional elements”. The only additional elements recited at the claims, which are the ones that can only provide an improvement to the technology, are the use of an automated reasoning service of a cloud provider network, however, it is recited at a high level of generality and therefore amounts to mere instructions to apply a judicial exception on a computer (see MPEP 2106.05(f)); and the display of information indicating whether the policy conforms to the desired conditions, which is merely displaying data of the result, being one of the examples that the courts have described as merely indicating a field of use or technological environment in which to apply a judicial exception (see 2106.05(h) (vi)- displaying the results of collection and analysis of data). Accordingly, these additional elements do not integrate the abstract idea into a practical application because it does not impose any meaningful limits on practicing the abstract idea. The claims are directed to an abstract idea. Rejections are still maintained. In reference to Applicant’s arguments: - Claim rejections under 35 USC 103. Examiner’s response: Rejections are withdrawn in view of arguments and claim amendments. Claim Rejections - 35 USC § 101 35 U.S.C. 101 reads as follows: Whoever invents or discovers any new and useful process, machine, manufacture, or composition of matter, or any new and useful improvement thereof, may obtain a patent therefor, subject to the conditions and requirements of this title. Claims 1-5, 7-21 stand rejected under 35 U.S.C. 101 because the claimed invention is directed to a judicial exception without significantly more. Step 1 analysis: In the instant case, the claims are directed to methods and a system. Thus, each of the claims falls within one of the four statutory categories (i.e., process, machine, manufacture, or composition of matter). Step 2A analysis: Based on the claims being determined to be within of the four categories (Step 1), it must be determined if the claims are directed to a judicial exception (i.e., law of nature, natural phenomenon, and abstract idea), in this case the claims fall within the judicial exception of an abstract idea. Specifically the abstract idea of Mathematical Concepts (including mathematical relationships, formulas, and/or calculations) and Mental Processes-“Concepts performed in the human mind (including an observation, evaluation, judgment, opinion)”. Claim 1: Step 2A: Prong 1 analysis: “generating, by an automated reasoning service of a cloud provider network, a first-order logic formula, wherein the first-order logic formula is generated based on a policy managed by an identity and access management service of the cloud provider network and a rule, wherein the rule expresses a desired condition of the policy, and wherein the first-order logic formula includes one or more string variables” - this limitation amounts to the generation of a formula including string variables, and this amounts to a mathematical concept (including mathematical relationships, formulas, and/or calculations), being abstract ideas. The use of the automated reasoning service of a cloud provider network is discussed next at Prong 2; “generating a Boolean abstraction of the first-order logic formula, wherein the Boolean abstraction of the first-order logic formula includes one or more Boolean variables each representing an atomic formula of the first-order logic formula” - this limitation amounts to the generation of a Boolean abstraction of the formula including Boolean variables, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “determining, for each string variable of the one or more string variables, a respective length value indicating a bounded length of possible string assignments to the string variable” - this limitation amounts to the determination of a respective length for each string variable, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “bounding the possible string assignments to the string variables according to the respective length values indicating the bounded length”- this limitation amounts to the bounding or restriction of the string according to the respective length for each string variable, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “generating a propositional encoding of each atomic formula of the first-order logic formula based on the respective length values indicating the bounded length for each string variable” - this limitation amounts to the encoding of each atomic formulas based on the respective length, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “invoking a satisfiability problem (SAT) solver on the Boolean abstraction of the first-order logic formula and the propositional encoding of each atomic formula of the first-order logic formula to obtain a result value indicating whether the first-order logic formula, with respect to the respective length values indicating the bounded length for each string variable, is satisfiable or unsatisfiable”- this limitation amounts to the calculation of a result value using a SAT solver on the Boolean abstraction of the formula, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “determining, based on the result value, whether the policy conforms to the desired condition of the policy expressed by the rule”- this limitation amounts to the determination of a policy to conform to a condition based on a result value calculated in the previous limitation, and this amounts to mental processes such as observing the value, evaluating it and judging its conformance, being abstract idea. Step 2A: Prong 2 analysis: This judicial exception is not integrated into a practical application because it only recites these additional elements: “an automated reasoning service of a cloud provider network” – this reasoning service is recited at a high level of generality, therefore it amounts to mere instructions to apply a judicial exception on a computer (see MPEP 2106.05(f)); “causing display of information indicating whether the policy conforms to the desired condition of the policy expressed by the rule”- displaying the result of the conformance of the policy amounts to merely displaying data of the result, being one of the examples that the courts have described as merely indicating a field of use or technological environment in which to apply a judicial exception (see 2106.05(h) (vi)- displaying the results of collection and analysis of data). Accordingly, these additional elements do not integrate the abstract idea into a practical application because it does not impose any meaningful limits on practicing the abstract idea. The claims are directed to an abstract idea. Step 2B analysis: The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements explained above amount to mere instructions to apply an exception, and merely indicating a field of use or technological environment in which to apply a judicial exception. The claims are not patent eligible. Claim 2: this claim recites further embellishment about the abstract ideas recited at claim 1, such as the mathematical formulas identifying string variables, determining bound length, further encoding of formulas, and applying SAT solver to the encoded formulas, being mathematical calculations, formulas and relationships (mathematical concept). Claim 3: this claim recites further embellishment about the abstract ideas recited at claim 1, such as the determining an alphabet for the encoded formula, which amounts to determining symbols, variables and constants of the formula, being mathematical calculations, formulas and relationships (mathematical concept). Claim 4: Step 2A: Prong 1 analysis: “obtaining, by a solver used by an automated reasoning service of a cloud provider network, a formula including one or more string variables, wherein the formula relates to a question about a desired condition of a policy managed by an identity and access management service of a cloud provider network” - this limitation amounts to the generation of a formula including string variables, and this amounts to a mathematical concept (including mathematical relationships, formulas, and/or calculations), being abstract ideas. The use of the solver used by an automated reasoning service of a cloud provider network is discussed next at Prong 2; “determining, for at least one string variable of the one or more string variables, a respective length value indicating a bounded length of possible assignments to the string variable” - this limitation amounts to the determination of a respective length for each string variable, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “bounding the possible string assignments to the string variables according to the respective length values indicating the bounded length”- this limitation amounts to the bounding or restriction of the string according to the respective length for each string variable, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “determining an alphabet for a propositional encoding of the formula, wherein the alphabet includes characters occurring in the formula and an extra character”- this limitation amounts to the determination of an alphabet for the encoded formula, which amounts to determining symbols, variables and constants of the formula, being mathematical calculations, formulas and relationships (mathematical concept); “generating the propositional encoding of the formula with respect to the respective length values indicating the bounded length for the at least one string variable and with respect to the alphabet” - this limitation amounts to the encoding of each atomic formulas based on the respective length, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “invoking a satisfiability problem (SAT) solver on the propositional encoding of the formula to obtain a result value indicating whether the formula, with respect to the respective length values indicating the bounded length for the at least one string variable, is satisfiable or unsatisfiable”- this limitation amounts to the calculation of a result value using a SAT solver on the Boolean abstraction of the formula, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas. Step 2A: Prong 2 analysis: This judicial exception is not integrated into a practical application because it only recites these additional elements: “a solver used by an automated reasoning service of a cloud provider network” – this reasoning service is recited at a high level of generality, therefore it amounts to mere instructions to apply a judicial exception on a computer (see MPEP 2106.05(f)); “providing the results value to another component of the automated reasoning service”- providing the results to another component amounts to mere data outputting, being an insignificant extra solution activity per 2106.05(g). Accordingly, these additional elements do not integrate the abstract idea into a practical application because it does not impose any meaningful limits on practicing the abstract idea. The claims are directed to an abstract idea. Step 2B analysis: The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements explained above amount to mere instructions to apply an exception, and insignificant extra-solution activities. The claims are not patent eligible. Moreover, re-evaluation of these additional elements or combination of elements that were considered to be insignificant extra-solution activity are needed to determine if they are considered well-understood, routine and conventional limitations: “providing the result value to another component of the automated reasoning service”- providing the results to another component amounts to transmitting a dataset over a network, further considered well-understood, routine and conventional under MPEP 2106.05(d) II (i). Claim 5: this claim recites further embellishment about the abstract ideas recited at claim 4, such as the mathematical formulas identifying string variables, determining bound length, further encoding of formulas, and applying SAT solver to the encoded formulas, being mathematical calculations, formulas and relationships (mathematical concept). Claim 7: this claim recites further embellishment about the string variables, being mathematical calculations, formulas and relationships (mathematical concept). Claim 8: this claim recites further embellishment about the determination of the respective length value for string variables, being mathematical calculations, formulas and relationships (mathematical concept). Claim 9: this claim recites further embellishment about the SAT solver use in the encoding of the formula, being mathematical calculations, formulas and relationships (mathematical concept). Claim 10: this claim recites further embellishment about the mathematical concepts in the previous claims, and determining satisfaction of the formula, which amounts to observation, evaluation and judgment (mental processes). Claim 11: this claim recites further determinations steps, which amount to observation, evaluation and judgment (mental processes). Claim 12: this claim recites receiving an input indicating a length value, which amounts to mere data gathering, being an insignificant extra solution activity per 2106.05(g) under Step 2A: Prong 2, and to receiving or transmitting data over a network, further considered well-understood, routine and conventional under MPEP 2106.05(d) II (i) under Step 2B. Further, it recites determinations steps, which amount to observation, evaluation and judgment (mental processes). Claim 13: this claim recites receiving further inputs, which amounts to mere data gathering, being an insignificant extra solution activity per 2106.05(g) under Step 2A: Prong 2, and to receiving or transmitting data over a network, further considered well-understood, routine and conventional under MPEP 2106.05(d) II (i) under Step 2B. Claim 14: this claim recites displaying information on conformance, which amounts to merely displaying data of the result, being one of the examples that the courts have described as merely indicating a field of use or technological environment in which to apply a judicial exception (see 2106.05(h) (vi)- displaying the results of collection and analysis of data) under Step 2A: Prong 2 and Step 2B. Claim 15: this claim recites generating a recommendation, which amounts to mental steps such as evaluating and judgment, being abstract ideas. Further, it recites displaying information of the recommendation, which amounts to merely displaying data of the result, being one of the examples that the courts have described as merely indicating a field of use or technological environment in which to apply a judicial exception (see 2106.05(h) (vi)- displaying the results of collection and analysis of data). Claim 16: Step 2A: Prong 1 analysis: The claim(s) recite(s): “generate a first-order logic formula, wherein the first-order logic formula is generated based on a policy managed by an identity and access management service of a cloud provider network and a rule, wherein the rule expresses a desired condition of the policy, and wherein the first-order logic formula includes one or more string variables” - this limitation amounts to the generation of a formula including string variables, and this amounts to a mathematical concept (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “generate a Boolean abstraction of the first-order logic formula, wherein the Boolean abstraction of the first-order logic formula includes one or more Boolean variables each representing an atomic formula of the first-order logic formula” - this limitation amounts to the generation of a Boolean abstraction of the formula including Boolean variables, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “determine, for each string variable of the one or more string variables, a respective length value indicating a bounded length of possible string assignments to the string variable” - this limitation amounts to the determination of a respective length for each string variable, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “bound the possible string assignments to the string variables according to the respective length values indicating the bounded length”- this limitation amounts to the bounding or restriction of the string according to the respective length for each string variable, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “generate a propositional encoding of each atomic formula of the first-order logic formula based on the respective length values indicating the bounded length for each string variable” - this limitation amounts to the encoding of each atomic formulas based on the respective length, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “invoke a satisfiability problem (SAT) solver on the Boolean abstraction of the first-order logic formula and the propositional encoding of each atomic formula in the first-order logic formula to obtain a result value indicating whether the first-order logic formula, with respect to the respective length values indicating the bounded length for each string variable, is satisfiable or unsatisfiable”- this limitation amounts to the calculation of a result value using a SAT solver on the Boolean abstraction of the formula, and this further amounts to mathematical concepts (including mathematical relationships, formulas, and/or calculations), being abstract ideas; “determine, based on the result value, whether the policy conforms to the desired condition of the policy expressed by the rule”- this limitation amounts to the determination of a policy to conform to a condition based on a result value calculated in the previous limitation, and this amounts to mental processes such as observing the value, evaluating it and judging its conformance, being abstract idea. Step 2A: Prong 2 analysis: This judicial exception is not integrated into a practical application because it only recites these additional elements: “a first one or more electronic devices to implement an automated reasoning service in a multi-tenant provider network, wherein the automated reasoning service includes instructions that upon execution cause the automated reasoning service to”– these first electronic devices to implement a reasoning service is recited at a high level of generality, therefore it amounts to mere instructions to apply a judicial exception on a computer (see MPEP 2106.05(f)); “a second one or more electronic devices to implement an automated reasoning solver in the multi-tenant provider network, wherein the automated reasoning solver includes instructions that upon execution cause the automated reasoning service to” – these second electronic devices to implement a reasoning service is recited at a high level of generality, therefore it amounts to mere instructions to apply a judicial exception on a computer (see MPEP 2106.05(f)); “cause display of information indicating whether the policy conforms to the desired condition of the policy expressed by the rule”- displaying the result of the conformance of the policy amounts to merely displaying data of the result, being one of the examples that the courts have described as merely indicating a field of use or technological environment in which to apply a judicial exception (see 2106.05(h) (vi)- displaying the results of collection and analysis of data). Accordingly, these additional elements do not integrate the abstract idea into a practical application because it does not impose any meaningful limits on practicing the abstract idea. The claims are directed to an abstract idea. Step 2B analysis: The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements explained above amount to mere instructions to apply an exception, and merely indicating a field of use or technological environment in which to apply a judicial exception. The claims are not patent eligible. Claim 17: this claim recites further embellishment about the abstract ideas recited at claim 16, such as the mathematical formulas identifying string variables, determining bound length, further encoding of formulas, and applying SAT solver to the encoded formulas, being mathematical calculations, formulas and relationships (mathematical concept). Claim 18: this claim recites further embellishment about the abstract ideas recited at claim 16, such as the determining an alphabet for the encoded formula, which amounts to determining symbols, variables and constants of the formula, being mathematical calculations, formulas and relationships (mathematical concept). Claim 19: this claim recites further embellishment about formulas translation into a non deterministic finite automaton, being mathematical calculations, formulas and relationships (mathematical concept). Claim 20: this claim recites performing in an iterative manner the mathematical calculations, which does not impose a meaningful limit con the claim limitation, considered as insignificant extra solution activity per 2106.05(g) under Step 2A: Prong 2, and to performing repetitive calculations, further considered well-understood, routine and conventional under MPEP 2106.05(d) II (ii) under Step 2B. Claim 21: this claim recites determining various access and permissions on a computing resource, and/or comparing permissiveness of two policies, which are mental steps (observation, evaluation, judgment), being abstract ideas. Viewed as a whole, these additional claim element(s) do not provide meaningful limitation(s) to transform the abstract idea into a patent eligible application of the abstract idea such that the claim(s) amounts to significantly more than the abstract idea itself. Therefore, the claim(s) are rejected under 35 U.S.C. 101 as being directed to non-statutory subject matter. Allowable Subject Matter For claims 1-5, 7-21 no art rejection is made for these claims, they are only rejected under 35 USC 101, as explained above in this office action. Conclusion THIS ACTION IS MADE FINAL. Applicant is reminded of the extension of time policy as set forth in 37 CFR 1.136(a). A shortened statutory period for reply to this final action is set to expire THREE MONTHS from the mailing date of this action. In the event a first reply is filed within TWO MONTHS of the mailing date of this final action and the advisory action is not mailed until after the end of the THREE-MONTH shortened statutory period, then the shortened statutory period will expire on the date the advisory action is mailed, and any nonprovisional extension fee (37 CFR 1.17(a)) pursuant to 37 CFR 1.136(a) will be calculated from the mailing date of the advisory action. In no event, however, will the statutory period for reply expire later than SIX MONTHS from the mailing date of this final action. Any inquiry concerning this communication or earlier communications from the examiner should be directed to LUIS A SITIRICHE whose telephone number is (571)270-1316. The examiner can normally be reached M-F 9am-6pm. Examiner interviews are available via telephone, in-person, and video conferencing using a USPTO supplied web-based collaboration tool. To schedule an interview, applicant is encouraged to use the USPTO Automated Interview Request (AIR) at http://www.uspto.gov/interviewpractice. If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, David Yi can be reached at (571) 270-7519. The fax phone number for the organization where this application or proceeding is assigned is 571-273-8300. Information regarding the status of published or unpublished applications may be obtained from Patent Center. Unpublished application information in Patent Center is available to registered users. To file and manage patent submissions in Patent Center, visit: https://patentcenter.uspto.gov. Visit https://www.uspto.gov/patents/apply/patent-center for more information about Patent Center and https://www.uspto.gov/patents/docx for information about filing in DOCX format. For additional questions, contact the Electronic Business Center (EBC) at 866-217-9197 (toll-free). If you would like assistance from a USPTO Customer Service Representative, call 800-786-9199 (IN USA OR CANADA) or 571-272-1000. /LUIS A SITIRICHE/Primary Examiner, Art Unit 2126
Read full office action

Prosecution Timeline

Dec 15, 2022
Application Filed
Aug 01, 2023
Response after Non-Final Action
Aug 21, 2025
Non-Final Rejection — §101
Oct 28, 2025
Examiner Interview Summary
Oct 28, 2025
Applicant Interview (Telephonic)
Nov 12, 2025
Response Filed
Mar 02, 2026
Final Rejection — §101 (current)

Precedent Cases

Applications granted by this same examiner with similar technology

Patent 9678992
NULL
2y 5m to grant Granted Jun 13, 2017
Patent 9514476
NULL
2y 5m to grant Granted Dec 06, 2016
Patent 9507875
NULL
2y 5m to grant Granted Nov 29, 2016
Patent 9507857
NULL
2y 5m to grant Granted Nov 29, 2016
Patent 9503402
NULL
2y 5m to grant Granted Nov 22, 2016
Study what changed to get past this examiner. Based on 5 most recent grants.

AI Strategy Recommendation

Get an AI-powered prosecution strategy using examiner precedents, rejection analysis, and claim mapping.
Powered by AI — typically takes 5-10 seconds

Prosecution Projections

3-4
Expected OA Rounds
65%
Grant Probability
99%
With Interview (+44.0%)
4y 2m
Median Time to Grant
Moderate
PTA Risk
Based on 221 resolved cases by this examiner. Grant probability derived from career allow rate.

Sign in with your work email

Enter your email to receive a magic link. No password needed.

Personal email addresses (Gmail, Yahoo, etc.) are not accepted.

Free tier: 3 strategy analyses per month