Los Diagramas de Decisión Binaria (BDDs) se han utilizado para representar modelos lógicos en una variedad de contextos de investigación, como líneas de productos de software, pruebas de circuitos y confinamiento de plasma, entre otros. Aunque los BDDs han demostrado ser muy útiles, el principal problema con esta técnica es que la síntesis de BDDs puede ser un proceso frustrantemente lento o incluso sin éxito, debido a su naturaleza heurística. Presentamos una extensión de la lógica proposicional para abordar un fenómeno recurrente en la modelización lógica, a saber, grupos de variables relacionadas por una relación de exclusión mutua, y también consideramos dos extensiones adicionales: una en la que al menos las variables en un grupo son verdaderas y otra en la que como máximo las variables son verdaderas. Agregamos primitivas XOR, alMenos-n y alMáximo-n a las fórmulas lógicas para reducir el tamaño de la entrada y también presentamos algoritmos para incorporar eficientemente estas construcciones en la construcción de BDDs. Demostramos, entre otros resultados, que el número de nodos creados durante el proceso para los grupos XOR se reduce de cuadrático a lineal para las cláusulas afectadas. El primitivo XOR se prueba en ocho modelos lógicos, dos de la industria y seis de proyectos de código abierto basados en Kconfig. Los resultados van desde no tener efectos negativos en modelos sin relaciones XOR hasta ganancias de rendimiento de hasta dos órdenes de magnitud en modelos con una abundancia de este tipo de relaciones.