Barcelogic SAT Solver: System description
Morgan Deters, Germain Faure, Robert Nieuwenhuis, Albert Oliveras · 2006
The Barcelogic SAT Solver is an efficient implementation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure [DP60, DLL62].Our original aim for developing it was the need of a DPLL-based engine forour DPLL(T) approach to Satisfiability Modulo Theories (SMT): deciding thesatisfiability of ground first-order formulas with respect to background theoriessuch as equality, linear integer or real arithmetic, arrays, etc. A DPLL(T) systemconsists of a general DPLL(X) engine, very similar in nature to a SAT solver,whose parameter X can be instantiated with a solver Solver