💻 computer science

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

Este artículo presenta codificaciones compactas de SAT y MaxSAT para la programación de reuniones entre empresas que utilizan el filtrado de dominios y variables compartidas para reducir significativamente el recuento de cláusulas y el uso de memoria, al tiempo que minimizan los rangos de tiempo de inactividad de los participantes, superando tanto una formulación de MaxSAT publicada como al solver comercial Gurobi en eficiencia de resolución.

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

Publicado 2026-08-04

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

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

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que eres el organizador de eventos definitivo para una enorme y de alto nivel convención de negocios. Tienes cientos de personas que necesitan tener reuniones uno a uno, pero todos tienen horarios diferentes, algunas salas son diminutas mientras que otras son enormes, y ciertas reuniones deben ocurrir antes de que otras puedan comenzar. Tu objetivo no es solo lograr que todos tengan una reunión; es asegurarte de que nadie se quede sentado aburrido por demasiado tiempo entre sus citas. Este es el caótico rompecabezas de la "programación de reuniones de Negocio a Negocio (B2B)".

Para resolver esto, los científicos de la computación utilizan un tipo especial de juego lógico llamado SAT (Satisfacibilidad). Piensa en el SAT como un detective superinteligente que comprueba si un conjunto de reglas puede ser verdadero al mismo tiempo. Si le dices al detective: "La Reunión A debe ser antes de la Reunión B, pero la Reunión B debe ser antes de la Reunión A", el detective dice instantáneamente: "¡Imposible!". Pero si las reglas son complicadas pero posibles, el detective encuentra un horario válido. Otra versión, MaxSAT, es como un detective que no solo encuentra un horario válido, sino que también intenta hacerlo perfecto minimizando cuánto tiempo pasan las personas esperando. Este trabajo profundiza en cómo podemos hacer que estos detectives lógicos sean más rápidos y astutos al organizar estos complejos eventos de negocios.

El Problema: Una Red Enredada de Reuniones

En el mundo de las reuniones de negocios, las cosas se complican rápido. Tienes una lista de reuniones, una lista de franjas horarias y una lista de salas. Las reglas son estrictas:

Sin Solapamiento: Una persona no puede estar en dos lugares a la vez.
Límites de Sala: Una sala no puede albergar más reuniones de su capacidad.
Precedencia: Algunas reuniones deben ocurrir antes que otras (como una sesión informativa matutina antes de un taller por la tarde).
El Problema del "Tiempo de Inactividad": El verdadero dolor de cabeza es el "tiempo de inactividad" (idle time). Si un participante tiene una reunión a las 9:00 AM y su siguiente reunión no es hasta las 11:00 AM, tiene dos horas de "tiempo de inactividad". El objetivo de esta investigación es equilibrar esto para que nadie esté esperando durante horas mientras otros solo esperan unos minutos. Se trata de equidad y eficiencia.

La Vieja Forma vs. El Nuevo Camino

Los investigadores analizaron un método existente (llamado ORG-MAXSAT) que ya era bastante bueno. Sin embargo, notaron que era como intentar organizar una fiesta escribiendo cada una de las combinaciones posibles de invitados y horarios, incluso aquellas que eran obviamente imposibles. Era voluminoso, lento y consumía mucha memoria de la computadora.

El equipo de la Universidad de Ingeniería y Tecnología VNU en Vietnam decidió construir una versión "compacta". Introdujeron tres trucos principales para encoger el problema:

El Filtro de "Pre-Chequeo" (Filtrado de Dominio): Antes de siquiera pedirle al detective de la computadora que resuelva el rompecabezas, añadieron un filtro inteligente. Este filtro observa las reglas e identifica inmediatamente las opciones imposibles. Por ejemplo, si una reunión debe ocurrir después de otra que termina a las 2:00 PM, el filtro elimina instantáneamente cualquier franja horaria antes de las 2:00 PM de la lista de posibilidades. Esto es como limpiar el desorden de un escritorio antes de intentar encontrar un bolígrafo específico. Demostraron que este filtro nunca desecha una solución válida; solo elimina la basura.
La "Escalera Compartida" (Codificación de Sufijo Compartido Disperso): Al tratar con las reglas de "debe ocurrir antes de", el método antiguo escribía una nota separada para cada par de reuniones. Si tenías 100 reuniones, eso eran miles de notas. El nuevo método notó que muchas de estas notas decían lo mismo. En lugar de escribir "Reunión A antes de B", "Reunión A antes de C" y "Reunión A antes de D" por separado, crearon una "escalera" de lógica compartida. Reutilizan variables para situaciones similares, como usar una llave maestra para varias puertas en lugar de fabricar una llave nueva para cada cerradura.
La Puntuación de "Equidad" (Equilibrio de Tiempo de Inactividad): En lugar de solo contar cuántos descansos tiene las personas, crearon una nueva forma de medir el "tiempo de inactividad". Observaron el tiempo entre la primera reunión de una persona y su última reunión. Si alguien tiene reuniones a las 9:00 y a las 11:00, su "lapso" es de dos horas. Si solo tuvo una reunión, tiene cero tiempo de inactividad. El objetivo es que la diferencia entre el tiempo de inactividad de la persona más ocupada y el de la persona menos ocupada sea lo más pequeña posible.

