Incompatible Requirement Set Resolution¶

When individually defensible commitments cannot all hold together, prove and localize the incompatibility, choose the smallest legitimate relaxation, and publish the guarantees and losses that remain.

Summary¶

Incompatible Requirement Set Resolution applies when a collection of axioms, requirements, guarantees, or prohibitions is not merely difficult to satisfy but has no joint realization under the same assumptions and scope. The pattern prevents two common failures: endless search for a nonexistent design and silent local weakening of whichever requirement becomes inconvenient.

The intervention has two sharply separated halves. The analytical half establishes what is impossible: define the commitment set, stabilize semantics and scope, model the conjunction, prove or otherwise certify infeasibility, and isolate one or more minimal unsatisfiable cores. The decision half establishes what will change: protect non-negotiable invariants, enumerate explicit relaxation operators, choose through a legitimate priority rule, propagate the change, and publish the residual guarantee. The proof constrains the choices; it does not make the value judgment for the decision maker.

The structural problem¶

Individually plausible commitments can be jointly impossible. A policy can promise a fixed total budget, universal eligibility, and an unchanged benefit when the arithmetic cannot support all three. A distributed protocol can demand agreement, validity, and unconditional termination under assumptions that rule the conjunction out. A design can require mass, stiffness, cost, geometry, and certified materials that admit no candidate. Every commitment may have a reasonable owner, and every pair may appear compatible, yet the entire set can still have an empty feasible region.

Without a shared resolution pattern, organizations usually respond in one of four ways. They keep searching and blame execution; they relax different requirements in different local contexts; they cite an impossibility slogan without checking its assumptions; or they convert protected commitments into soft weights without authorization. All four create a gap between the promise on paper and the behavior in operation.

Intervention logic¶

Bound the claim. Name the decision space, actors, states, time horizon, environment, resources, and conditions over which simultaneous satisfaction is being claimed.
Inventory the commitments. Give every axiom, requirement, guarantee, prohibition, and derived dependency a stable identifier, source, owner, wording, and status.
Normalize semantics. Align definitions, units, quantifiers, temporal conditions, and applicability scope. Keep assumptions separate from desired commitments.
Classify strength. Mark hard, protected, defeasible, aspirational, and soft items before optimization begins.
Construct one joint model. Make the conjunction testable in a logical, algebraic, temporal, combinatorial, probabilistic, or domain-specific representation.
Test satisfiability honestly. Produce a satisfying witness when one exists. When none is found, distinguish a sound unsatisfiability result from solver timeout or limited search.
Localize the conflict. Extract one or more minimal unsatisfiable cores and verify the certificate independently.
Enumerate resolution operators. Consider removal, weakening, scoping, conditionalization, sequencing, substitution, assumption change, resource expansion, decision-rule change, and architecture redesign.
Protect invariants and reject exported harm. Remove options that violate non-negotiable floors or simply move the conflict beyond the modeled boundary.
Choose legitimately. Compare the remaining satisfiable options using an explicit authority, priority, distributional, reversibility, and harm rule.
Propagate the change. Update tests, proofs, policies, interfaces, contracts, documentation, monitoring, and downstream dependencies.
Publish the residual guarantee. State exactly what remains guaranteed, under which assumptions, what was sacrificed, and how out-of-scope cases behave.
Recheck on drift. Rerun the analysis when requirements, law, demand, resources, evidence, technology, or assumptions change.

Key components¶

