Hello HN, We are sharing a hybrid SAT solver focused on practical efficiency (O(log n) + CDCL). Results from the scale test: Instance: hash 001344c9b3cb1626a

Hello HN, We are sharing a hybrid SAT solver focused on practical efficiency (O(log n) + CDCL). Results from the scale test: Instance: hash 001344c9b3cb1626af1c7c35155cf26a (SAT Competence). Size: 4,751,686 Clauses and 1,313,245 Variables. Result: UNSAT Total time: 132.68 seconds (2 minutes, 12 seconds). The Quaternion Dynamics phase (O(log n)) enabled a speed increase of over 50x in variables, keeping the total time low. Proving UNSAT in this time for an instance of this magnitude is proof of the method's efficiency. Full log (Spanish Original): ============================================================ SAT SOLVER - DINAMICA POLINOMIAL DE QUATERNIONES O(log n) + PySAT = SAT/UNSAT CORRECTO ============================================================ Sube tu archivo .cnf o .cnf.xz: • 001344c9b3cb1626af1c7c35155cf26a-bench_13439.smt2.cnf.xz(n/a) - 11905108 bytes, last modified: 7/12/2025 - 100% done Saving 001344c9b3cb1626af1c7c35155cf26a-bench_13439.smt2.cnf.xz to 001344c9b3cb1626af1c7c35155cf26a-bench_13439.smt2.cnf (1).xz Archivo: 001344c9b3cb1626af1c7c35155cf26a-bench_13439.smt2.cnf (1).xz Tamano: 11905108 bytes Descomprimiendo .xz... Descomprimido: 108797713 caracteres Parseando CNF... Variables: 1313245 Clausulas: 4751686 -------------------------------------------------- Ejecutando algoritmo híbrido... -------------------------------------------------- [1] Aproximación cuaterniónica O(log n)... Heurístico: 4102660/4751686 (86.34%) [2] Decisión exacta con PySAT (CDCL)... ================================================== RESULTADO: UNSAT Tiempo total: 132.6845 segundos Complejidad O(log n): 15.618034 Clausulas satisfechas (heuristico): 4102660/4751686 ================================================== Archivo guardado: 001344c9b3cb1626af1c7c35155cf26a-bench_13439.smt2.cnf (1)_DIMACS_resultado.txt Preview: c ================================================== c SAT Solver - Dinamica Polinomial de Quaterniones c O(log n) + CDCL (PySAT) = SAT/UNSAT CORRECTO c ================================================== c Archivo: 001344c9b3cb1626af1c7c35155cf26a-bench_13439.smt2.cnf (1).xz c Variables: 1313245 c Clausulas: 4751686 c Complejidad O(log n): 15.618034 c Clausulas satisfechas (heuristico): 4102660/4751686 (86.34%) c s UNSAT ... The solver is available for testing with any known SAT Competence instance. Link to Solver Files (OSF): https://osf.io/d5kg4/files/mpxgu https://osf.io/d5kg4/files/mpxgu Good luck with your Pandora's box!