Skip to content

Boolean SAT or SMT Path Search

Tool — instantiates Conjunctive Path Assurance

Encodes the whole conduction logic as a Boolean or SMT formula and lets a solver either exhibit a dangerous state combination or prove that none exists.

Enumerating combinations by hand runs out of steam fast, and testing samples them without ever settling the question. Boolean SAT or SMT Path Search takes a different route: it translates the entire conduction logic — every edge's activation condition — into a single logical formula over the system's state variables, adds the assertion "the target is reachable," and hands it to an automated solver. Its defining move is that the answer is decisive: the solver either returns a concrete satisfying assignment — an actual combination of conditions that lights up a complete route — or reports unsatisfiable, a machine-checked proof that no such combination exists within the model. It is the one tool in the set that can say "impossible," not merely "not observed."

Example

A cloud platform wants to be sure no low-trust role can ever reach a delete-production permission. The team encodes the identity model as constraints: each role's direct grants, each group's inherited grants, the wildcard resource tags, the trust policies that let one role assume another. Then it asserts the forbidden reachability and runs an SMT solver. It comes back satisfiable, with a witness: a contractor role inherits through two nested groups, and a wildcard tag lets it assume an admin role that holds the permission — a three-condition conjunction no one had spotted. The team removes the wildcard, adds a blocking clause, and re-runs; now the solver returns unsatisfiable, a proof that the route is closed under the modeled policy. Minimizing the original witness pinpoints the two grants that were actually essential.

How it works

Choose the state variables; write each edge's activation condition as a clause or constraint (Boolean for on/off logic, SMT when arithmetic, timing, or data values matter); conjoin them with the "target reachable" assertion; invoke the solver. A satisfying assignment is a concrete activating conjunction; unsatisfiability is a proof of unreachability over the encoding. Unsat-core extraction shrinks a witness to its minimal activating set, and blocking-and-repeating enumerates further distinct combinations. What distinguishes it from sampling or testing is soundness over the model: unsatisfiable is a proof, not an absence of evidence.

Tuning parameters

  • Encoding fidelity — how faithfully the formula captures real behavior (pure Boolean vs. SMT with arithmetic, bit-vectors, or timing). Higher fidelity catches subtler combinations but costs modeling effort and solver time — and the verdict is only as sound as the encoding.
  • Property asserted — exactly which "target reachable" condition you write down. Too weak and it misses hazards; too strong and the solver floods you with benign models.
  • Minimization — whether to return any satisfying assignment or extract the minimal core. Minimal cores name the essential conjunction; full assignments are cheaper to get.
  • Single witness vs. enumeration — stop at the first dangerous combination or block-and-repeat to list them all. Full enumeration maps the dangerous region but costs far more solver time.

When it helps, and when it misleads

Its strength is unique in this set: within its model it can prove no route exists, and it finds non-obvious combinations across dozens of interacting variables that no human would enumerate. Its failure mode is that soundness is relative to the encoding — an unmodeled variable or behavior is simply invisible, so unsatisfiable means "unreachable in the model," never "unreachable in reality" — and large formulas can exceed solver limits. The classic misuse is trusting a green unsat from a model that quietly omits the risky variable. The discipline is to validate the encoding against known-reachable cases before believing an unsat, and to treat the proof as exactly as strong as the model is faithful.[1]

How it implements the components

  • joint_state_variable_set — the formula's variables are the joint-state variables whose combination the search ranges over.
  • edge_activation_predicate — each edge's conduction condition is encoded directly as a clause or constraint.
  • minimal_activating_conjunction_set — a satisfying assignment, minimized to its unsat core, is a minimal activating conjunction; unsatisfiability proves there is none.

It reasons but never runs: the empirical end_to_end_activation_oracle belongs to Full-Factorial Joint-State Test and Digital-Twin Hazard Rehearsal, and the path_break_or_interlock_requirement that blocks the combination it finds belongs to Independent Interlock or Guard.

References

[1] SAT (Boolean satisfiability) and SMT (satisfiability modulo theories, as in solvers like Z3) decide whether a formula can be made true; an unsatisfiable result is a genuine proof — but only of the encoded formula, which is why the encoding's faithfulness, not the solver, is the thing to check. ↩