Mortgage eligibility with Z3

Legal and financial rules are constraints. A mortgage application either satisfies all of them or it does not. This tutorial encodes four standard US lending guidelines as Z3 constraints and uses them to answer two questions: is this applicant approved, and if not, what would it take to qualify?

Why Z3 and not just the LLM?#

An LLM can reason about individual rules. But lending decisions involve multiple rules that must all be satisfied simultaneously, and a small model will sometimes pass an applicant who violates one rule while checking another. More importantly, an LLM cannot answer "what is the exact minimum income needed to qualify?" It can approximate, but Z3 can find the precise threshold.

z3.Solver checks whether a set of constraints is satisfiable. If it is, the applicant is approved. If not, re-checking each rule individually names exactly which ones failed. z3.Optimize goes further: given a set of constraints and an objective (minimise annual income), it finds the exact value that makes the constraints satisfiable.

The four rules#

Rule	Constraint
Minimum age	age ≥ 18
Credit score	FICO ≥ 620
Debt-to-income	monthly debt ≤ 43% of monthly income
Loan-to-income	loan amount ≤ 4.5x annual income

The agent#

Two primitives: one that checks all four rules simultaneously, one that finds the minimum income needed to pass.

python

# checker.py
import z3
from opensymbolicai.blueprints import PlanExecute
from opensymbolicai.core import decomposition, primitive


class MortgageChecker(PlanExecute):

    @primitive(read_only=True)
    def check_eligibility(
        self,
        age: int,
        credit_score: int,
        annual_income: float,
        monthly_debt: float,
        loan_amount: float,
    ) -> str:
        """Check all four mortgage rules simultaneously using Z3.

        Returns an approval or a denial listing every failed rule by name.
        Example: check_eligibility(35, 720, 85000, 1500, 280000) -> "Approved ..."
        """
        rules = {
            "minimum age (18+)":      z3.IntVal(age) >= 18,
            "credit score (620+)":    z3.IntVal(credit_score) >= 620,
            "debt-to-income (<=43%)": z3.RealVal(monthly_debt) * 12 <= z3.RealVal(0.43) * z3.RealVal(annual_income),
            "loan-to-income (<=4.5x)": z3.RealVal(loan_amount) <= z3.RealVal(4.5) * z3.RealVal(annual_income),
        }

        solver = z3.Solver()
        solver.add(z3.And(list(rules.values())))

        if solver.check() == z3.sat:
            return "Approved — all eligibility rules satisfied."

        failed = []
        for name, rule in rules.items():
            s = z3.Solver()
            s.add(rule)
            if s.check() != z3.sat:
                failed.append(name)

        return f"Denied — failed: {', '.join(failed)}."

    @primitive(read_only=True)
    def minimum_income(self, monthly_debt: float, loan_amount: float) -> str:
        """Use Z3 Optimize to find the minimum annual income that satisfies the DTI and LTI rules.

        Example: minimum_income(2200, 320000) -> "$71,111.11/year minimum annual income required."
        """
        ai = z3.Real("annual_income")
        opt = z3.Optimize()
        opt.add(ai > 0)
        opt.add(z3.RealVal(monthly_debt) * 12 <= z3.RealVal(0.43) * ai)
        opt.add(z3.RealVal(loan_amount) <= z3.RealVal(4.5) * ai)
        opt.minimize(ai)

        if opt.check() == z3.sat:
            val = opt.model()[ai]
            min_income = float(val.as_decimal(6).rstrip("?"))
            return f"${min_income:,.2f}/year minimum annual income required."
        return "Cannot determine minimum income."

check_eligibility adds all four rules as a conjunction and calls solver.check(). If UNSAT, it re-checks each rule individually to find which ones failed and names them. minimum_income uses z3.Optimize with the same two financial rules and a minimize objective to find the exact income threshold.

Run it#

bash

uv run main.py

Output:

text

[Alex — qualified applicant]
  result: Approved — all eligibility rules satisfied.
  [PASS]

[Jordan — low credit score]
  result: Denied — failed: credit score (620+).
  [PASS]

[Casey — high debt and large loan]
  result: Denied — failed: debt-to-income (<=43%), loan-to-income (<=4.5x).
  [PASS]

[Casey — minimum income to qualify]
  result: $71,111.11/year minimum annual income required.
  [PASS]

The LTI rule is the binding constraint for Casey: $320,000 / 4.5 = $71,111. Z3 finds this exactly.

What to notice#

SAT vs UNSAT gives you a complete answer. A yes/no result is not enough for a denial. The agent re-runs each rule individually after UNSAT to isolate exactly which rules failed. Casey's denial names both the debt-to-income and loan-to-income rules, not just one.

z3.Optimize answers "what would it take?" Tutorial 33 used z3.Solver to find a satisfying assignment. This tutorial introduces z3.Optimize: the same constraint-solving machinery with a minimize objective added. It finds the smallest annual income where both DTI and LTI are satisfied simultaneously, turning a rejection into a concrete target.

The LLM reads the application; Z3 checks the rules. The plan for Alex's case is one line: result = check_eligibility(35, 720, 85000, 1500, 280000). The LLM extracted five numbers from a natural language description and passed them to the primitive. Z3 evaluated all four constraints. Neither step bled into the other.

Rules stay in one place. Adding a fifth rule (minimum employment duration, a maximum loan amount) means adding one entry to the rules dict. The approval and denial logic does not change.