Migra C1 de Set Covering para Set Partitioning e documenta limitacoes (v0.10)

- C1 alterado: z[nid] <= 1 -> z[nid] == 1 para todas as missoes; toda missao
  deve ser coberta por exatamente 1 aeronave (sem missoes descobertas).
- n_missoes padrao reduzido de 50 para 20 (n_evam de 5 para 4): garante
  factibilidade do MIP com Set Partitioning no envelope de 4 aeronaves.
- Time limit padrao do solver CBC fixado em 120 s (era ilimitado): evita
  travamento ao tentar provar infeasibility.
- Corrigido display "Not Solved": status de L1 preservado quando PuLP
  redefine mdl.status apos setObjective() em L2.
- f0_cenario_insp_grande.json revisado: apenas 2803 com f0=595h em INSP 2A
  (F_max=600h, downtime=4 dias); demais matriculas com f0=0.
- Gerado planejamento_insp_grande.html: Gantt exibe INSP 2A visivelmente;
  20/20 missoes cobertas; CBC Optimal em < 15 s.
- changelog.md e LOG.md atualizados com limitacoes detalhadas para
  contribuidores: escopo validado, bugs de display, riscos numericos do
  big-M com LRT < 5h e comportamento de 2811 ociosa.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

docs/changelog.md

@@ -14,6 +14,31 @@ Formato:
 
 ---
 
+## v0.10 — VTO — 2026-06
+
+### Alterado
+
+- **Set Covering → Set Partitioning (C1):** a restrição de cobertura de missões foi alterada de `Σ_k y_entrada ≤ 1` (Set Covering — missão opcional) para `Σ_k y_entrada = 1` (Set Partitioning — toda missão obrigatória). Isso reflete a premissa operacional de que cada missão deve ser realizada por exatamente uma aeronave, sem possibilidade de missões descobertas. A distinção anterior entre missões "hard" (EVAM) e "opcionais" foi eliminada.
+- **Número padrão de missões sintéticas reduzido de 50 para 20** (`--n-missoes`, `n_evam` de 5 para 4): Set Partitioning é mais restritivo e, com janelas de tempo fixas e restrições de inspeção simultâneas, 50 missões tornavam o MIP difícil de resolver ou inviável. Com 20 missões, a factibilidade é garantida na margem operacional de 4 aeronaves.
+- **Time limit padrão do solver CBC fixado em 120 s** (era ilimitado). O solver agora nunca trava indefinidamente; retorna a melhor solução encontrada dentro do prazo. O CLI mantém `--time-limit` para ajuste.
+- **Correção de display do status do solver:** PuLP redefinía `mdl.status` para "Not Solved" ao reutilizar o modelo em L2 (após `setObjective`). O status de L1 é agora preservado quando L2 reporta 0, evitando exibição enganosa.
+- **Cenário `f0_cenario_insp_grande.json` revisado:** apenas a matrícula 2803 recebe `f0=595h` para INSP 2A (F_max=600h, downtime=4 dias), forçando a inspeção aparecer no Gantt. As demais matrículas partem com `f0=0` (plena disponibilidade), evitando que o problema se torne inviável por múltiplos relógios apertados simultaneamente.
+
+### Adicionado
+
+- `db/processed/planejamento_insp_grande.html`: visualização Gantt + mapa + tabela para o cenário com inspeção de 4 dias (INSP 2A — INSP CHECK 2A, 96 h de solo).
+
+### Limitações conhecidas (para contribuidores)
+
+1. **Escopo validado restrito:** Set Partitioning foi validado apenas para o cenário sintético com 20 missões, seed 42, 4 aeronaves e somente uma matrícula (2803) com LRT apertado. Fora desse envelope, o MIP pode ser infeasible ou ultrapassar o time limit sem solução.
+2. **Missões sintéticas incluem bases fora da Amazônia** (SBBR, SBGL, SBYS etc.) geradas aleatoriamente pelo seed. Para estudos de caso realistas, o gerador deve ser restrito ao conjunto de bases do Esquadrão Arara.
+3. **Folga negativa no relatório:** quando uma aeronave realiza inspeção dentro do horizonte, o campo `folga` exibido (`LRT_ini − horas_celula_total`) pode ser negativo porque não desconta o reset do relógio pós-inspeção. Isso é um bug de display; a restrição `H ≤ F_max` está correta no modelo.
+4. **LRT muito curto (< 5 h) pode gerar instabilidade numérica no big-M:** o cenário foi configurado com LRT_ini=5 h para 2803, que está próximo do limiar onde o big-M deixa de ser eficaz. Valores menores podem permitir que o solver ignore a restrição por tolerância numérica (ε ≈ 1 e-4 do CBC).
+5. **Aeronave 2811 fica ociosa neste cenário:** o solver atribui todas as 20 missões a 3 aeronaves. Isso é matematicamente ótimo, mas pode não ser desejável operacionalmente. Considerar restrição de equilíbrio de carga em versões futuras.
+6. **Status "Not Solved" após L2:** a correção atual usa o status de L1 como proxy. Se L1 retornar apenas uma solução feasível (não ótima, por time limit), o modelo pode ser reportado como "Optimal" quando não é. Monitorar o campo `prio_otima` para validar.
+
+---
+
 ## v0.2 — VTO — 2026-06
 
 ### Adicionado