Lo Que Encontraron

Los investigadores probaron su nuevo método "Compacto" contra el método antiguo y contra algunos software comercial muy potentes (como Gurobi y CPLEX) en 126 casos de prueba oficiales y 100 casos de "prueba de estrés" adicionales con aún más reuniones.

Aquí están los resultados, que son bastante impresionantes:

Tamaño Menor: El nuevo método redujo el número de "cláusulas" lógicas (las reglas que la computadora tiene que verificar) en un 40.3% en promedio.
Menos Memoria: Utilizó un 55.9% menos de memoria pico. Imagina necesitar la mitad de la RAM para resolver el mismo rompecabezas.
Mayor Velocidad: El tiempo total para resolver los problemas cayó un 14.0%.
El Poder del Filtrado: El uso solo del filtro de "Pre-Chequeo" redujo el número de variables en un 24.1% y las reglas en un 16.2%.
El Poder de Compartir: El truco de la "Escalera Compartida" recortó otro 0.5% a 5.5% de las reglas, dependiendo de qué tan saturado estuviera el horario.

El Veredicto

La parte más emocionante es que sus nuevos métodos compactos de SAT y MaxSAT pudieron resolver cada uno de los 126 casos de prueba oficiales. Mejor aún, lo hicieron más rápido que el solver comercial líder, Gurobi, en términos de tiempo de la mediana. Aunque otras herramientas comerciales (como CPLEX o CP Optimizer) tuvieron dificultades para resolver todos los casos dentro del límite de tiempo, este nuevo enfoque basado en SAT los manejó todos.

El artículo no pretende haber resuelto los problemas de programación de todo el universo para siempre, pero definitivamente ha demostrado que, al limpiar las reglas y compartir el trabajo de manera más inteligente, podemos hacer que las computadoras sean mucho mejores organizando nuestras vidas ocupadas. Convierte un enorme y enredado nudo de reuniones en un horario ordenado y equilibrado donde todos obtienen su parte justa de tiempo, y nadie se queda esperando en el pasillo por demasiado tiempo.

Resumen Técnico: Codificaciones Compactas de SAT y MaxSAT para la Programación de Reuniones B2B con Equilibrio de Tiempo de Inactividad

Definición del Problema

El artículo aborda la programación de reuniones de Negocio a Negocio (B2B), un problema de optimización combinatoria donde las reuniones por parejas solicitadas deben asignarse a ranos horarios y ubicaciones específicas. La programación debe satisfacer varias restricciones:

No superposición de participantes: Un participante no puede asistir a dos reuniones simultáneamente.
Capacidad de ubicación: El número de reuniones en cualquier franja horaria no puede exceder el número de ubicaciones disponibles ( $K$ ).
Disponibilidad y Restricciones: Las reuniones deben ocurrir dentro de las sesiones solicitadas, ranos fijos o ranos prohibidos.
Precedencia: Los arcos dirigidos $(i, j)$ imponen que la reunión $i$ debe ocurrir antes que la reunión $j$ .

El objetivo propuesto en este trabajo difiere de formulaciones previas (que a menudo minimizan los "grupos de descansos" o limitan la disparidad en el recuento de descansos). En su lugar, este estudio minimiza el rango de los totales de ranos de inactividad interna ( $\Delta I$ ) entre los participantes que tienen al menos dos reuniones. Los ranos de inactividad interna se definen como el tiempo no ocupado estrictamente entre la primera y la última reunión asignada de un participante. Esta métrica distingue entre interrupciones cortas y esperas largas, buscando una distribución de carga equilibrada similar al Problema de Currículo Académico Equilibrado (BACP). También se reporta una medida de tiempo de inactividad agregada ( $I_\Sigma$ ) como métrica complementaria.

Metodología

Los autores proponen una codificación compacta de SAT (Satisfacibilidad Booleana) y MaxSAT que integra tres mejoras principales de modelado sobre las formulaciones publicadas existentes:

Filtrado de Dominio Preservador de Soluciones (Preprocesamiento):
Antes de generar la Forma Normal Conjuntiva (CNF), los autores aplican un algoritmo de preprocesamiento (Algoritmo 1) que elimina asignaciones no soportadas. Esto integra:
- Filtros de límites de extremos: Propagación de restricciones de precedencia a lo largo de rutas (usando arcos directos o clausura transitiva).
- Emparejamiento por participante: Eliminación de asignaciones que no pueden formar parte de un horario libre de conflictos para un participante específico.
- Propagación de ranos saturados: Eliminación de ranos donde la capacidad ya está totalmente utilizada por asignaciones forzadas.
- Afirmación: Este proceso preserva todos los horarios factibles mientras reduce el tamaño del dominio, reduciendo así el número de variables y cláusulas.
Codificación de Precedencia de Sufijo Compartido Disperso (SPARSESUFFIX):
En lugar de codificar relaciones de precedencia mediante cláusulas por pares (que pueden ser cuadráticas respecto al tamaño del dominio), los autores introducen una codificación dispersa.
- Materializa únicamente los "puntos de corte" distintos en el dominio del predecesor donde la restricción se vuelve activa.
- Reutiliza variables auxiliares para cortes iguales a través de diferentes relaciones.
- Se demuestra que este enfoque es equivalente a las cláusulas por pares, pero reduce significativamente el recuento de cláusulas, particularmente cuando se combina con la reducción de dominio.
Objetivo de Tiempo de Inactividad Basado en el Rango:
El artículo introduce una codificación exacta para minimizar el rango de los ranos de inactividad interna ( $\Delta I$ ).
- Deriva los primeros y últimos ranos ocupados para cada participante.
- Utiliza un número lineal de variables auxiliares para calcular la diferencia entre el máximo y el mínimo de recuentos de inactividad entre todos los participantes relevantes.

