Overview
This Sat solver has two methods implemented in java:
1-Dynamic Largest Individual Sum (DLIS) heuristic
2-Davis-Putnam-Logemann-Loveland (DPLL).
In DLIS, the idea is to choose the variable that appears most frequently in unsatisfied clauses or has the largest sum of occurrences in unsatisfied clauses. By selecting such variables, DLIS focuses on resolving conflicts related to the most problematic parts of the formula. The DPLL algorithm works by recursively exploring the search space of possible assignments to the variables of a given formula until a satisfying assignment is found or it determines that the formula is unsatisfiable.