Understanding SAT / UNSAT

Understanding SAT / UNSAT

When you check an agent action against a policy, ICME returns one of several possible results. The most common are SAT and UNSAT. This page explains what each result means, what causes each one, and how to interpret the less common results you may encounter.

---

The basics

ICME uses an SMT (Satisfiability Modulo Theories) solver to evaluate agent actions against your compiled policy. The solver's job is to determine whether a given action is satisfiable — consistent with your policy constraints — or unsatisfiable — in violation of them.

SAT (Satisfiable) means the action is permitted. The solver found that the action is consistent with all constraints in your policy. Your agent can proceed.

UNSAT (Unsatisfiable) means the action is blocked. The solver proved that the action violates at least one constraint in your policy. No combination of circumstances makes the action permissible under your rules.

These are not confidence scores. They are not probabilities. SAT and UNSAT are mathematical conclusions. The same action evaluated against the same policy will always produce the same result.

---

The full result set

Beyond SAT and UNSAT, you may encounter three additional results in certain circumstances.

SATISFIABLE (conditional) The action is consistent with your policy, but only under certain conditions that weren't fully specified in the action description. The solver found at least one scenario where the action would be permitted and at least one where it would be blocked.

This usually means your policy has a gap, a rule that depends on a variable the action didn't provide, or the action description was ambiguous. See troubleshooting SATISFIABLE results below.

IMPOSSIBLE The action contains premises that directly contradict your policy rules, making it logically impossible to evaluate. This often indicates a conflict within the policy itself rather than a problem with the action.

Example: your policy contains both "all transfers to external wallets are permitted" and "transfers to unverified wallets are blocked" — an action involving an external wallet that is neither explicitly verified nor unverified will return IMPOSSIBLE.

NO TRANSLATION The action description could not be formalized into the logical vocabulary of your policy. This typically means the action describes something your policy has no rules about, or the action was written in a way the formalizer couldn't parse reliably.

---

What causes UNSAT

An action returns UNSAT when the solver proves it violates at least one constraint. The response body includes a reason field that identifies which rule was violated and why.

Threshold violations

json

{
  "result": "UNSAT",
  "blocked": true,
  "reason": "Action violates policy rule 1: transfer amount 5000 exceeds permitted maximum of 1000 USDC",
  "violated_rule": 1,
  "proof": "zk-proof-receipt-..."
}

Recipient not on approved list

json

{
  "result": "UNSAT",
  "blocked": true,
  "reason": "Action violates policy rule 2: recipient wallet 0xDEF456 is not present in the verified whitelist",
  "violated_rule": 2,
  "proof": "zk-proof-receipt-..."
}

Rate limit exceeded

json

{
  "result": "UNSAT",
  "blocked": true,
  "reason": "Action violates policy rule 3: 6 transfers detected within the last 60 seconds, exceeding the permitted maximum of 5",
  "violated_rule": 3,
  "proof": "zk-proof-receipt-..."
}

Multiple violations When an action violates more than one rule, the response identifies the first violated constraint. Fix that constraint and re-check — there may be additional violations.

---

What causes SAT

An action returns SAT when the solver confirms it satisfies all constraints in your policy. The response includes the proof receipt regardless of whether the result is SAT or UNSAT.

json

