Muitos problemas difíceis do LeetCode são problemas fáceis de programação com restrições

• Até os problemas difíceis do LeetCode podem ser resolvidos com muito mais facilidade usando solvers de restrições
• Em vez de programação dinâmica complexa ou algoritmos próprios, é possível usar solvers de restrições como o MiniZinc para resolver problemas de otimização matemática de forma simples
• Linguagens de programação tradicionais têm dificuldade para expressar esse tipo de problema de otimização matemática, o que destaca a força da abordagem baseada em restrições
• Mesmo quando surgem casos de exceção ou restrições adicionais, a mudança no modelo dentro de um solver de restrições é mínima
• A complexidade em tempo de execução pode ser pior do que a de um algoritmo otimizado escrito à mão, mas há muitas vantagens em flexibilidade e produtividade de desenvolvimento

---

Problemas do LeetCode resolvidos com um solver de restrições

Escolhendo a ferramenta certa

• O autor recebeu o problema do "troco com moedas" em sua primeira entrevista após se formar na universidade

  • Dadas denominações de moedas, o objetivo era encontrar a quantidade mínima de moedas necessária para devolver um valor específico
  • Ele usou um algoritmo guloso simples, mas isso não garantia a solução ótima em todos os casos
  • A resposta correta era programação dinâmica, mas ele não conseguiu implementá-la e foi reprovado na entrevista

• Mas, em vez de implementar o algoritmo manualmente, é possível resolver isso com muita facilidade usando um solver de restrições como o MiniZinc

  • Exemplo de código:

    int: total;
    array[int] of int: values = [10, 9, 1];
    array[index_set(values)] of var 0..: coins;
    
    constraint sum (c in index_set(coins)) (coins[c] * values[c]) == total;
    solve minimize sum(coins);
    

  • É possível testar diretamente o exemplo no MiniZinc online

  • O solver encontra progressivamente a solução ótima

Vários problemas de otimização/satisfação

• Problemas de otimização matemática comuns em plataformas como o LeetCode, com maximização/minimização de função objetivo e várias restrições,
  costumam ser difíceis de resolver em linguagens de programação por exigirem implementação de baixo nível, mas se encaixam bem em solvers de restrições
• Por exemplo, vários problemas com as características abaixo entram nessa categoria

Exemplo 1: problema do lucro máximo com ações

• "Dada uma lista de preços de ações, encontre o lucro máximo que pode ser obtido comprando uma vez e vendendo depois"
  • Tradicionalmente, isso exige brute force O(n²) ou um algoritmo ótimo O(n)
  • No MiniZinc, pode ser definido de forma simples como o problema de restrições abaixo

    array[int] of int: prices = [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5, 8];
    var int: buy;
    var int: sell;
    var int: profit = prices[sell] - prices[buy];
    
    constraint sell > buy;
    constraint profit > 0;
    solve maximize profit;
    

Exemplo 2: chegar a 0 somando/subtraindo números específicos (problema de satisfação)

• "É possível chegar a 0 somando ou subtraindo três números de uma lista?"
  • Basta encontrar uma solução satisfatória, não um valor ótimo
  • Em um solver de restrições, isso pode ser expresso assim

    include "globals.mzn";
    array[int] of int: numbers = [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5, 8];
    array[index_set(numbers)] of var {0, -1, 1}: choices;
    
    constraint sum(n in index_set(numbers)) (numbers[n] * choices[n]) = 0;
    constraint count(choices, -1) + count(choices, 1) = 3;
    solve satisfy;
    

Exemplo 3: maior área retangular em um histograma

• "Dado um histograma com a altura de cada barra, encontre a maior área retangular possível"
  • Tradicionalmente, isso exige algoritmos complexos e gerenciamento de vários estados
  • Com restrições apenas, é possível descrever a solução de forma concisa

    array[int] of int: numbers = [2,1,5,6,2,3];
    
    var 1..length(numbers): x; 
    var 1..length(numbers): dx;
    var 1..: y;
    
    constraint x + dx <= length(numbers);
    constraint forall (i in x..(x+dx)) (y <= numbers[i]);
    
    var int: area = (dx+1)*y;
    solve maximize area;
    
    output ["(\(x)->\(x+dx))*\(y) = \(area)"]
    

A abordagem com solver de restrições é melhor?

• Em uma entrevista, há fragilidades em perguntas sobre complexidade de tempo e afins

  • Solvers de restrições têm tempo de execução difícil de prever e normalmente são mais lentos do que algoritmos ótimos sob medida
  • Ainda assim, costumam ser melhores do que um algoritmo mal implementado, e a maioria dos programadores não consegue escrever manualmente a solução ótima toda vez

• A principal vantagem real é a flexibilidade para adicionar novas restrições

  • Por exemplo, no caso das ações, mudar de uma única compra e venda para várias operações faz a complexidade algorítmica disparar
  • Em um modelo de restrições no MiniZinc, isso pode ser acomodado com pequenas mudanças no código, mesmo com requisitos muito mais complexos

    include "globals.mzn";
    int: max_sales = 3;
    int: max_hold = 2;
    array[int] of int: prices = [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5, 8];
    array [1..max_sales] of var int: buy;
    array [1..max_sales] of var int: sell;
    array [index_set(prices)] of var 0..max_hold: stocks_held;
    var int: profit = sum(s in 1..max_sales) (prices[sell[s]] - prices[buy[s]]);
    
    constraint forall (s in 1..max_sales) (sell[s] > buy[s]);
    constraint profit > 0;
    
    constraint forall(i in index_set(prices)) (stocks_held[i] = (count(s in 1..max_sales) (buy[s] <= i) - count(s in 1..max_sales) (sell[s] <= i)));
    constraint alldifferent(buy ++ sell);
    solve maximize profit;
    
    output ["buy at \(buy)\n", "sell at \(sell)\n", "for \(profit)"];
    

• Exemplos online de problemas com restrições costumam se concentrar em quebra-cabeças como Sudoku, mas eles podem ser usados de forma mais interessante e prática em problemas com lógica de negócio ou requisitos de otimização

  • Por exemplo, também há grande potencial para aplicar técnicas avançadas de otimização como symmetry breaking

Encerramento e referências

• Este texto faz parte da newsletter semanal do autor, que trata de história do software, métodos formais, novas tecnologias e teoria da engenharia de software
• Se tiver interesse, você pode assinar ou consultar o site principal do autor
• O novo livro do autor, "Logic for Programmers", também está sendo publicado