242 lines
12 KiB
Python
242 lines
12 KiB
Python
"""第四问覆盖证书与最小命中集搜索（CLI；核心实现见 mcm26b.guarantee.cover）。
|
||
|
||
第四问的定向源在"读点位于源的前向半平面内"时才可能被检出，因此
|
||
"某频道在所有被访点都 no_signal ⟹ 该频道不存在源"的缺席证明，等价于要求
|
||
被访点集合 S 满足
|
||
|
||
∀ p ∈ Ω, ∀ h ∈ [0,360): ∃ c ∈ S,
|
||
|c − p| ≤ r_eff_min(1000) 且 (c − p)·u(h) ≥ 0
|
||
|
||
（题面规定朝向覆盖"两侧各 90 度，含边界"，故取 ≥ 0）。现役 49 点方格的
|
||
"单元对角 ≤ 1000"是**充分**条件但远非必要；本脚本用贪心击中集求等价覆盖的
|
||
更小点集，并输出可复现证书。
|
||
|
||
uv run python scripts/verify_q4_cover.py # 校核 + 搜索 + 打印
|
||
uv run python scripts/verify_q4_cover.py --spacing 200 --write-plan q4_mincover_v1
|
||
uv run python scripts/verify_q4_cover.py --check-json my_points.json
|
||
"""
|
||
|
||
from __future__ import annotations
|
||
|
||
import argparse
|
||
import hashlib
|
||
import json
|
||
from pathlib import Path
|
||
|
||
from mcm26b.config import ProblemConfig
|
||
from mcm26b.guarantee import (CERTIFY_HEADINGS, CERTIFY_STEP_M, R_EFF_MIN_M,
|
||
CoverageCertificate, CoveragePlan,
|
||
candidate_lattice, coverage_masks, forward_targets,
|
||
greedy_cover, omega_positions, plan_names,
|
||
square_49_plan, verify_full_disk,
|
||
verify_forward_half_disk, verify_plan, write_plan)
|
||
|
||
ROOT = Path(__file__).resolve().parents[1]
|
||
DEFAULT_PLAN_DIR = ROOT / "src/mcm26b/guarantee/plans"
|
||
|
||
|
||
def _report(points, kind: str, step_m: float, headings: int,
|
||
r_eff: float = R_EFF_MIN_M,
|
||
heading_margin_deg: float = 0.0) -> dict:
|
||
"""按覆盖语义校核点集，返回证书字典。"""
|
||
if kind == "forward_half_disk":
|
||
certificate = verify_forward_half_disk(points, step_m, headings,
|
||
r_eff=r_eff,
|
||
heading_margin_deg=heading_margin_deg)
|
||
else:
|
||
certificate = verify_full_disk(points, step_m, r_eff)
|
||
return certificate.as_dict()
|
||
|
||
|
||
def prune_redundant(masks: list[int], chosen: list[int]) -> list[int]:
|
||
"""贪心结果冗余剪枝：删掉任何"其余点已完全覆盖其目标"的点。"""
|
||
full = 0
|
||
for index in chosen:
|
||
full |= masks[index]
|
||
pruned = list(chosen)
|
||
changed = True
|
||
while changed:
|
||
changed = False
|
||
for index in list(pruned):
|
||
rest = 0
|
||
for other in pruned:
|
||
if other != index:
|
||
rest |= masks[other]
|
||
if rest == full:
|
||
pruned.remove(index)
|
||
changed = True
|
||
return pruned
|
||
|
||
|
||
def fine_prune(points, step_m: float, headings: int, r_eff: float,
|
||
heading_margin_deg: float):
|
||
"""证书分辨率上的冗余剪枝：删掉任何点后校核仍 0 缺口才真删。
|
||
|
||
粗网格（搜索用）上的冗余判据偏保守，会在证书分辨率下留下可删的点；
|
||
本步每个候选删除都用**证书同一口径**复核，因此不削弱证书。
|
||
"""
|
||
points = list(points)
|
||
improved = True
|
||
while improved:
|
||
improved = False
|
||
for index in range(len(points)):
|
||
trial = points[:index] + points[index + 1:]
|
||
certificate = verify_forward_half_disk(
|
||
trial, step_m, headings, r_eff=r_eff,
|
||
heading_margin_deg=heading_margin_deg)
|
||
if certificate.uncovered == 0:
|
||
points = trial
|
||
improved = True
|
||
print(f" 精细剪枝：删点后仍 0 缺口，剩 {len(points)} 点", flush=True)
|
||
break
|
||
return points
|
||
|
||
|
||
def main() -> int:
|
||
parser = argparse.ArgumentParser(description=__doc__.splitlines()[0])
|
||
parser.add_argument("--spacing", type=float, default=200.0,
|
||
help="贪心候选点网格间距（米）")
|
||
parser.add_argument("--radius", type=float, default=2850.0,
|
||
help="候选点所在圆盘半径（米）")
|
||
parser.add_argument("--target-step", type=float, default=CERTIFY_STEP_M,
|
||
help="搜索用采样位置步长（米）")
|
||
parser.add_argument("--headings", type=int, default=CERTIFY_HEADINGS,
|
||
help="搜索用采样朝向档数")
|
||
parser.add_argument("--verify-step", type=float, default=None,
|
||
help="证书校核位置步长（默认等于 --target-step）")
|
||
parser.add_argument("--verify-headings", type=int, default=None,
|
||
help="证书校核朝向档数（默认等于 --headings）")
|
||
parser.add_argument("--design-radius", type=float, default=None,
|
||
help="搜索时的设计距离（默认 1000；<1000 即留裕量）")
|
||
parser.add_argument("--heading-margin", type=float, default=0.0,
|
||
help="搜索时的前向角裕量（度）")
|
||
parser.add_argument("--verify-radius", type=float, default=None,
|
||
help="证书校核距离（默认 1000；<1000 即留裕量）")
|
||
parser.add_argument("--verify-heading-margin", type=float, default=0.0,
|
||
help="证书校核前向角裕量（度）；应 ≥ 180/verify_headings/2")
|
||
parser.add_argument("--no-prune", action="store_true", help="关闭冗余剪枝")
|
||
parser.add_argument("--fine-prune", action="store_true",
|
||
help="在证书分辨率上再做一轮冗余剪枝（删点后仍 0 缺口才删）")
|
||
parser.add_argument("--coverage", choices=("forward_half_disk", "full_disk"),
|
||
default="forward_half_disk", help="覆盖语义")
|
||
parser.add_argument("--check-json", type=Path, default=None,
|
||
help="只校核给定点集（[[x,y],...] 或 {\"points\":[...]}）")
|
||
parser.add_argument("--write-plan", default=None,
|
||
help="把贪心最小集写成覆盖计划（名称，落 src/mcm26b/guarantee/plans/）")
|
||
parser.add_argument("--out", type=Path, default=None, help="证书 JSON 输出路径")
|
||
args = parser.parse_args()
|
||
|
||
verify_step = (args.verify_step if args.verify_step is not None
|
||
else args.target_step)
|
||
verify_headings = (args.verify_headings if args.verify_headings is not None
|
||
else args.headings)
|
||
design_radius = (args.design_radius if args.design_radius is not None
|
||
else R_EFF_MIN_M)
|
||
verify_radius = (args.verify_radius if args.verify_radius is not None
|
||
else R_EFF_MIN_M)
|
||
|
||
if args.check_json is not None:
|
||
payload = json.loads(args.check_json.read_text(encoding="utf-8"))
|
||
raw = payload.get("points") if isinstance(payload, dict) else payload
|
||
points = [tuple(map(float, p)) for p in raw]
|
||
report = _report(points, args.coverage, verify_step, verify_headings,
|
||
verify_radius, args.verify_heading_margin)
|
||
print(json.dumps(report, ensure_ascii=False, indent=2))
|
||
return 0 if report["uncovered"] == 0 else 1
|
||
|
||
shipped = square_49_plan()
|
||
shipped_report = _report(shipped.points, "forward_half_disk",
|
||
verify_step, verify_headings,
|
||
verify_radius, args.verify_heading_margin)
|
||
print(f"目标空间：{shipped_report['targets']} 个 (p,h)"
|
||
f"（校核位置步长 {verify_step} m，朝向 {verify_headings} 档，"
|
||
f"r_verify={verify_radius:.0f} m，角裕量 "
|
||
f"{args.verify_heading_margin}°）")
|
||
print(f"现役 {shipped.name}：{len(shipped.points)} 点，"
|
||
f"缺口 {shipped_report['uncovered']}，"
|
||
f"NN 巡回 {shipped_report['nn_tour_m'] / 1000:.1f} km"
|
||
f"（{shipped_report['nn_tour_virtual_s']:.0f} s 移动）", flush=True)
|
||
|
||
targets = forward_targets(args.target_step, args.headings)
|
||
candidates = candidate_lattice(args.spacing, args.radius)
|
||
print(f"候选点 {len(candidates)}（{args.spacing} m 网格，半径 {args.radius} m）；"
|
||
f"设计裕量 r_design={design_radius:.0f} m，前向角裕量 "
|
||
f"{args.heading_margin}°", flush=True)
|
||
masks = coverage_masks(targets, candidates, r_eff=design_radius,
|
||
heading_margin_deg=args.heading_margin)
|
||
chosen = greedy_cover(masks, len(targets))
|
||
if not args.no_prune:
|
||
chosen = prune_redundant(masks, chosen)
|
||
best_points = [candidates[i] for i in chosen]
|
||
if args.fine_prune:
|
||
best_points = fine_prune(best_points, verify_step, verify_headings,
|
||
verify_radius, args.verify_heading_margin)
|
||
best_report = _report(best_points, "forward_half_disk",
|
||
verify_step, verify_headings,
|
||
verify_radius, args.verify_heading_margin)
|
||
print(f"设计裕量最小命中集：{len(best_points)} 点，缺口 {best_report['uncovered']}，"
|
||
f"NN 巡回 {best_report['nn_tour_m'] / 1000:.1f} km"
|
||
f"（{best_report['nn_tour_virtual_s']:.0f} s 移动）", flush=True)
|
||
|
||
if best_report["uncovered"] != 0:
|
||
print("贪心结果未通过证书校核，拒绝生成计划。")
|
||
return 1
|
||
|
||
generator = {"script": "scripts/verify_q4_cover.py",
|
||
"spacing_m": args.spacing, "radius_m": args.radius,
|
||
"target_step_m": args.target_step, "headings": args.headings,
|
||
"design_r_eff_m": design_radius,
|
||
"heading_margin_deg": args.heading_margin,
|
||
"pruned": not args.no_prune,
|
||
"verify_step_m": verify_step,
|
||
"verify_headings": verify_headings,
|
||
"verify_r_eff_m": verify_radius,
|
||
"verify_heading_margin_deg": args.verify_heading_margin,
|
||
"code_sha256": hashlib.sha256(
|
||
Path(__file__).read_bytes()).hexdigest()}
|
||
certificate = CoverageCertificate(
|
||
kind=best_report["kind"], target_step_m=verify_step,
|
||
headings=verify_headings, r_eff_min_m=verify_radius,
|
||
targets=best_report["targets"], uncovered=best_report["uncovered"],
|
||
worst_hit_distance_m=best_report["worst_hit_distance_m"],
|
||
nn_tour_m=best_report["nn_tour_m"],
|
||
generator_sha256=generator["code_sha256"],
|
||
verify_heading_margin_deg=args.verify_heading_margin)
|
||
plan = CoveragePlan(
|
||
name=args.write_plan or "q4_mincover_draft", problem=4,
|
||
kind="certified", coverage="forward_half_disk",
|
||
note=(f"设计裕量最小命中集：{len(best_points)} 点，"
|
||
f"r_design={design_radius:.0f} m / 前向角裕量 {args.heading_margin}°；"
|
||
f"证书按 {verify_step:.0f} m/{verify_headings} 档、r_verify="
|
||
f"{verify_radius:.0f} m、角裕量 {args.verify_heading_margin}° "
|
||
f"校核缺口 0（同一证书口径复核，含精细剪枝）；最坏命中 "
|
||
f"{best_report['worst_hit_distance_m']:.0f} m，"
|
||
f"NN 巡回 {best_report['nn_tour_m'] / 1000:.1f} km"),
|
||
generator=generator, certificate=certificate,
|
||
points=tuple(best_points))
|
||
payload = {"model": {"r_omega_m": 1800.0, "r_eff_min_m": 1000.0},
|
||
"design": {"r_design_m": design_radius,
|
||
"heading_margin_deg": args.heading_margin},
|
||
"verify": {"r_eff_m": verify_radius,
|
||
"heading_margin_deg": args.verify_heading_margin,
|
||
"step_m": verify_step, "headings": verify_headings},
|
||
"shipped": shipped_report, "mincover": best_report}
|
||
if args.out is not None:
|
||
out = args.out if args.out.is_absolute() else ROOT / args.out
|
||
out.parent.mkdir(parents=True, exist_ok=True)
|
||
out.write_text(json.dumps(payload, ensure_ascii=False, indent=2) + "\n",
|
||
encoding="utf-8")
|
||
print(f"证书已写入 {out}")
|
||
if args.write_plan:
|
||
target = DEFAULT_PLAN_DIR / f"{args.write_plan}.json"
|
||
write_plan(plan, target)
|
||
verified = verify_plan(plan)
|
||
print(f"计划已写入 {target}；运行期分辨率复核缺口 {verified.uncovered}")
|
||
print("已注册计划：" + "，".join(plan_names()))
|
||
_ = (ProblemConfig(), omega_positions) # 保持公开入口可发现性
|
||
return 0
|
||
|
||
|
||
if __name__ == "__main__":
|
||
raise SystemExit(main())
|