Component	Description
Commitment Set ↗	The commitment set is the complete input to the claim of simultaneous satisfaction. It includes more than a list of requirements: it records sources, owners, strength, scope, dependencies, and whether an item is an axiom, desired guarantee, prohibition, environmental assumption, or derived consequence. Mixing these types can create a false conflict, so the distinctions are part of the component.
Commitment Semantics and Scope ↗	A contradiction is meaningful only after terms and quantifiers are stable. “Always available,” “all users,” “no data retained,” and “within budget” are not testable until time windows, populations, failure modes, and accounting boundaries are named. Scope repair should happen before the system claims an impossibility; otherwise a wording defect can be mistaken for a structural theorem.
Constraint Strength Classification ↗	The classification says which commitments are hard, protected, defeasible, aspirational, or soft. It protects the process against an optimizer that solves infeasibility by quietly violating safety, rights, law, or correctness. It also prevents the opposite failure of labeling everything hard, which leaves no authorized resolution path even after incompatibility is proved.
Joint Satisfiability Model and Feasible Set ↗	The model puts every active commitment into one decision frame. Its feasible set is the set of realizations satisfying them all. A nonempty set refutes the incompatibility claim by example. An empty set requires stronger evidence than failure to find a point: a proof, certificate, exhaustive finite analysis, or other sound argument appropriate to the domain.
Minimal Unsatisfiable Core ↗	A minimal unsatisfiable core is an inclusion-minimal subset that remains impossible. It focuses review on the commitments that must change and protects unrelated requirements from broad cuts. Minimal does not mean minimum-size, causally unique, or morally decisive. Several distinct cores can exist, and a proposed relaxation must be checked against the whole model rather than only the first returned core.
Incompatibility Certificate ↗	The certificate makes the impossibility independently checkable. It can be a formal derivation, proof-producing solver trace, lower-bound argument, dual certificate, exhaustive search record, or verified theorem instantiation. It must travel with the assumptions, quantifiers, decision domain, and model version on which it depends.
Protected Invariant ↗	Protected invariants state what the process may not sacrifice by ordinary weighting. Examples include safety floors, rights, conservation laws, semantic integrity, or a statutory limit. If all members of a core are protected, the correct result is escalation, redesign, or a declared unresolved frame—not an undocumented exception.
Relaxation Option and Constraint Priority Rule ↗	A relaxation option is an explicit transformation of the commitment set. It names what changes, how feasibility is restored, who bears the loss, and what new risks appear. The priority rule chooses among options using legitimate criteria such as lexical priority, rights, reversibility, distributional burden, expected harm, or authorized policy. Solver weights can support this choice but cannot replace its governance.
Residual Guarantee Ledger ↗	The residual guarantee ledger is the authoritative post-resolution contract. It states which commitments survive, which are conditional, what assumptions now bound them, and what is no longer promised. This record prevents marketing, policy, requirements, or interface documentation from continuing to claim the impossible original conjunction.
Tradeoff Rationale, Impact Trace, and Recheck Trigger ↗	The rationale explains why one satisfiable relaxation was selected. The impact trace propagates the change to dependent systems and affected people. The recheck trigger recognizes that impossibility is scoped: a new material, budget, law, fault model, demand level, or algorithm can invalidate the old result or create a new conflict.

Common mechanisms¶

Constraint solvers, SAT/SMT checks, and model checkers search for satisfying realizations and can sometimes produce proof artifacts for unsatisfiability. Minimal unsatisfiable core extraction narrows the conflict. Proof checking provides independent assurance. Requirements traceability matrices connect commitments to sources and downstream changes. Compatibility matrices are useful screens but cannot prove global consistency.

After incompatibility is established, constraint relaxation experiments, Weighted MaxSAT or soft-constraint optimization, Pareto frontier analysis, and scenario sensitivity sweeps compare repaired sets. Stakeholder frontier reviews and decision records with residue make authority, burden, dissent, and uncertainty visible. Scope-boundary stress tests verify that conditional guarantees are genuine and operational rather than rhetorical footnotes.

These are mechanisms, not the archetype. A SAT solver alone does not decide which right, promise, or safety property should yield; a workshop alone does not prove that a trade-off is necessary.

Parameter dimensions¶

Important dimensions include:

Set size and core structure: number of commitments, number and overlap of minimal cores, and whether conflict is pairwise or higher-order.
Commitment strength: hard, protected, defeasible, aspirational, or soft.
Model class: Boolean, arithmetic, temporal, combinatorial, stochastic, hybrid, empirical, or normative.
Evidence strength: satisfying witness, heuristic failure, proof certificate, exhaustive argument, theorem instantiation, or expert judgment.
Resolution operator: removal, weakening, scoping, conditionalization, sequencing, substitution, assumption change, resource expansion, or redesign.
Authority and legitimacy: who may authorize sacrifice, who has standing, and which appeal or review paths apply.
Distributional burden: which actors, regions, cases, or lifecycle stages bear the loss.
Reversibility: cost of restoring a commitment if assumptions change.
Scope observability: whether the system can detect when a conditional guarantee applies.
Residual assurance: how the repaired set is tested, monitored, and versioned.

Invariants and outcomes¶

