DETAILED ACTION
This Office Action is in response to the claims filed 04 May 2026. Claims 1, 4, and 16 are amended. Claim 6 is cancelled. Claims 2-3, 5, 7-15, and 17-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 .
Continued Examination Under 37 CFR 1.114
A request for continued examination under 37 CFR 1.114, including the fee set forth in 37 CFR 1.17(e), was filed in this application after final rejection. Since this application is eligible for continued examination under 37 CFR 1.114, and the fee set forth in 37 CFR 1.17(e) has been timely paid, the finality of the previous Office action has been withdrawn pursuant to 37 CFR 1.114. Applicant's submission filed on 04 May 2026 has been entered.
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 implemented as automated reasoning service code executed by one or more processors 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 implemented as automated reasoning service code executed by one or more processors of a cloud provider network is discussed next at Prong 2;
“generating, by the automated reasoning service, 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; the use of the automated reasoning service is discussed next at Prong 2;
“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, by the automated reasoning service, 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; the use of the automated reasoning service is discussed next at Prong 2;
“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 implemented as automated reasoning service code executed by one or more processors 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));
“the automated reasoning service” – 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 implemented as automated reasoning service code executed by one or more processors 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 implemented as automated reasoning service code executed by one or more processors of a cloud provider network is discussed next at Prong 2;
“determining, by the automated reasoning service 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; the use of an automated reasoning service is discussed next at Prong 2;
“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, by the automated reasoning service, 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, by the automated reasoning service, 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 implemented as automated reasoning service code executed by one or more processors 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));
“the automated reasoning service” – 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 is implemented as automated reasoning service code that upon execution by one or more processors of the automated reasoning service cause the automated reasoning service to”– these first electronic devices to implement a reasoning service using an automated reasoning service code 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 is implemented as automated reasoning solver code that upon execution by one or more processors of the automated reasoning solver cause the automated reasoning service to” – these second electronic devices to implement a reasoning service using an automated reasoning service code 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
Any inquiry concerning this communication or earlier communications from the examiner should be directed to Sally T. Ley whose telephone number is (571)272-3406. The examiner can normally be reached Monday - Thursday, 10:00am - 6:00pm ET.
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, Viker Lamardo can be reached at (571) 270-5871. 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.
/STL/Examiner, Art Unit 2147
/VIKER A LAMARDO/Supervisory Patent Examiner, Art Unit 2147
Prosecution Insights