Resumen: Proponemos IMITSAT, una política de ramificación para solucionadores de aprendizaje de cláusula impulsado por conflictos (CDCL) basados en el aprendizaje de imitación para el problema de satisfacción booleana (SAT). A diferencia de los métodos anteriores que predicen señales a nivel de instancia para mejorar la ramificación de CDCl indirectamente, o confiar en el aprendizaje de refuerzo y la información insuficiente de CDCL para mejorar la ramificación, IMITSAT aprende de expertos Keytrace que colapsa una ejecución completa de la secuencia de decisiones sobrevivientes. Reproducir una discusión clave en la misma instancia está casi libre de conflictos, proporcionando una densa supervisión de nivel de decisión y reduciendo directamente las propagaciones, el contribuyente dominante al tiempo de pared. Esta supervisión condicionada con prefijo permite a IMITSAT reproducir ramas de alta calidad sin exploración, produciendo una convergencia más rápida, un entrenamiento estable e integración perfecta en CDCL. Experimentos extensos demuestran que IMITSAT reduce los recuentos de propagación y el tiempo de ejecución, superando los enfoques aprendidos de última generación. Lanzamos el código fuente y el modelo capacitado en esta URL HTTPS
Publicado Originalme en export.arxiv.org El 30 de septiembre de 2025.
Ver Fuente Original