{
  "result": "SAT",
  "blocked": false,
  "reason": "Action satisfies all policy constraints",
  "proof": "zk-proof-receipt-..."
}
```

A `SAT` result means the action is permitted under your current policy. It does not mean the action is universally safe — it means it passed the rules you wrote. If a permitted action causes a problem, the solution is to update your policy, not to distrust the solver.

---

### Troubleshooting SATISFIABLE results

A `SATISFIABLE` result (distinct from `SAT`) means the solver could not determine a definitive outcome because the action description didn't provide enough information to evaluate all relevant constraints.

**Common causes:**

**Missing context in the action description**

Your policy rule requires information the action didn't provide.

Policy rule: *"Transfers over $5,000 to new vendors require a second authorization."*

Action submitted: *"Transfer $6,000 to Acme Corp."*

The solver knows the amount exceeds $5,000 but cannot determine whether Acme Corp is a new vendor — that information wasn't in the action. Result: `SATISFIABLE`.

Fix: make your action descriptions explicit.
```
Transfer $6,000 to Acme Corp. Acme Corp has been an approved vendor for 3 years.
```

**Ambiguous policy rules**

Your policy uses a term that wasn't defined precisely enough during compilation.

Policy rule: *"Large transfers require approval."*

"Large" wasn't defined, so the compiler made an assumption about what it means. Actions near that boundary may return `SATISFIABLE`.

Fix: rewrite the rule with an explicit threshold and recompile.
```
Transfers over $10,000 require approval.
```

**Overlapping rules with different outcomes**

Two rules apply to the same action but point in different directions, and the action doesn't provide enough context to determine which takes precedence.

Fix: review your policy for rules that might conflict and add explicit precedence or conditions.

---

### Troubleshooting IMPOSSIBLE results

`IMPOSSIBLE` almost always indicates a problem with your policy rather than your action. The solver found that your policy's own rules contradict each other, making it mathematically impossible to evaluate the action.

Run a simple diagnostic: submit the action that returned `IMPOSSIBLE` with a minimal, unambiguous description. If it still returns `IMPOSSIBLE`, recompile your policy and check the consistency report — conflicting rules will be flagged during compilation.

Common patterns that cause `IMPOSSIBLE`:
```
# These two rules conflict for any external wallet
1. All transfers to external wallets are permitted.
2. Transfers to unverified wallets are not permitted.

# Fix: make the rules mutually exclusive
1. Transfers to verified external wallets are permitted.
2. Transfers to unverified wallets are not permitted.
```
```
# These conflict for emergency transfers
1. No transfers over $10,000 are permitted.
2. Emergency fund transfers are always permitted regardless of amount.

# Fix: add explicit conditions
1. Transfers over $10,000 are not permitted, except to the designated emergency fund wallet (0xABC...).

---

Troubleshooting NO TRANSLATION results

NO TRANSLATION means the formalizer couldn't extract evaluable claims from the action description. This is usually one of three things:

The action is out of scope for your policy Your policy covers financial transactions, but the action describes a database query. The formalizer has no variables to map it to. Either expand your policy to cover the new action type or return NO TRANSLATION as a signal to your agent that this action type requires a different evaluation path.

The action description is too vague "Do the usual thing with the funds." — there is nothing for the formalizer to work with.

Fix: require your agent to produce structured, explicit action descriptions before submitting them for evaluation.

The action description is too complex A very long, multi-part action with many nested conditions may exceed the formalizer's reliable operating range. Break it into individual atomic actions and check each one separately.

---

Using results in your agent logic

A minimal integration pattern:

python

def check_action(policy_id, action_description, api_key):
    response = requests.post(
        "https://api.icme.io/v1/checkIt",
        headers={"X-API-Key": api_key},
        json={
            "policy_id": policy_id,
            "action": action_description
        }
    )
    result = response.json()

    if result["result"] == "SAT":
        # Proceed with action
        return True, result["proof"]

    elif result["result"] == "UNSAT":
        # Block action, log reason and proof
        log_blocked_action(action_description, result["reason"], result["proof"])
        return False, result["proof"]

    elif result["result"] == "SATISFIABLE":
        # Insufficient context — request more information
        # or default to blocking and flagging for review
        return False, None

    elif result["result"] == "IMPOSSIBLE":
        # Policy conflict — alert, do not proceed
        alert_policy_conflict(result)
        return False, None

    elif result["result"] == "NO_TRANSLATION":
        # Action out of scope — route to fallback handler
        return handle_out_of_scope_action(action_description)

The proof field should always be stored alongside the action and result — it is your cryptographic receipt that the correct policy was applied to the correct action and produced the correct result.

---

A note on determinism

Unlike LLM-based guardrails, ICME's results are fully deterministic. Given the same policy and the same action, the solver will always return the same result. This has two practical implications:

You can write unit tests for your guardrails. Build a test suite of actions you expect to be permitted and actions you expect to be blocked. Run it every time you update your policy. If a previously-passing test fails after a policy update, you have an immediate signal that the policy change had unintended consequences.

Caching is safe. If your agent submits the same action repeatedly, the result will not change unless the policy changes. You can cache results for identical action descriptions against the same policy_id to reduce latency and cost.