Logic Algorithms

Boolean satisfiability (SAT) asks whether a propositional formula can be made true by some assignment of its variables. It is NP-complete, so no known algorithm decides it in polynomial time; a polynomial solution would settle P versus NP. This project sidesteps the worst case with local search, trading completeness for speed, and uses it to solve Sudoku puzzles.

SAT solvers take conjunctive normal form,

a conjunction of clauses, each clause a disjunction of literals ${\ell }_{ij}$. A Sudoku board encodes as one Boolean variable $x_{r,c,d}$ per (row, column, digit) triple, true when cell $(r,c)$ holds digit $d$; the code names each variable by the three-digit string rcd and negates with a leading -. The Sudoku class writes the rules out as clauses to a .cnf file — each cell gets an at-least-one disjunction over its nine digits plus pairwise at-most-one clauses, each row, column, and $3\times 3$ block gets a clause per digit forcing it to appear, and every given cell contributes a unit clause. Smaller staged files (one_cell, rows, rows_and_cols, rules) build the encoding up piece by piece for testing. A completed board is a satisfying assignment.

The SAT solver is generic: it reads any CNF file, maps each variable to an index with a two-way dictionary, and starts from a random full assignment, flipping one variable at a time. GSAT and WalkSAT share a noise parameter (threshold $=0.3$) and a flip budget (max_iterations $=100,000$). On each step GSAT, with probability $p$, flips a random variable, and otherwise scans all variables and flips the one whose flip leaves the most clauses satisfied — hill climbing that stalls on local optima where no single flip helps.

WalkSAT narrows the search. It first collects the currently unsatisfied clauses, picks one at random and, with probability $p$, flips a random variable in it; otherwise it considers only that clause's variables and flips the one that leaves the most clauses satisfied. Restricting the greedy scan to a single broken clause is what makes each step cheap.

Neither algorithm is complete: on an unsatisfiable formula they simply exhaust the flip budget without reporting that no assignment exists. On satisfiable instances like a valid Sudoku they find an assignment quickly, which is the regime this project targets.