Este artículo presenta un novedoso contador de modelos SMT, llamado pact, para resolver el problema de conteo de modelos en la formulación híbrida de SMT (Teoría de Módulo de Satisfacción). Si bien los enfoques existentes basados en la fragmentación de bits tienen la limitación de limitarse a variables discretas, pact estima el número de soluciones con garantías teóricas mediante el conteo aproximado de modelos basado en hash. pact realiza llamadas logarítmicas al solucionador de SMT para variables de proyección y mejora el rendimiento mediante el uso de funciones hash optimizadas. Amplios experimentos de referencia demuestran que pact mejora significativamente el rendimiento en comparación con los métodos existentes. Por ejemplo, de 14 202 instancias, pact procesa 603 correctamente, mientras que los métodos existentes solo procesan 13.
