💻 computer science

Compact SAT and MaxSAT Encodings for Business-to-Business Meeting Scheduling with Idle-Time Balancing

Este artigo introduz codificações compactas de SAT e MaxSAT para o agendamento de reuniões entre empresas que utilizam filtragem de domínio e variáveis compartilhadas para reduzir significativamente a contagem de cláusulas e o uso de memória, ao mesmo tempo em que minimiza os intervalos de tempo de ociosidade dos participantes, superando tanto uma formulação MaxSAT publicada quanto o solver comercial Gurobi em eficiência de resolução.

Autores originais: Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

Publicado 2026-08-04

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é o organizador de festas definitivo para uma convenção de negócios massiva e de alto nível. Você tem centenas de pessoas que precisam ter reuniões individuais, mas todos têm horários diferentes, algumas salas são minúsculas enquanto outras são enormes, e certas reuniões devem acontecer antes que outras possam começar. Seu objetivo não é apenas conseguir uma reunião para todos; é garantir que ninguém fique sentado entediado por muito tempo entre seus compromissos. Este é o quebra-cabeça caótico do "agendamento de reuniões Business-to-Business (B2B)".

Para resolver isso, cientistas da computação usam um tipo especial de jogo lógico chamado SAT (Satisfatibilidade). Pense no SAT como um detetive superinteligente que verifica se um conjunto de regras pode ser verdadeiro ao mesmo tempo. Se você disser ao detetive: "A Reunião A deve ocorrer antes da Reunião B, mas a Reunião B deve ocorrer antes da Reunião A", o detetive dirá instantaneamente: "Impossível!". Mas se as regras forem complicadas, porém possíveis, o detetive encontra um cronograma válido. Outra versão, o MaxSAT, é como um detetive que não apenas encontra um cronograma válido, mas também tenta torná-lo perfeito ao minimizar quanto tempo as pessoas passam esperando. Este trabalho mergulha em como podemos tornar esses detetives lógicos mais rápidos e inteligentes ao organizar esses eventos de negócios complexos.

O Problema: Uma Teia Emaranhada de Reuniões

No mundo das reuniões de negócios, as coisas ficam bagunçadas rapidamente. Você tem uma lista de reuniões, uma lista de intervalos de tempo e uma lista de salas. As regras são rígidas:

Sem Sobreposição: Uma pessoa não pode estar em dois lugares ao mesmo tempo.
Limites de Sala: Uma sala não pode comportar mais reuniões do que sua capacidade.
Precedência: Algumas reuniões devem acontecer antes de outras (como um briefing matinal antes de um workshop à tarde).
O Problema do "Tempo Ocioso": O verdadeiro pesadelo é o "tempo ocioso". Se um participante tem uma reunião às 9:00 e a próxima não é até as 11:00, ele tem duas horas de "tempo ocioso". O objetivo desta pesquisa é equilibrar isso para que ninguém fique esperando por horas enquanto outros esperam apenas alguns minutos. Trata-se de justiça e eficiência.

O Jeito Antigo vs. O Jeito Novo

Os pesquisadores analisaram um método existente (chamado ORG-MAXSAT) que já era muito bom. No entanto, eles notaram que era como tentar organizar uma festa escrevendo cada combinação possível de convidados e horários, mesmo aqueles que eram obviamente impossíveis. Era volumoso, lento e consumia muita memória do computador.

A equipe da VNU University of Engineering and Technology, no Vietnã, decidiu construir uma versão "compacta". Eles introduziram três truques principais para encolher o problema:

O Filtro de "Pré-Verificação" (Filtragem de Domínio): Antes mesmo de pedir ao detetive de computador para resolver o quebra-cabeça, eles adicionaram um filtro inteligente. Este filtro analisa as regras e imediatamente descarta opções impossíveis. Por exemplo, se uma reunião deve acontecer após outra que termina às 14:00, o filtro remove instantaneamente quaisquer intervalos de tempo antes das 14:00 da lista de possibilidades. Isso é como limpar a bagunça de uma mesa antes de tentar encontrar uma caneta específica. Eles provaram que este filtro nunca descarta uma solução válida; ele apenas remove o lixo.
A "Escada Compartilhada" (Codificação de Sufixo Compartilhado Esparso): Ao lidar com as regras de "deve acontecer antes de", o método antigo escrevia uma nota separada para cada par de reuniões. Se você tivesse 100 reuniões, seriam milhares de notas. O novo método percebeu que muitas dessas notas diziam a mesma coisa. Em vez de escrever "Reunião A antes de B", "Reunião A antes de C" e "Reunião A antes de D" separadamente, eles criaram uma "escada" de lógica compartilhada. Eles reutilizam variáveis para situações semelhantes, como usar uma chave mestra para várias portas em vez de fazer uma chave nova para cada fechadura.
A Pontuação de "Justiça" (Equilíbrio do Tempo Ocioso): Em vez de apenas contar quantas pausas as pessoas têm, eles criaram uma nova maneira de medir o "tempo ocioso". Eles olharam para o tempo entre a primeira reunião de uma pessoa e sua última reunião. Se alguém tem reuniões às 9:00 e às 11:00, seu "intervalo" é de duas horas. Se a pessoa tivesse apenas uma reunião, ela teria zero tempo ocioso. O objetivo é garantir que a diferença entre o tempo ocioso da pessoa mais ocupada e o da pessoa menos ocupada seja a menor possível.