The analysis must preserve the scope and assumptions of the incompatibility result, keep protected commitments explicit, prevent hidden relaxations, and ensure the final guarantee is no broader than operational behavior. A successful implementation stops futile search, localizes the conflict, protects unrelated requirements, creates an accountable trade-off, aligns documentation with behavior, and leaves a versioned path for future reconsideration.

Recognized variants¶

Trilemma Resolution¶

Trilemma Resolution is the exactly-three-property form. Its compact structure supports a complete catalogue of drop, weaken, scope, or dissolve paths. The familiar “pick any two” language is valid only when the three-property incompatibility is actually established and no hidden fourth commitment changes the option set. This variant is the intended destination for the later queue target trilemma.

Impossibility-Bounded Guarantee Scoping¶

This variant changes a universal guarantee into a truthful conditional guarantee. It is appropriate when a theorem or boundary rules out performance for all inputs, fault patterns, timing models, or distributions, but a useful guarantee is available inside an observable region. The system must detect when it is out of scope and defer, degrade, or switch modes safely.

Normative Commitment Incompatibility Resolution¶

When the commitments encode duties, rights, policy promises, or public burdens, legitimacy is part of the intervention. Formal analysis can show that at least one commitment must change; it cannot decide who should bear the loss. Standing, authority, due process, remedy, compensation, and dissent therefore become first-class components.

Tradeoffs¶

The pattern trades accessibility against formal precision, decisive action against reversibility, broad guarantees against truthful scope, and protected values against feasible-space size. Minimal-core extraction can accelerate action but can also hide alternative cores. Optimization can compare options efficiently while laundering value judgments into weights. Resource expansion can preserve promises but create new dependency, cost, or sustainability burdens.

Failure modes¶

The most dangerous failure is a false impossibility caused by a bad model. Other common failures are treating timeout as proof, relying on pairwise checks, converting hard constraints into soft penalties without authority, assuming the first core is unique, citing a theorem outside its assumptions, exporting harm beyond the boundary, and preserving the original promise after implementation has weakened it.

A second class of failure occurs after a technically correct proof. Decision makers may imply that “the math chose” one sacrifice, exclude affected groups, or bury conditionality in fine print. The remedy is to separate certificate from choice, preserve the decision rationale and dissent, and make the residual guarantee operationally authoritative.

Neighbor distinctions¶

Constraint Formulation defines the commitments; this archetype resolves a proved empty feasible set.
Constraint Propagation and Decoupling derives implications and partitions the problem; it may expose a core but does not choose the sacrifice.
Pareto Frontier Navigation compares feasible trade-offs after the impossible all-at-once point is removed.
Objective Weighting Governance controls soft-objective weights; it must not demote protected commitments silently.
Tradeoff Guardrail supplies protected invariants that bound the resolution.
Composability Testing and Validation and Antagonism Screening and Separation focus on component interaction rather than a general commitment-set proof.
Paradox Reframing dissolves apparent contradictions through semantic or level changes; this archetype applies when incompatibility survives that repair.
Deductive Chain Validation checks the proof; it does not own the governed relaxation.
Assumption-Bounded Distributed Agreement is a domain application of impossibility-bounded guarantees rather than a duplicate general parent.

Examples¶

Fixed-budget public benefit¶

A program cannot simultaneously keep a statutory budget cap, universal eligibility, and an unchanged benefit after enrollment exceeds the funded population. The proof establishes necessity of change. The authorized process—not the arithmetic—chooses supplemental funding, narrower eligibility, lower benefits, or conditional pro-rating and records the distributional consequences.

Hard-deadline scheduling¶

A set of exclusive-machine jobs has processing times and hard deadlines that cannot all fit. An unsatisfiable core identifies the conflicting jobs. Options include overtime, extra capacity, deadline changes, preemption, or dropping work. The final schedule and service promise are updated together.

Distributed agreement¶

A protocol specification asks for agreement, validity, and unconditional termination under a fully asynchronous fault model. The impossibility boundary forces a declared timing, randomness, availability, or guarantee change. The final contract states when progress is conditional and what happens during partitions.

Engineering design¶

Mass, stiffness, cost, geometry, and certified-material constraints leave no candidate design. The team protects safety and certification, verifies the model, and compares material, geometry, cost, and performance relaxations. The new limits propagate to tests, procurement, and customer claims.

Non-examples¶

