Solving Hard Satisfiability Problems: A Unified Algorithm Based on Discrete Lagrange Multipliers