Tese de graduação sobre programação baseada em restrições

Resumo

O simulador verifica repetidamente muitas condições à medida que os eventos possíveis aumentam. Então, se for possível julgar a partir do progresso que 'esta condição nunca mais será satisfeita', não seria seguro parar essa verificação? Com base na direção da mudança dos valores, foi projetado e implementado um método para remover condições desnecessárias da busca em execução, voltado para a linguagem de modelagem de sistemas híbridos HydLa.

No modelo de avaliação, conseguimos reduzir o tempo de execução para cerca de metade do convencional, sem alterar os resultados da simulação. O importante não é que todos os cálculos tenham se tornado uniformemente mais rápidos. O que fizemos foi reduzir o próprio número de possibilidades a serem consideradas, utilizando a estrutura do problema.

A maneira de pensar sobre programação baseada em restrições aprendida neste estudo se tornou a base do Minha filosofia de design atual. Em vez de especificar diretamente cada resultado, a abordagem é definir regras, prioridades e limites, e derivar soluções que se realizem dentro desses parâmetros.

Questão — Quanto mais aumentam as possibilidades, mais lenta se torna a computação

HydLa é uma linguagem para descrever "sistemas híbridos", que combinam mudanças contínuas e eventos discretos, como restrições matemáticas e lógicas. Mesmo sem escrever toda a sequência de procedimentos, é possível simular comportamentos que atendam às condições declarando o que deve ser estabelecido.

Por outro lado, em modelos onde muitas regras se tornam válidas dependendo das condições, o simulador verifica repetidamente uma grande quantidade de candidatos. Como continuam a permanecer como candidatos mesmo condições que já foram ultrapassadas e que não serão satisfeitas no futuro, quanto maior o modelo, mais cálculos desnecessários se acumulam.

Tema — um sistema que mistura contínuo e discreto

Uma bola quicando é um exemplo claro de um sistema híbrido. No ar, sua posição e velocidade mudam continuamente, e no instante em que atinge o chão, ocorre um evento discreto de ricochete. Termostatos, carros e robôs também possuem esses dois tipos de mudança internamente, mesmo que em escalas diferentes.

Para a avaliação, utilizou-se um modelo no qual uma bola movendo-se horizontalmente rebate em uma superfície dividida em vários setores. Para cada setor da superfície, existe uma regra condicional do tipo 'se a bola chegar a esta área, ela rebate'. Ao aumentar o número de setores, aumenta-se o que pode ser representado, mas também aumentam as condições que o simulador precisa verificar.

Gargalo — o número de condições aumenta a complexidade computacional

As regras que só se tornam válidas quando certas condições são atendidas são chamadas de "restrições com guarda". No modelo de avaliação, a regra de rebote de um determinado setor só se torna válida quando a bola atinge o chão e sua posição horizontal está dentro desse setor específico.

Quando o número de parcelas é aumentado de 10 para 200, o simulador convencional ficou aproximadamente mais lento proporcional ao quadrado do número de parcelas. Em modelos de grande escala, o mesmo problema se torna maior devido ao aumento de objetos, áreas de contato e eventos possíveis.

Investigação — Onde estavam 96% do tempo de processamento

Ao medir o tempo de processamento, no modelo com 100 seções, 96% do total foi utilizado em FindMinTime. Este é o processamento de procurar, entre os candidatos, o 'próximo evento mais rápido' a ocorrer. Assim, todas as condições de guarda estavam sendo avaliadas repetidamente.

Os locais que precisam ser melhorados ficaram claros. Não é necessário refazer todo o método de cálculo; basta reduzir de forma segura os candidatos a serem passados para FindMinTime. O objetivo foi alterar apenas as possibilidades que não precisam ser verificadas, sem mudar os resultados da simulação.

Abordagem — remover com segurança condições que nunca mais se concretizarão

Gostaria que você imaginasse uma bola descendo uma escada quicando. Se a bola passa por um degrau e continua avançando, esse degrau não pode mais afetar a bola. Quem olha o gráfico ignora imediatamente os degraus que estão atrás da bola. O algoritmo original continuava verificando cada um deles, um por um.

A parte difícil é mostrar que o guarda removido não será necessário mais tarde. Se você removê-lo apenas porque é falso agora, quando ele se tornar verdadeiro novamente, poderá silenciosamente retornar um resultado incorreto. Portanto, o método proposto usa a monotonicidade — a questão é se é possível garantir que uma variável continuará a aumentar ou a diminuir durante um determinado intervalo de tempo.

Quando a direção da mudança não muda

A primeira abordagem é aplicável quando a variável se move em apenas uma direção durante toda a simulação. Em um modelo com a superfície dividida, a posição horizontal da bola sempre aumenta. Uma vez que atravessa uma seção, as condições dessa seção nunca mais são satisfeitas. Essa propriedade pode ser verificada antes da simulação usando técnicas de verificação de modelo, permitindo que os guardas que se tornam desnecessários à medida que a execução avança sejam removidos com segurança.

Quando a direção da mudança muda no meio do caminho

Muitos sistemas reais não se movem em uma única direção indefinidamente. As variáveis podem aumentar, mudar de direção e então diminuir. Assim, o artigo apresentou uma segunda abordagem. Primeiro, supõe-se uma direção, monitora-se essa suposição com uma asserção e, no ponto em que a direção muda, o processo de redução é reiniciado. A proteção removida para um intervalo monótono é restaurada quando o próximo intervalo começa.

Resultado — Tempo de execução do modelo de avaliação reduzido pela metade

Implementou-se uma abordagem para lidar com monotonicidade uniforme e avaliou-se em modelos com superfícies divididas. Tanto o algoritmo original quanto o método proposto apresentam aumento do tempo necessário à medida que o número de seções cresce. No entanto, o método proposto teve consistentemente menos carga de trabalho. Comparando as curvas ajustadas, o coeficiente de maior ordem caiu de 1,1463 para 0,6083, e neste benchmark o tempo total de simulação foi reduzido aproximadamente pela metade.

Isto não é uma afirmação de que todos os modelos HydLa serão duas vezes mais rápidos. O que está sendo mostrado é onde esse método funciona — modelos que têm muitos alvos com guardas, nos quais a direção da mudança pode ser provada, e durante a execução os guardas se tornam permanentemente irrelevantes.

Perspectiva obtida a partir desta pesquisa

O que foi feito neste estudo não foi acelerar um pouco cada cálculo individual. O objetivo foi usar o que se sabe sobre o comportamento do sistema para reduzir o conjunto de possibilidades a ser considerado. A ideia de restringir o espaço de busca sem alterar o resultado é a força da programação baseada em restrições.

O que foi implementado e avaliado é o caso em que a variável continua a se mover em uma direção. Quando a direção da mudança se altera no meio do caminho, a análise foi limitada ao projeto, e a avaliação permaneceu como uma questão futura. Também há espaço para usar propriedades além da monotonicidade e encontrar restrições desnecessárias adicionais.

O fato de eu atualmente tentar projetar as condições e limites que a IA pode explorar, em vez de projetar diretamente a saída da IA, também está ligado a essa experiência. Ao lidar com resultados complexos, é tão importante definir o que não precisa ser considerado quanto definir o que deve ser calculado.