SAT/SMT Satisfiability Check¶

Automated decision tool — instantiates Incompatible Requirement Set Resolution

Encodes the whole commitment set as logical formulas and lets an automated solver decide, once and for all, whether any joint assignment satisfies them — returning a concrete witness or reporting that none exists.

A pile of individually reasonable requirements can be jointly impossible in a way no eyeballing will catch — the conflict can be global even when every pair looks fine. SAT/SMT Satisfiability Check settles the question mechanically: it translates every commitment into a formula over shared variables, hands the conjunction to a complete decision procedure, and gets back a definite verdict — satisfiable, with an actual assignment that meets all of them at once, or unsatisfiable, meaning the feasible set is empty and no design inside the current model can exist. Its defining move is that the check is global and complete: it reasons over all the constraints together, so it exposes exactly the kind of many-way conflict that pairwise review and intuition miss, and it hands back a checkable artifact rather than an opinion.

Example¶

A build team must pick versions for roughly 40 interdependent libraries. Each library declares the version ranges of the others it works with. The product owner wants library A at ≥3.0 (for a new API), library B pinned at 1.4 (the only audited release), and a logging plugin that — three dependencies down — requires A below 3.0. Every pairwise constraint is satisfiable, and no reviewer spots the problem by reading the manifest. The check encodes each "package X at version v" as boolean/integer variables and each compatibility rule as a clause, then asks an SMT solver whether the conjunction has a model. It comes back unsatisfiable and hands over the offending clause set as a seed. Loosen the plugin's pin and re-run, and the same solver now returns satisfiable with a concrete, installable version assignment — a witness the build system can act on directly. Modern package managers reach for SAT/SMT solvers for exactly this reason: version resolution is a joint-satisfiability problem, not a pairwise one.

How it works¶

Encode each commitment as a formula over shared variables — plain propositional clauses for SAT, or, for SMT, formulas that mix in background theories (linear arithmetic, arrays, bit-vectors, uninterpreted functions) so numeric and structured requirements are modelled faithfully rather than flattened. Conjoin them all and pose one question: does a satisfying assignment exist? A complete procedure (CDCL for SAT; a theory-aware search for SMT) either constructs a model — a feasible point proving the whole set is jointly consistent — or terminates with unsatisfiable, a machine-checkable proof that the feasible set is empty. What distinguishes the tool from its siblings is that this is the raw yes/no decision plus a witness: it does not say which commitments to blame or what to give up, only whether any joint solution is there to be found.

Tuning parameters¶

Logic / theory fragment — propositional SAT versus SMT over arithmetic, arrays, or bit-vectors. Richer theories model the requirements more truthfully but cost solve time, and some theory combinations are undecidable.
Encoding granularity — how finely commitments map to variables and clauses. Finer encodings capture more real conflicts; they also blow up formula size and solve time.
Timeout / "unknown" budget — how long the solver runs before giving up. On hard or undecidable fragments it returns unknown, which is emphatically not consistent.
Witness vs. proof emphasis — ask for a satisfying model, an unsatisfiability proof, or both. The proof is what feeds core extraction and independent proof-checking downstream.
Assumption literals — which commitments to toggle as retractable assumptions, so you can re-query incrementally ("what if B moves?") without re-encoding from scratch.

When it helps, and when it misleads¶

Its strength is turning "we think these clash" into a definite, reproducible verdict backed by an artifact — a real feasible assignment when one exists, a real refutation when it doesn't — and catching the global conflicts that no compatibility grid can surface, because pairwise consistency does not imply joint consistency.^[1]

The verdict is only ever as truthful as the encoding. A satisfiable result can be an artifact of an under-constrained model that quietly omitted a real requirement, and an unsatisfiable one can come from an over-tight translation rather than a genuine conflict; the tool answers the question you actually posed, not the one you meant. On hard fragments it may only return unknown, which must never be filed as consistent. The classic misuse is to encode just the commitments you want to survive so the solver "proves" a decision already made. The discipline that guards against this is to validate the encoding against known-good and known-bad cases, keep every clause traceable to a source commitment, and read satisfiable as "meets the letter," never "meets the intent."

How it implements the components¶

SAT/SMT Satisfiability Check fills the modelling-and-decision core of the archetype — the components a decision procedure can actually produce:

joint_satisfiability_model — the conjoined logical encoding of all commitments over shared variables is this model; the tool builds and owns it.
consistency_criteria — the solver's formal notion of a satisfying assignment operationalizes what "jointly consistent" means for this set.
feasible_set — a returned model is a point in the feasible set; unsatisfiable is the proof that the set is empty. Running the check is how you learn which.

It does not localize the conflict to a smallest offending subset (minimal_unsatisfiable_core, incompatibility_certificate — that's Minimal Unsatisfiable Core Extraction) or choose which commitment should yield (relaxation_option, constraint_priority_rule — that's Weighted MaxSAT or Soft-Constraint Optimization); it only decides whether a joint solution exists.

Instantiates: Incompatible Requirement Set Resolution — supplies the yes/no satisfiability verdict and the witness or refutation the rest of the resolution hangs on.
Sibling mechanisms: Minimal Unsatisfiable Core Extraction · Weighted MaxSAT or Soft-Constraint Optimization · Impossibility-Theorem Instantiation Review · Stakeholder Frontier Review · Constraint-Satisfaction Solver Pass · Proof Checking · Compatibility Matrix · Requirements Traceability Matrix · Constraint Relaxation Experiment · Pareto Frontier Analysis · Scenario Sensitivity Sweep · Scope-Boundary Stress Test · Decision Record with Residue

Notes¶

Satisfiable means "a joint assignment exists," not "the assignment is good" — the model satisfies the encoded letter of the requirements, and unstated intent lives outside it. And a solver that times out on a hard fragment returns unknown, a third answer that must be carried as such and never quietly recorded as consistency.

References¶

[1] SMT — Satisfiability Modulo Theories — extends propositional SAT with decision procedures for background theories (arithmetic, arrays, bit-vectors, …), combined so a single check can reason over both boolean structure and typed data. It is what lets numeric and structured requirements be modelled directly instead of being crudely booleanized. ↩