El estudio evalúa estos componentes contra una formulación base ORG-MAXSAT (una adaptación de un modelo publicado) y solvers comerciales (Gurobi, CPLEX, CP Optimizer). La evaluación cubre 126 instancias de referencia oficiales y 100 instancias derivadas de "Estrés" con densidades de precedencia variables.

Contribuciones Clave

El artículo identifica tres contribuciones específicas:

Procedimiento de Preprocesamiento: Un filtro integrado que elimina asignaciones no soportadas antes de la generación de la CNF. La Proposición 1 demuestra que esto preserva la factibilidad, y los resultados empíricos muestran que reduce las variables de asignación en un 24.1% y las cláusulas en un 16.2%.
Representación de Sufijo Compartido Disperso: Una codificación exacta (SPARSESUFFIX) que materializa solo los puntos de corte requeridos en el dominio del predecesor. La Proposición 3 demuestra su equivalencia con las cláusulas por pares. El estudio demuestra que, si bien la reducción de dominio disminuye el recuento de variables, el intercambio de sufijos reduce independientemente el recuento de cláusulas.
Objetivo Específico de B2B: Un objetivo de rango de tiempo de inactividad que mide la disparidad en los tiempos de espera interna, codificado con un número lineal de variables auxiliares.

Resultados Experimentales

Los experimentos se realizaron en una máquina de 4 núcleos con un límite de tiempo de 7,200 segundos. Los hallazgos clave incluyen:

Tamaño de la Fórmula y Memoria: Comparado con la base ORG-MAXSAT adaptada, la codificación compacta propuesta redujo el recuento de cláusulas mediano en un 40.3% y el uso pico de memoria mediana en un 55.9%.
Impacto de la Reducción de Dominio: El filtrado de dominio por sí solo redujo las variables de asignación en un 24.1% y las cláusulas en un 16.2%, contribuyendo con la mayor parte de la reducción del tamaño de la fórmula.
Codificación de Precedencia: La codificación SPARSESUFFIX redujo el recuento de cláusulas mediano entre un 0.5% y un 1.0% en las instancias de precedencia oficiales y hasta un 5.5% en las instancias derivadas de mayor densidad (al combinarse con la clausura transitiva).
Rendimiento del Solver:
- Los tres métodos SAT/MaxSAT propuestos (SAT Incremental, SAT No Incremental y UWrMaxSAT) resolvieron todas las 126 instancias oficiales.
- Comparado con Gurobi (el único solver comercial que resolvió todas las instancias), los métodos SAT/MaxSAT propuestos lograron tiempos totales medianos más bajos.
- El SAT Incremental logró el tiempo mediano más bajo (0.227s) entre los métodos completos.
- CP Optimizer tuvo el tiempo mediano más bajo (0.110s) pero no pudo resolver 11 instancias dentro del límite de tiempo.

Significado y Afirmaciones

El artículo afirma que la codificación compacta propuesta ofrece una mejora significativa de eficiencia sobre las formulaciones booleanas existentes para la programación de reuniones B2B. Al separar el filtrado de dominio de la representación de precedencia, los autores demuestran que la reducción de dominio es el principal motor para reducir el tamaño de la fórmula, mientras que la codificación de sufijo compartido disperso proporciona una reducción adicional de cláusulas de forma independiente al conjunto de relaciones.

El estudio sostiene que el nuevo objetivo de rango de tiempo de inactividad proporciona una medida más matizada de la calidad del horario que las métricas anteriores de "grupos de descansos", distinguiendo entre interrupciones cortas y esperas largas. Además, los resultados indican que los solvers modernos de SAT y MaxSAT, cuando están equipados con estas codificaciones compactas, pueden superar a los principales solvers MIP y CP en términos de tiempo de resolución mediano para esta clase específica de problemas, resolviendo todas las instancias de referencia donde algunos solvers comerciales agotaron el tiempo.

Los autores mantienen la modestia respecto al trabajo futuro, señalando que el estudio actual se centra en el tiempo de ejecución única y que investigaciones futuras podrían explorar ejecuciones de tiempo repetidas y objetivos lexicográficos (minimizar $\Delta I$ antes que $I_\Sigma$ ).