A feasible cost–quality frontier is ordinary multiobjective optimization. An ambiguous definition is a schema or language problem. A chemical incompatibility between materials is antagonism screening. A solver that failed to find a solution has not proved impossibility. A controversial but internally consistent axiom set is an assumption or warrant issue, not this archetype.

Practical review questions¶

What exact conjunction is claimed, over which domain, time horizon, and assumptions?
Can anyone produce a satisfying witness?
Is the infeasibility result sound, independently checkable, and distinguishable from search failure?
What are the materially different minimal unsatisfiable cores?
Which commitments are protected, and who authorized that status?
What resolution operators restore feasibility without exporting hidden harm?
Who has legitimate authority and stakeholder standing to choose among them?
What exactly remains guaranteed after the choice?
How will downstream documents and behavior be updated?
What future change triggers a recheck?

Common Mechanisms¶

Compatibility Matrix — A pairwise register of which constituents may share a domain and which must be kept apart, each verdict tied to the antagonism condition and the evidence behind it.
Constraint Relaxation Experiment — Systematically loosens one commitment at a time — while holding the protected ones fixed — and re-tests, to learn which relaxation restores feasibility and at what cost.
Constraint-Satisfaction Solver Pass — Encodes the commitments as a formal constraint model and runs a solver that propagates them to a reduced feasible region — or mechanically detects that no joint solution exists.
Decision Record with Residue — Captures the chosen resolution as a durable record that also ledgers what survived and what was given up — the guarantees that still hold, the losses accepted, and everything the decision now touches downstream.
Impossibility-Theorem Instantiation Review — Checks whether the requirement set is a disguised instance of an already-proven impossibility theorem, so a known 'you cannot have all of these at once' result settles the conflict without a fresh search.
Minimal Unsatisfiable Core Extraction — Given a set already proven to have no joint solution, strips it down to a smallest subset that is still unsatisfiable — the irreducible knot of commitments that actually clash.
Pareto Frontier Analysis — Maps the frontier of non-dominated designs among competing objectives, exposing the exchange rate between them so a priority choice can be made with eyes open instead of chasing an impossible all-at-once optimum.
Proof Checking — Independently re-verifies a decidability or impossibility proof step by step, so the boundary claim rests on a checked argument rather than on its author's authority.
Requirements Traceability Matrix — Threads every requirement through to the design, code, and verification that satisfy it, so any requirement with no downstream link — or no passing test — is a visible coverage hole.
SAT/SMT Satisfiability Check — 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.
Scenario Sensitivity Sweep — Varies the uncertain inputs across plausible scenarios to learn whether the incompatibility is robust or an artifact of one assumption — and which assumptions, if they moved, would flip the verdict.
Scope-Boundary Stress Test — Pushes each commitment to the edges of where it is meant to apply, to reveal whether the incompatibility is genuine or an artifact of over-broad scope that a sharper boundary would dissolve.
Stakeholder Frontier Review — Convenes the owners of the conflicting commitments to choose, under named authority, which one yields at the frontier of feasible options — turning a computed trade-off into a legitimate, owned decision.
Weighted MaxSAT or Soft-Constraint Optimization — When the commitments can't all hold, splits them into hard constraints that must never break and weighted soft ones, then computes the assignment that keeps every hard constraint while sacrificing the least-valuable softs.

Compression statement¶

Given a scoped set of axioms, requirements, guarantees, or prohibitions, normalize their semantics and strength; construct one joint satisfiability model; distinguish a genuine empty feasible set from search failure or modeling error; extract and independently verify one or more minimal unsatisfiable cores; protect non-negotiable invariants; enumerate removal, weakening, scoping, conditionalization, sequencing, assumption-change, resource-expansion, and architecture-change options; select a satisfiable resolution through an explicit authority and priority rule; then trace impacts and replace the impossible original promise with a residual guarantee ledger and recheck triggers.

Canonical formula: Let C = {c₁,…,cₙ} be commitments interpreted over decision space X under assumptions A and scope S. If F(C,A,S) = {x ∈ X : x satisfies every cᵢ} = ∅, find an inclusion-minimal U ⊆ C with F(U,A,S)=∅ and an incompatibility certificate π. Choose a resolution operator ρ from remove, weaken, scope, conditionalize, sequence, substitute, change A, expand X, or redesign, subject to protected invariants P, such that F(ρ(C,A,S)) ≠ ∅. Publish Δ = C − ρ(C,A,S), the residual guarantee G, decision rationale R, and recheck trigger T.

