From f0e0e817d0075c89952079ad9a5594b85e1a2ef8 Mon Sep 17 00:00:00 2001 From: Yernat Yestekov Date: Tue, 11 Aug 2026 17:24:28 -0700 Subject: [PATCH] fix(processor): fail loudly on z3 unknown in satisfiability solver Under load the per-call 5s z3 timeout can return z3.unknown. The pinned adapter treated that non-decisive result as decisive: _reduce_unsat_core kept any clause whose removal did not return unsat, and _select_witness skipped any domain value that did not return sat. A timed-out check therefore silently emitted a non-minimal core or a non-canonical witness while the published SolverConfigurationModel still claimed subset-minimal core reduction and canonical-lexicographic witness selection, surfacing later as spurious replay_satisfiability_evidence failures instead of a diagnosable error. _check now raises SolverOperationalError on z3.unknown (reported as SatisfiabilityOperationalError at the service boundary), so every decision is decisive or fails loudly. It also asserts an explicit false for empty finite-domain memberships instead of relying on zero-argument z3.Or, and solve_model rejects duplicate clause ids at the boundary rather than letting them collapse in the tracking table (which z3 otherwise rejects with an opaque exception). Co-Authored-By: Claude Opus 5 (1M context) --- .../raes_processor/satisfiability/_solver.py | 42 +++++++--- .../tests/test_scenario_satisfiability.py | 84 +++++++++++++++++++ 2 files changed, 116 insertions(+), 10 deletions(-) diff --git a/implementations/python/packages/raes_processor/satisfiability/_solver.py b/implementations/python/packages/raes_processor/satisfiability/_solver.py index 41ecb4419..8658280b5 100644 --- a/implementations/python/packages/raes_processor/satisfiability/_solver.py +++ b/implementations/python/packages/raes_processor/satisfiability/_solver.py @@ -22,19 +22,32 @@ class SolverResult: def solve_model(model: NormalizedConstraintModel) -> SolverResult: """Solve one normalized model and select deterministic portable evidence.""" + _require_unique_clause_ids(model) all_clause_ids = tuple(clause.clause_id for clause in model.clauses) - status = _check(model, all_clause_ids, {}) - if status == z3.sat: + # ``_check`` fails loudly on ``z3.unknown``, so a non-satisfiable decision + # here is decisively unsatisfiable rather than an incomplete timeout. + if _check(model, all_clause_ids, {}) == z3.sat: return SolverResult( outcome=SatisfiabilityOutcome.SATISFIABLE, assignment=_select_witness(model, all_clause_ids), ) - if status == z3.unsat: - return SolverResult( - outcome=SatisfiabilityOutcome.UNSATISFIABLE, - core=_reduce_unsat_core(model, all_clause_ids), - ) - raise SolverOperationalError("solver returned an incomplete result") + return SolverResult( + outcome=SatisfiabilityOutcome.UNSATISFIABLE, + core=_reduce_unsat_core(model, all_clause_ids), + ) + + +def _require_unique_clause_ids(model: NormalizedConstraintModel) -> None: + """Reject collapsed clause identity before it can corrupt tracked evidence. + + ``_check`` tracks each clause by a name derived from its id; duplicate ids + collapse in the lookup table while z3 rejects the repeated assumption, so the + invariant is enforced explicitly at the solver boundary rather than silently. + """ + + clause_ids = [clause.clause_id for clause in model.clauses] + if len(set(clause_ids)) != len(clause_ids): + raise SolverOperationalError("normalized model contains duplicate clause ids") def _select_witness( @@ -93,11 +106,20 @@ def _check( for index, value in enumerate(symbol.domain) if any(_scalar_equal(value, allowed) for allowed in clause.allowed_values) ] - expression = z3.Or(*(variables[symbol.symbol_id] == index for index in indexes)) + # An empty allowed set is an unsatisfiable membership; assert false + # explicitly instead of depending on a zero-argument ``z3.Or``. + expression = ( + z3.Or(*(variables[symbol.symbol_id] == index for index in indexes)) if indexes else z3.BoolVal(False) + ) solver.assert_and_track(expression, z3.Bool(_z3_name(clause_id))) for symbol_id, index in fixed.items(): solver.add(variables[symbol_id] == index) - return solver.check() + result = solver.check() + if result == z3.unknown: + # A per-call timeout returns unknown; treating it as a decisive answer + # would silently break unsat-core minimality or witness canonicality. + raise SolverOperationalError(f"solver returned unknown: {solver.reason_unknown()}") + return result def _scalar_equal(left: object, right: object) -> bool: diff --git a/implementations/python/tests/test_scenario_satisfiability.py b/implementations/python/tests/test_scenario_satisfiability.py index e397c58c8..eb67dcc3a 100644 --- a/implementations/python/tests/test_scenario_satisfiability.py +++ b/implementations/python/tests/test_scenario_satisfiability.py @@ -7,6 +7,7 @@ from pathlib import Path import pytest +import z3 from pydantic import ValidationError from raes_contracts.satisfiability import ( SatisfiabilityOutcome, @@ -14,9 +15,11 @@ ) from raes_processor.satisfiability import ( SatisfiabilityEvidenceError, + SatisfiabilityOperationalError, analyze_scenario_file, replay_satisfiability_evidence, ) +from raes_processor.satisfiability._solver import SolverOperationalError, solve_model _SATISFIABLE = """\ name: satisfiable-control @@ -63,6 +66,21 @@ cpu: ${cpu_count} """ +_EMPTY_TARGET_DOMAIN = """\ +name: empty-target-domain +variables: + copies: + type: integer + allowed_values: [0] + required: true +nodes: + target: + type: vm +infrastructure: + target: + count: ${copies} +""" + def _write(tmp_path: Path, name: str, content: str) -> Path: path = tmp_path / name @@ -313,3 +331,69 @@ def test_published_valid_and_invalid_fixtures_enforce_outcome_joins() -> None: ScenarioSatisfiabilityEvidenceModel.model_validate_json(invalid_payload) assert "outcome must select exactly one matching payload" in str(exc_info.value) + + +def _force_unknown_on_call(monkeypatch: pytest.MonkeyPatch, target_call: int) -> None: + """Make the ``target_call``-th z3 check report ``unknown`` (a timeout proxy).""" + + original = z3.Solver.check + state = {"calls": 0} + + def patched(self: z3.Solver, *assumptions: object) -> z3.CheckSatResult: + state["calls"] += 1 + if state["calls"] == target_call: + return z3.unknown + return original(self, *assumptions) + + monkeypatch.setattr(z3.Solver, "check", patched) + + +def test_unknown_during_core_reduction_fails_loudly_without_forging_minimality( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + source = _write(tmp_path, "unsatisfiable.sdl.yaml", _UNSATISFIABLE) + # Call one is the decisive UNSAT check; call two is the first deletion probe, + # where an undetected timeout would silently retain a droppable clause and + # publish a core claiming subset-minimality it never established. + _force_unknown_on_call(monkeypatch, target_call=2) + + with pytest.raises(SatisfiabilityOperationalError): + analyze_scenario_file(source) + + +def test_unknown_during_witness_selection_fails_loudly_without_forging_canonicality( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + source = _write(tmp_path, "satisfiable.sdl.yaml", _SATISFIABLE) + # Call one decides SAT; call two probes the canonical first domain value, + # where an undetected timeout would skip it and forge a non-lexicographic + # witness while still claiming canonical-lexicographic selection. + _force_unknown_on_call(monkeypatch, target_call=2) + + with pytest.raises(SatisfiabilityOperationalError): + analyze_scenario_file(source) + + +def test_duplicate_clause_ids_rejected_at_solver_boundary(tmp_path: Path) -> None: + source = _write(tmp_path, "satisfiable.sdl.yaml", _SATISFIABLE) + model = analyze_scenario_file(source).normalized_model + # ``model_copy`` bypasses contract validation to inject a collapsed clause + # id; the solver must reject it rather than track the assumption twice. + duplicated = model.model_copy(update={"clauses": model.clauses + (model.clauses[0],)}) + + with pytest.raises(SolverOperationalError, match="duplicate clause ids"): + solve_model(duplicated) + + +def test_empty_target_domain_is_unsatisfiable(tmp_path: Path) -> None: + source = _write(tmp_path, "empty-target-domain.sdl.yaml", _EMPTY_TARGET_DOMAIN) + + evidence = analyze_scenario_file(source) + + assert evidence.outcome is SatisfiabilityOutcome.UNSATISFIABLE + assert evidence.unsat_core is not None + # The count target admits only values >= 1, so a {0} domain produces an empty + # membership clause that must resolve to false, not a bare zero-argument Or. + assert any(clause.allowed_values == () for clause in evidence.normalized_model.clauses)