10 · Perfis, orçamentos e custo

Quais partes do motor rodam não é uma configuração de desempenho: isso decide o que uma resposta pode afirmar. Uma refutação que o solver SAT afirmou não pode trazer um certificado autocontido; um reparo tirado de uma expansão que ninguém construiu não pode afirmar ser o menos disruptivo. Por isso, as configurações do motor vêm em perfis nomeados, cada um uma combinação que sustenta um tipo de afirmação, escolhido a cada requisição com profile.

Os cinco perfis

Perfil	O que ele lhe dá	Quando usá-lo
fast	um veredito em cerca de um quarto de segundo: uma testemunha SAT conferida, ou um UNSAT que o solver SAT afirma. Sem certificado e sem reparo	o padrão para uma pergunta, e para toda linha de uma tabela que deve ficar verde
patch	um reparo e um certificado, da expansão algébrica, com o solver SAT desligado	um buraco que o fast encontrou, ou um UNSAT para o qual você precisa de certificado
proof	o perfil de portão: o solver SAT decide, a expansão repara o que ele deixa, com o certificado completo. Uma obrigação quebrada é perguntada de novo com o solver SAT desligado, para que o seu reparo e o seu veredito venham de uma única execução	um portão que precisa produzir tanto um veredito quanto um reparo
enumerate	toda situação que quebra a política, e uma prova de que não há outra	revisão e diagnóstico; lento por concepção, e não para um portão
forest	o padrão das random forests: o solver SAT decide, em escala de produção, e o seu UNSAT é admitido	random forests (capítulo 14)

Cada chave que cada perfil define, gerada a partir dos perfis que o serviço roda:

Chave	fast	patch	proof	enumerate	forest
enable_phase0	true	false	true	false	true
oracle_unsat_admissible	true	false	true	false	true
certificate_detail	none	full	full	full	none
enable_phase3	false	false	false	true	true
enable_phase4	false	true	false	true	true
max_roots	1	1	1	0	1
report_phase2_trace	false	false	false	false	false
report_minimal_contexts	false	false	false	false	false
verbose	true	true	true	true	true
wall_budget_seconds	60.0	300.0	900.0	900.0	3600.0
contradiction_budget_seconds	60.0	120.0	180.0	180.0	60.0
Procura um reparo	não	sim	sim	sim	não

E por que cada um está configurado assim, nas palavras do serviço:

Perfil	Por quê
fast	o formato que só decide, e responde em cerca de um quarto de segundo; um minuto é generoso e não há busca de reparo a financiar
patch	a execução de reparo: a busca é o objetivo, então a maior parte do orçamento é dela
proof	o perfil de gate: a Fase 0 decide, a Fase 2 corrige o que ela deixa, e sem fechamento -- segundos em vez de minutos, que é a diferença entre um gate e uma rodada noturna
enumerate	o desfecho por fechamento e uma contagem ilimitada de raízes: todo contexto que quebra a política e uma prova de que não há outro. Lento por definição, e para diagnóstico em vez de para um gate
forest	uma floresta implantada é retreinada em vez de corrigida, então não há reparo a buscar e todo o orçamento é da própria propriedade

O protocolo de duas execuções

O caminho mais barato até uma resposta útil são duas execuções, e a segunda só quando é necessária:

1. Decida com fast. Cerca de um quarto de segundo. UNSAT e nenhum certificado necessário: pare, e o registro diz oracle_dependent: true, para que a afirmação mais fraca fique registrada em vez de subentendida.
2. SAT, ou STALL, ou UNSAT com certificado necessário: pergunte de novo com patch. O reparo precisa da expansão algébrica, que o fast não constrói, e um certificado que qualquer pessoa possa reproduzir também.

O proof faz as duas execuções por você, e só paga pela segunda onde a primeira encontrou um buraco. Uma tabela de propriedades faz o mesmo linha a linha: decide cada linha com o solver SAT e resolve uma linha uma segunda vez só onde a sua resposta deve o que o solver SAT não consegue construir, um reparo ou um certificado que a linha pede (capítulo 11).