O Que Eles Descobriram

Os pesquisadores testaram seu novo método "Compacto" contra o método antigo e contra alguns softwares comerciais muito poderosos (como Gurobi e CPLEX) em 126 casos de teste oficiais e 100 casos extras de "teste de estresse" com ainda mais reuniões.

Aqui estão os resultados, que são bastante impressionantes:

Tamanho Menor: O novo método reduziu o número de "cláusulas" lógicas (as regras que o computador precisa verificar) em 40,3% em média.
Menos Memória: Ele usou 55,9% menos memória de pico. Imagine precisar de metade da RAM para resolver o mesmo quebra-cabeça.
Velocidade Maior: O tempo total para resolver os problemas caiu 14,0%.
O Poder da Filtragem: O uso apenas do filtro de "Pré-Verificação" cortou o número de variáveis em 24,1% e as regras em 16,2%.
O Poder do Compartilhamento: O truque da "Escada Compartilhada" reduziu em mais 0,5% a 5,5% o número de regras, dependendo de quão lotado estava o cronograma.

O Veredito

A parte mais emocionante é que seus novos métodos compactos de SAT e MaxSAT foram capazes de resolver todos os 126 casos de teste oficiais. Melhor ainda, eles fizeram isso mais rápido do que o principal solver comercial, o Gurobi, em termos de tempo mediano. Enquanto outras ferramentas comerciais (como CPLEX e CP Optimizer) tiveram dificuldade para resolver todos os casos dentro do limite de tempo, a nova abordagem baseada em SAT lidou com todos eles.

O artigo não afirma ter resolvido os problemas de agendamento do universo para sempre, mas certamente mostrou que, ao limpar as regras e compartilhar o trabalho de forma mais inteligente, podemos tornar os computadores muito melhores em organizar nossas vidas ocupadas. Eles transformam um nó enorme e emaranhado de reuniões em um cronograma organizado e equilibrado, onde todos têm sua parte justa de tempo e ninguém fica esperando no corredor por muito tempo.

Resumo Técnico: Codificações Compactas de SAT e MaxSAT para Agendamento de Reuniões B2B com Balanceamento de Tempo de Inatividade

Definição do Problema

O artigo aborda o agendamento de reuniões Business-to-Business (B2B), um problema de otimização combinatória onde reuniões pareadas solicitadas devem ser atribuídas a slots temporais e locais específicos. O agendamento deve satisfazer vários critérios:

Não sobreposição de Participantes: Um participante não pode comparecer a duas reuniões simultaneamente.
Capacidade de Local: O número de reuniões em qualquer slot temporal não pode exceder o número de locais disponíveis ( $K$ ).
Disponibilidade e Restrições: As reuniões devem ocorrer dentro de sessões solicitadas, slots fixos ou slots proibidos.
Precedência: Arcos direcionados $(i, j)$ impõem que a reunião $i$ deve ocorrer antes da reunião $j$ .

O objetivo proposto neste trabalho difere de formulações anteriores (que frequentemente minimizam "grupos de intervalos" ou limitam a disparidade na contagem de intervalos). Em vez disso, este estudo minimiza o intervalo do total de slots de inatividade interna ( $\Delta I$ ) entre participantes que possuem pelo menos duas reuniões. Os slots de inatividade interna são definidos como o tempo não ocupado estritamente entre a primeira e a última reunião atribuída a um participante. Esta métrica distingue entre interrupções curtas e esperas longas, visando um equilíbrio na distribuição de carga semelhante ao Problema do Currículo Acadêmico Balanceado (BACP). Uma medida de inatividade agregada ( $I_\Sigma$ ) também é relatada como uma métrica complementar.

Metodologia

Os autores propõem uma codificação compacta de SAT (Satisfatibilidade Booleana) e MaxSAT que integra três principais melhorias de modelagem sobre as formulações publicadas existentes:

Filtragem de Domínio Preservadora de Solução (Pré-processamento):
Antes de gerar a Forma Normal Conjuntiva (CNF), os autores aplicam um algoritmo de pré-processamento (Algoritmo 1) que remove atribuições não suportadas. Isso integra:
- Filtros de limite de extremidade: Propagação de restrições de precedência ao longo de caminhos (usando arcos diretos ou fechamento transitivo).
- Correspondência por participante: Remoção de atribuições que não podem fazer parte de um cronograma livre de conflitos para um participante específico.
- Propagação de slot saturado: Eliminação de slots onde a capacidade já foi totalmente utilizada por atribuições forçadas.
- Alegação: Este processo preserva todos os cronogramas viáveis enquanto reduz o tamanho do domínio, reduzindo, assim, o número de variáveis e cláusulas.
Codificação de Precedência de Sufixo Compartilhado Esparso (SPARSESUFFIX):
Em vez de codificar relações de precedência usando cláusulas pareadas (que podem ser quadráticas em relação ao tamanho do domínio), os autores introduzem uma codificação esparsa.
- Ela materializa apenas os "pontos de corte" distintos no domínio do predecessor onde a restrição se torna ativa.
- Ela reutiliza variáveis auxiliares para cortes iguais entre diferentes relações.
- Este método é provado como equivalente às cláusulas pareadas, mas reduz significativamente a contagem de cláusulas, particularmente quando combinado com a redução de domínio.
Objetivo de Inatividade Baseado em Intervalo:
O artigo introduz uma codificação exata para minimizar o intervalo dos slots de inatividade interna ( $\Delta I$ ).
- Ele deriva os primeiros e últimos slots ocupados para cada participante.
- Utiliza um número linear de variáveis auxiliares para calcular a diferença entre o máximo e o mínimo de contagens de inatividade entre todos os participantes relevantes.

O estudo avalia esses componentes contra uma formulação base ORG-MAXSAT (uma adaptação de um modelo publicado) e solvers comerciais (Gurobi, CPLEX, CP Optimizer). A avaliação abrange 126 instâncias de benchmark oficiais e 100 instâncias derivadas de "Estresse" com densidades de precedência variadas.

Principais Contribuições

O artigo identifica três contribções específicas:

Procedimento de Pré-processamento: Um filtro integrado que remove atribuições não suportadas antes da geração da CNF. A Proposição 1 prova que isso preserva a viabilidade, e os resultados empíricos mostram que reduz as variáveis de atribuição em 24,1% e as cláusulas em 16,2%.
Representação de Sufixo Compartilhado Esparso: Uma codificação exata (SPARSESUFFIX) que materializa apenas os pontos de corte necessários no domínio do predecessor. A Proposição 3 prova sua equivalência às cláusulas pareadas. O estudo demonstra que, embora a redução de domínio diminua a contagem de variáveis, o compartilhamento de sufixo reduz independentemente a contagem de cláusulas.
Objetivo Específico de B2B: Um objetivo de intervalo de tempo de inatividade que mede a disparidade nos tempos de espera interna, codificado com um número linear de variáveis auxiliares.

Resultados Experimentais

Os experimentos foram conduzidos em uma máquina de 4 núcleos com um limite de tempo de 7.200 segundos. As principais descobertas incluem:

Tamanho da Fórmula e Memória: Comparado à base ORG-MAXSAT adaptada, a codificação compacta proposta reduziu a contagem mediana de cláusulas em 40,3% e o uso de pico de memória mediana em 55,9%.
Impacto da Redução de Domínio: A filtragem de domínio sozinha reduziu as variáveis de atribuição em 24,1% e as cláusulas em 16,2%, contribuindo com a maior parte da redução do tamanho da fórmula.
Codificação de Precedência: A codificação SPARSESUFFIX reduziu a contagem mediana de cláusulas em 0,5%–1,0% nas instâncias de precedência oficiais e até 5,5% nas instâncias derivadas de maior densidade (quando combinada com o fechamento transitivo).
Desempenho do Solver:
- Todos os três métodos propostos de SAT/MaxSAT (Incremental SAT, Non-Incremental SAT e UWrMaxSAT) resolveram todas as 126 instâncias oficiais.
- Comparado ao Guroi (o único solver comercial que resolveu todas as instâncias), os métodos SAT/MaxSAT propostos alcançaram tempos totais medianos menores.
- O Incremental SAT alcançou o menor tempo mediano (0,227s) entre os métodos completos.
- O CP Optimizer teve o menor tempo mediano (0,110s), mas falhou em resolver 11 instâncias dentro do limite de tempo.

Significância e Alegações

O artigo afirma que a codificação compacta proposta oferece uma melhoria significativa de eficiência sobre as formulações Booleanas existentes para o agendamento de reuniões B2B. Ao separar a filtragem de domínio da representação de precedência, os autores demonstram que a redução de domínio é o principal motor para reduzir o tamanho da fórmula, enquanto a codificação de sufixo compartilhado esparso fornece uma redução adicional de cláusulas independente do conjunto de relações.

O estudo assegura que o novo objetivo de intervalo de tempo de inatividade fornece uma medida mais matizada da qualidade do cronograma do que as métricas anteriores de "grupos de intervalos", distinguindo entre interrupções curtas e esperas longas. Além disso, os resultados indicam que os solvers modernos de SAT e MaxSAT, quando equipados com estas codificações compactas, podem superar os principais solvers de MIP e CP em termos de tempo de solução mediana para esta classe específica de problemas, resolvendo todos os benchmarks onde alguns solvers comerciais excederam o tempo limite.

Os autores mantêm-se modestos quanto ao trabalho futuro, observando que o estudo atual foca em tempo de execução única e que pesquisas futuras poderiam explorar execuções de tempo repetidas e objetivos lexicográficos (minimizando $\Delta I$ antes de $I_\Sigma$ ).