Implementing a DPLL SAT Solver in Python

Boolean Satisfiability Problem (SAT) is a fundamental problem in computer science with applications in verification, artificial intelligence, and optimization. This challenge asks you to implement a basic DPLL (Davis-Putnam-Logemann-Loveland) algorithm, a widely used technique for solving SAT problems. Your solver should take a Conjunctive Normal Form (CNF) formula as input and determine if it is satisfiable, returning a satisfying assignment if one exists.

Problem Description

You are tasked with creating a Python function solve_sat(cnf) that implements a DPLL SAT solver. The input cnf is a list of clauses, where each clause is a list of literals. A literal is an integer representing a variable (positive integer) or its negation (negative integer). For example, [[1, -2, 3], [-1, 4], [2, -3]] represents the CNF formula (x1 OR NOT x2 OR x3) AND (NOT x1 OR x4) AND (x2 OR NOT x3).

The function should return:

• True if the CNF formula is satisfiable, along with a dictionary representing a satisfying assignment (mapping variable numbers to boolean values - True or False).
• False if the CNF formula is unsatisfiable.

The DPLL algorithm should incorporate the following techniques:

1. Unit Propagation: If a clause contains only one literal, assign that literal's value to satisfy the clause.
2. Pure Literal Elimination: If a variable appears only positively or only negatively in the CNF formula, assign it a value that makes all its clauses true.
3. Splitting: If neither unit propagation nor pure literal elimination can simplify the formula, choose a variable and recursively call the solver with both possible truth assignments (True and False) for that variable.

Examples

Example 1:

Input: [[1, -2, 3], [-1, 4], [2, -3]]
Output: (True, {1: True, 2: False, 3: True, 4: True})
Explanation:  One possible satisfying assignment is x1=True, x2=False, x3=True, x4=True. This assignment makes all clauses true.

Example 2:

Input: [[1], [-1]]
Output: False
Explanation: This formula is unsatisfiable because the clauses [1] and [-1] contradict each other.

Example 3:

Input: [[1, 2], [-1, 2], [1, -2], [-1, -2]]
Output: False
Explanation: This is a classic unsatisfiable formula. No assignment can satisfy all four clauses.

Example 4:

Input: [[1, 2], [-1, 3], [-2, -3]]
Output: (True, {1: True, 2: True, 3: False})
Explanation: One possible satisfying assignment is x1=True, x2=True, x3=False.

Constraints

• The input CNF formula will consist of integers between -N and N, where N is a positive integer.
• The number of clauses will be between 1 and 100.
• The number of literals in each clause will be between 1 and 10.
• The solver should be reasonably efficient; avoid exponential time complexity where possible through effective unit propagation and pure literal elimination.
• The assignment dictionary returned should only contain variables that appear in the input CNF.

Notes

• The order in which you choose variables for splitting can significantly impact performance. Consider heuristics for variable selection (e.g., choosing variables that appear in the most clauses).
• Implement unit propagation and pure literal elimination before splitting to reduce the search space.
• Be mindful of recursion depth. Deeply nested unsatisfiable formulas can lead to stack overflow errors. While not explicitly required, consider techniques to mitigate this if you encounter issues.
• The assignment dictionary should map variable numbers (positive integers) to boolean values (True or False).
• The returned assignment is one possible satisfying assignment; there may be others.
• The function should handle empty CNF formulas correctly (returning True with an empty assignment).