Mudando uma chave: config

Um perfil é uma base, não uma trava. config substitui chaves isoladas por cima dele, nessa ordem, então uma requisição que muda um orçamento deixa de pé as fases que o perfil escolheu. Uma chave que o serviço não conhece é recusada com a lista das que ele aceita; um valor fora dos limites de uma chave é ajustado ao limite, ou recusado onde o limite representa outra coisa. O run.config_effective do job é o que rodou, e run.clamped_by diz o que um limite mudou.

As chaves, geradas a partir do registro do serviço:

Chave	Tipo	Significado	Valores
enable_phase0	bool	executa o oráculo CDCL limitado
oracle_unsat_admissible	bool	permitir que uma refutação afirmada por oráculo encerre a execução; nenhum certificado que dependa de uma é autocontido
enable_phase1_5	bool	executar a expansão por reprodução sexuada
enable_phase2	bool	executar o loop de expansão evolutiva
enable_phase3	bool	executar a fase final (endgame) do fechamento por base de borda
enable_phase4	bool	executa condensação e busca exaustiva sobre o que o fechamento deixou indecidido
max_roots	int	limite superior para as raízes que o fechamento retorna; 0 é ilimitado	≥ 0
max_quotient_dimension	int	teto absoluto da base do quociente; 0 usa a proteção escalonada	≥ 0
min_quotient_dimension	int	piso sob a guarda do quociente escalado; 0 significa sem piso	≥ 0
max_quotient_dimension_scalar	double	fração do espaço ambiente de grau 2 que a base do quociente pode alcançar antes que o fechamento desista	≥ 0.0
max_pivot_row_width	int	termos que uma linha pivô armazenada da eliminação da varredura de fantasmas pode conter. Linhas mais largas que isso são descartadas por inteiro em vez de armazenadas, o que limita o custo residente da fase ao preço de um quociente maior a filtrar; 0 remove o limite e deixa a eliminação crescer livremente	≥ 0
phase3_admission	string	estratégia de admissão de fronteira para o fechamento	Greedy, Stratified
wall_budget_seconds	double	orçamento de tempo de relógio para a resolução; para em um limite de loop com a cascata intacta, de modo que uma execução interrompida é um fechamento parcial válido, e não um fechamento corrompido. 0 significa sem prazo, e o serviço não concede um: um orçamento abaixo do piso é elevado até ele	≥ 1.0; ≤ 21600.0
sds_target_threshold	int	pontuação de disrupção igual ou inferior à qual a busca seat-belt aceita um candidato e para de varrer	≥ 0
contradiction_budget_seconds	double	orçamento de tempo de relógio separado para a busca de cinto de segurança, que é executada após a resolução. 0 significa sem prazo, e não sem busca, e o serviço não concede ausência de prazo: use enable_contradiction_search para desativar a busca	≥ 1.0; ≤ 3600.0
enable_contradiction_search	bool	após um veredito diferente de UNSAT, executa a busca de cinto de segurança. Desligado significa que nenhum candidato é proposto, em vez de um pior
verbose	bool	verbosidade do console da execução
enable_operation_tracking	bool	registra a proveniência de cada inserção que aumenta o posto, sem a qual um certificado completo não pode ser reconstruído
report_phase2_trace	bool	publicar no payload o rastreamento de ranking por geração
report_minimal_contexts	bool	reservado para a redução de contexto mínimo, que não existe
certificate_detail	string	quanto da refutação registrar e, portanto, quanta contabilidade a resolução paga	full, core, none

certificate_detail decide quanto da refutação é registrado: full registra a derivação inteira; core primeiro reduz o sistema ao menor conjunto das suas equações que ainda refuta, e certifica esse, o que mantém pequeno um certificado num sistema grande; none não registra certificado.

Os orçamentos

Uma execução tem dois relógios:

• wall_budget_seconds limita a resolução inteira. Uma execução que ele interrompe termina como STALL, com verdict.budget_exhausted: true e a causa budget-expired, e vale a pena rodar de novo com um orçamento maior. O wall_budget_ceiling_seconds da sua chave o limita: uma requisição acima do teto é reduzida a ele, não recusada, e run.clamped_by diz isso. Acima de 900 segundos é preciso a permissão long_solve.
• contradiction_budget_seconds limita a busca de um reparo. Uma busca que ele interrompe devolve o melhor reparo encontrado até ali, ainda provado fechar o buraco; só o menos disruptivo é retirado, e corrective_action.search_truncated é true.

Zero significa sem limite nos dois, o que o teto da sua chave ainda limita. Um orçamento esgotado nunca é uma falha silenciosa: uma execução interrompida diz que foi interrompida, e o que ela devolve continua correto.

Contando todos os caminhos: enumerate

Uma testemunha responde existe um buraco. Sob o perfil enumerate, com enumerate definido na requisição, o motor responde quantos, e são todos: ele fecha o sistema por completo, conta as situações que quebram a política e prova que a contagem está completa, porque a contagem é uma dimensão que ele calculou, e não o ponto em que uma busca parou de encontrar coisas. A resposta traz a contagem e se ela está completa; uma contagem que o motor teve de interromper vale como um limite inferior. A forma mais forte é zero, provado: nenhuma situação quebra a política, e não sobra nenhuma para procurar.

Este é um instrumento de revisão. Nenhum perfil de portão o roda, e nenhum veredito precisa dele: um veredito e um certificado assinado são alcançados sem ele. Ele é lento por concepção, e enumerate é recusado junto com fast ou patch, que não rodam o fechamento de que ele precisa.

O que o frat_proof custa

Uma prova FRAT de uma refutação da Fase 0 (capítulo 7) não custa nada a menos que você a peça. Pedida, ela é uma segunda resolução de uma refutação a que o solver SAT já chegou, com o registro de prova ligado. Nas refutações de referência, uma execução foi de uma mediana de 30 ms para 44 ms, o CNF teve de 0,2 a 5,5 KB, o registro FRAT de 1,3 a 49 KB, e o frat-rs o conferiu em cerca de 30 ms. Isso não é um limite garantido: em alguns sistemas a prova é muito mais difícil que a resolução, e uma prova que o orçamento da execução interrompe não é escrita, o que deixa o certificado como o do oráculo, exatamente como sem a opção. Os arquivos guardados contam contra o max_proof_bytes da sua chave, e uma prova que o excederia é descartada, nunca o veredito (capítulo 16).

O que uma resolução custa

Cada job terminado escreve um registro de uso, e os segundos de resolução que ele usou contam contra o monthly_solve_seconds da sua chave (capítulo 16):

Como o job terminou	Contado
teve sucesso, seja qual for o veredito, SAT e STALL incluídos	sim
falhou por uma causa sua: uma política que não compila, um digest que não confere, um orçamento que você definiu	sim
falhou por uma causa nossa: um worker perdido, um erro interno	não
falhou por uma causa que nada classificou	não
cancelado	sim, pelos segundos de fato usados
recusado antes de qualquer coisa rodar	nada é registrado

Um impasse é contado porque usou o processamento e ainda devolve um reparo: é uma resposta entregue. A cota é conferida quando um job é enviado, e não de novo enquanto ele roda, então uma execução que começou dentro da cota termina.

No plano gratuito, um job roda só a Fase 0, que é o perfil fast; um job que pede mais, um perfil patch ou proof ou uma fase posterior, roda por completo até o número mensal de resoluções completas do plano (capítulo 40).

Os limites

• O que um perfil não roda, a sua resposta não pode afirmar: o fast não constrói certificado nem reparo, e o seu UNSAT é uma afirmação do solver SAT.
• Uma execução interrompida por orçamento é uma resposta parcial correta, e diz isso; um orçamento maior pode dar uma mais forte.
• A contagem de uma enumeração só está completa onde a resposta diz que está.
• Os números do FRAT acima são medições em refutações de referência, não um limite garantido para as suas.