Daniel Berend

In this paper, we present and study a new algorithm for the Maximum Satisfiability (Max Sat) problem. The algorithm, GO-MOCE, is based on the Method of Conditional Expectations (MOCE, also known as Johnson’s Algorithm), and applies a greedy variable ordering to it. We conduct an extensive empirical evaluation on two collections of instances – instances from a past Max Sat competition and random instances. We show that GO-MOCE reduces the number of unsatisfied clauses by tens of percents as compared to MOCE. We prove that, using tailored data structures we designed, GO-MOCE retains the linear time complexity. Moreover, its runtime overhead in our experiments is at most 10%. We combine GO-MOCE with CCLS, a state-of-the-art solver, and show that the combined solver improves CCLS on the above mentioned collections.