Abstractions this archetype builds on — directly (a source ingredient) or as a related pattern. Links follow the typed catalog namespace.

Built directly on (5)

Axiom: A claim a system declines to derive — a load-bearing starting point accepted without proof so that the rest of the structure can be built on top of it.
Axiomatic Incompatibility: A small set of individually plausible axioms is provably jointly unsatisfiable, forcing a chosen trade-off.
Consistency: A set of commitments cannot jointly derive a contradiction.
Constraint: Limits possibilities to guide outcomes.
Trade-offs: Balancing competing priorities.

Also references 22 related abstractions

Applicability Scope: An artifact publishes a bounded region of conditions under which its outputs or guarantees hold, so consumers can detect out-of-scope use before it causes harm.
Boundedness: Values remain within limits.
Closure: Ensures operations remain within a set.
Compatibility: The relational condition under which two or more entities can coexist or compose without breakage, interference, or contradiction.
Consensus: Producing a single shared decided state from many participants with disagreeing or adversarial views, under a fault model, satisfying agreement, validity, and termination together.
Counterfactual Reasoning: Hypothetical alternatives.
Decision: Committing to one alternative from a set under uncertainty and trade-off, collapsing open deliberation into a chosen path and foreclosing the others.
Diagonal Impossibility: In a self-modeling system, a putative total analyzer is refuted by constructing an object engineered to make the analyzer's verdict on it contradict the property it decides.
Formal System: Symbols, formation rules, axioms, and inference rules closed under mechanical derivation.
Local-to-Global Aggregation: Locally checkable properties promote to a global verdict under an explicit aggregation discipline.

▸ Show 12 more

Variants¶

Narrower or domain-specific specializations that share this archetype's core structure. Recognized variants are established; candidate variants are provisional.

Trilemma Resolution · subtype · recognized

Resolves an exactly three-property incompatibility by proving the joint guarantee impossible and choosing which property to drop, weaken, scope, sequence, or condition.

Distinct from parent: The parent handles incompatibility among any number of commitments; this variant requires a three-property core and names the three drop, scope, or dissolve paths.
Use when: The conflict is naturally expressed as three desirable properties or guarantees; The “pick any two” framing is supported by a proof or explicit model rather than repeated as a slogan; Each of the three sacrifice paths has materially different consequences or stakeholders.
Typical domains: distributed systems, public policy, social choice, architecture and engineering
Common mechanisms: impossibility theorem instantiation review, pareto frontier analysis, stakeholder frontier review, decision record with residue

Impossibility-Bounded Guarantee Scoping · risk or failure variant · recognized

Responds to a proven impossibility boundary by narrowing the conditions under which a guarantee is claimed instead of pretending the theorem does not apply.

Distinct from parent: The parent permits many resolution operators; this variant emphasizes conditional guarantees and scope detectors.
Use when: A theorem rules out a universal or unconditional guarantee under stated assumptions; A useful conditional guarantee is still possible inside a narrower fault, input, timing, distribution, or competence region; Consumers can detect when the system has left that region and can safely defer, degrade, or switch modes.
Typical domains: machine learning, distributed systems, optimization, formal verification
Common mechanisms: impossibility theorem instantiation review, scope boundary stress test, scenario sensitivity sweep

Normative Commitment Incompatibility Resolution · governance variant · recognized

Resolves jointly impossible duties, rights, policy promises, or governance commitments through legitimate priority, exception, compensation, and review rules.

Distinct from parent: The parent is domain-general; this variant adds legitimacy and distributional requirements to the choice among feasible relaxations.
Use when: The incompatible commitments encode value judgments or obligations rather than only technical constraints; Different groups bear the losses associated with different relaxations; No formal proof can by itself determine which commitment should yield.
Typical domains: law and regulation, public policy, institutional governance, ethics
Common mechanisms: stakeholder frontier review, decision record with residue, requirements traceability matrix

Near names: Axiomatic Incompatibility Resolution, Inconsistent Requirement Set Resolution, Hard-Constraint Conflict Resolution, Unsatisfiable-Core Resolution, Impossibility-Aware Tradeoff Design, Guarantee-Set Reconciliation.