Weighted MaxSAT or Soft-Constraint Optimization¶

Optimization tool — instantiates Incompatible Requirement Set Resolution

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.

A bare satisfiability check answers an infeasible set with a blunt "no" and stops. Weighted MaxSAT / Soft-Constraint Optimization keeps going: it marks some constraints hard (inviolable) and assigns the rest numeric weights, then computes the assignment that satisfies every hard constraint while maximizing the total weight of satisfied soft ones — equivalently, minimizing the weight of what it breaks. Its defining move is to reframe the archetype's central question, which commitment yields?, as an optimization with an explicit objective: the tool does not just find a relaxation, it computes the least-costly legitimate relaxation given the priorities you encode, and reports precisely which softs it sacrificed and why. Where a plain solver tells you the set is impossible, this one hands back the best possible near-miss.

Example¶

A conference committee must place ≈120 accepted talks into rooms and time slots. Hard constraints, non-negotiable: a speaker is never in two places at once; a room holds one talk per slot; nothing is scheduled before its speaker arrives. Soft, weighted by how much the committee cares: keep same-track talks contiguous (weight 5 each), honor speakers' preferred slots (weight 3), and above all don't clash the two headline talks against each other (weight 8). No timetable grants every wish. Weighted MaxSAT searches for the schedule that keeps all the hard rules and maximizes satisfied soft weight — and reports, say, that the optimum sacrifices two speakers' slot preferences (cost 6) rather than clash the headliners (cost 8). The output is a concrete, buildable schedule plus the itemized list of which preferences it broke and the weight logic behind each — a decision the committee can inspect, contest, and re-run with different weights. Timetabling and rostering are canonical homes for soft-constraint optimization for exactly this reason.

How it works¶

Three moves distinguish it. First, classify every constraint as hard or soft — the hard set defines what the answer must never violate. Second, attach weights to the softs; the weight vector is the priority rule the optimizer ranks candidate relaxations against (additive weights, or strict lexicographic tiers when some concerns must dominate others outright). Third, optimize: a MaxSAT engine (branch-and-bound, or modern core-guided search) returns the assignment of maximum satisfied soft-weight subject to all hard constraints. The relaxation is thus an output — computed, itemized, and reproducible — not a choice made by hand. Crucially, the tool does not judge whether the weights are legitimate; it faithfully optimizes whatever objective it is handed.

Tuning parameters¶

Hard/soft partition — which constraints are inviolable versus negotiable. Over-hardening can make even MaxSAT infeasible (no assignment satisfies the hard set); under-hardening lets the optimizer sacrifice something that should never have moved.
Weight scale / priority encoding — the numbers that rank the softs. Additive weights trade concerns off continuously; lexicographic tiers enforce strict precedence. This encoding is the constraint-priority rule, and it decides which relaxation wins.
Objective form — maximize total satisfied weight, minimize total violated weight, or minimize the single worst violation (a leximin/fairness objective). Each encodes a different notion of "least-bad."
Optimality vs. anytime — demand a certified optimum, or accept the best solution found within a time budget. Large instances often reach only a good feasible answer.
Tie-breaking — which rule chooses among several assignments that share the top score.

When it helps, and when it misleads¶

Its strength is that it refuses to stop at "impossible": it produces an actual, buildable least-cost relaxation and makes the value trade-offs explicit and re-runnable — change a weight, watch the sacrificed set move, and see the sensitivity directly.

Its hazard is that the optimum is "best" only relative to the weights, which are themselves contestable value judgments. Collapsing many concerns into one weighted sum can hide trade-offs and select a corner solution no stakeholder actually endorses.^[1] And the classic run-backwards move is to tune the weights until the solver returns the answer you had already chosen, then present it as "the optimal solution." The discipline that keeps it honest is to separate who sets the weights (a governance act) from the solver that optimizes them, sanity-check the sacrificed set against the people who own those commitments, and probe weight sensitivity rather than trusting a single objective's headline result.

How it implements the components¶

Weighted MaxSAT fills the choose-the-relaxation side of the archetype — the components that turn "infeasible" into a specific, ranked concession:

constraint_strength_classification — the hard/soft split is the tool's first and defining act, fixing what may never break versus what may bend.
relaxation_option — every violable soft constraint is a candidate relaxation, and the optimizer's output is exactly the chosen set of concessions.
constraint_priority_rule — the weights (additive or lexicographic) operationalize the priority ordering the optimizer ranks relaxations by, mechanically applying it to select the least-cost one.

It does not decide bare satisfiability (joint_satisfiability_model, feasible_set — that's SAT/SMT Satisfiability Check) or legitimize the weights and authorize the sacrifice (protected_invariant, exception_authority, tradeoff_rationale — that's Stakeholder Frontier Review); it computes the least-cost relaxation for whatever priorities it is given.

Instantiates: Incompatible Requirement Set Resolution — supplies the computed least-cost relaxation and its itemized concessions for governance to legitimize.
Consumes: SAT/SMT Satisfiability Check — reached for once a plain satisfiability check reports the set unsatisfiable; it also relies on a priority weighting supplied from outside the tool.
Sibling mechanisms: SAT/SMT Satisfiability Check · Stakeholder Frontier Review · Minimal Unsatisfiable Core Extraction · Impossibility-Theorem Instantiation Review · Pareto Frontier Analysis · Constraint Relaxation Experiment · Constraint-Satisfaction Solver Pass · Compatibility Matrix · Requirements Traceability Matrix · Proof Checking · Scenario Sensitivity Sweep · Scope-Boundary Stress Test · Decision Record with Residue

Notes¶

The hard set can itself be jointly unsatisfiable — if the constraints you marked inviolable already conflict, MaxSAT has no feasible assignment and returns nothing. That is not a tool failure but a signal to push the hard constraints back through Minimal Unsatisfiable Core Extraction or Impossibility-Theorem Instantiation Review: something you declared non-negotiable has to move before any optimization is possible.

References¶

[1] Collapsing multiple objectives into a single weighted sum — scalarization — is a standard but lossy move in multi-objective optimization: the result is highly sensitive to the chosen weights, and a pure weighted sum can never reach certain trade-off points (those on non-convex parts of the frontier). This is why the weights deserve as much scrutiny as the solver's answer. ↩