Solver
The solver finds satisfying inputs for the active expression, detects tautologies and contradictions, and checks variable impact.
Overview
The Solver section appears in the left panel below the Inputs section. It runs automatically when you change the expression. For simple boolean expressions it uses a fast QM-based backend. For predicate expressions it can use the Z3 SMT solver (loaded lazily via WASM).
The solver status pill in the header shows the current backend:
- Solver: QM — using the fast Quine–McCluskey solver
- Solver: SMT ✓ — Z3 loaded and solving predicates
- Solver: loading… — Z3 WASM is being fetched (~6 MB)
Backends
Logic Studio has two solver backends, selected automatically:
| Backend | When used | Strengths | Weaknesses |
|---|---|---|---|
| logic-solver (SAT) | Pure boolean expressions | Fast, deterministic, no load time | Boolean atoms only; no numeric/set semantics |
| Z3 (SMT) | Predicate expressions, when Z3 is loaded | Full SMT; understands numeric constraints, set membership, subsumption | ~6 MB WASM download; requires SharedArrayBuffer (COOP/COEP headers); first solve is slow |
requestIdleCallback. If you solve a predicate expression before Z3 has loaded, Logic Studio falls back to treating predicates as opaque booleans via the SAT backend.
Outcomes
The solver reports one of these outcomes:
- Satisfiable: at least one input assignment makes the expression true. The solver shows a satisfying assignment.
- Unsatisfiable (UNSAT): no input can make the expression true — it's a contradiction.
- Always true: the expression evaluates to true for every input — it's a tautology.
- Always false: the expression is always false — it's a contradiction.
Constrained solving
When you set variable constraints in the Inputs panel (0, 1, or dc), the solver respects them. Constraining a variable to 1 is equivalent to adding an assumption variable = true to the solving problem.
This lets you ask questions like "given that logged_in = true and banned = false, what else is required for the expression to be true?"
Variable impact
The Solver section shows a variable impact bar chart. Each input variable's impact is the fraction of input assignments where that variable is the deciding factor for the output (flipping it changes the outcome). Variables with high impact are the most important to the expression.
Variables marked as irrelevant (the expression is independent of them) are highlighted in the impact section.
Equivalence diff
The Equiv Diff tab (right column tab 5) lets you compare two expressions for logical equivalence. Paste a second expression into the diff input; Logic Studio checks whether the two are equivalent and, if not, shows a counterexample input assignment that distinguishes them.
