Teorías de módulo de satisfacción (SMT) es el problema de satisfacibilidad para fórmulas de primer orden con respecto a las teorías de fondo. SMT extiende la satisfacibilidad proposicional mediante la introducción de varias teorías subyacentes. Para mejorar la eficacia de la resolución SMT, se han realizado muchos esfuerzos en algoritmos de bajo nivel, pero generalmente no pueden aprovechar la capacidad del hardware paralelo. Proponemos un marco de alto nivel y flexible, a saber, la descomposición y la conciliación (LDC), para paralelizar la resolución de problemas de SMT sin cuantificadores. En general, un problema SMT primero se descompone en subproblemas, luego el razonamiento local dentro de cada subproblema se concilia con el razonamiento global sobre los símbolos compartidos a través de subproblemas en paralelo. LDC se puede construir en cualquier solucionador existente sin ajustar su implementación interna, y es flexible ya que es aplicable a varias teorías subyacentes. Instalamos LDC en la teoría de la igualdad con funciones no interpretadas, e implementamos un solucionador paralelo PZ 3 basado en Z 3. Los resultados del experimento en los benchmarks QF_UF de SMT-LIB así como los problemas aleatorios muestran el potencial de LDC, como (1) PZ 3 generalmente supera a Z 3 en 4 de 8 subcategorías de problemas bajo varias configuraciones de núcleo; (2) PZ 3 generalmente logra aceleración súper lineal sobre Z 3 en problemas con estructuras dispersas, lo que hace posible elegir un solucionador apropiado de Z 3 y PZ 3 de antemano de acuerdo con la estructura del problema de entrada; (3) en comparación con PCVC 4, un solucionador de SMT paralelo basado en una cartera de última generación, PZ 3 acelera la velocidad en una mayor parte de los problemas y tiene una mejor relación de velocidad general.