A Finite Domain Satisfiability Solver with Clause Learning and Non-Chronological Backtracking

Abstract Boolean Satisfiability (SAT) is a well known NP-complete problem that has recently received much attention due to increasing practical application in various fields such as Artificial Intelligence, Group Theory, Formula Verification, Electronic Design Automation, Logic Synthesis, etc. A search algorithm to solve this problem was proposed by Davis, Putnam, Logemann, and Loveland (DPLL) some four decades ago. Although DPLL is an old algorithm, most of the current state-of-the-art SAT solvers are based on it. Recent additions to DPLL such as clause learning, non-chronological backtracking, and random,restart have improved the capability of problem solving. Finite Domain Satisfiability is a generalization of Boolean Satisfiability in which the size of the domain of a variable may be greater than two. Many practical applications fall under this category, but to solve them, traditionally they are encoded into Boolean format and solved using a Boolean solver. This not only obscures the structure of the problem but also increases the size of the problem, hence making it harder to solve.