I den här artikeln beskrivs ManySAT en ny portföljbaserad parallell SAT-lösare noggrant. Designen av ManySAT drar nytta av de viktigaste svagheterna hos moderna SAT-lösare: deras känslighet för parameterinställning och deras brist på robusthet. MångaSAT använder en portfölj av kompletterande sekventiella algoritmer som erhållits genom noggranna variationer av standard DPLL algoritm. Dessutom delar varje sekventiell algoritm klausuler för att förbättra den totala prestandan för hela systemet. Detta står i kontrast till de flesta av de parallella SAT-lösarna i allmänhet utformade med hjälp av splitter-och-konvergensparadigmet. Experiment på många industriella SAT-fall, och den första rangen som ManySAT fick i parallellspåret av 2008 SAT-Race visar tydligt potentialen i vår designfilosofi.
Den första parallella portföljen SAT lösare var ManySat REF.
ManySAT: a Parallel SAT Solver
{'venue': 'J. Satisf. Boolean Model. Comput.', 'journal': 'J. Satisf. Boolean Model. Comput.', 'mag_field_of_study': ['Computer Science']}