DPLL-SAT-Solver: Peg Game Logic Optimizer

This project implements an automated reasoning engine that solves the generalized Peg Game puzzle by compiling the game state and rules into Propositional Logic and solving them using the Davis-Putnam-Logemann-Loveland (DPLL) algorithm.

🧩 Problem Overview

The Peg Game is a classic puzzle where pegs are jumped over one another into empty holes, removing the jumped peg. The goal is to find a sequence of $K$ jumps that leads to a specific end state—typically leaving only one peg on the board.

In this implementation, the puzzle is treated as a Satisfiability (SAT) Problem. The program determines if a valid sequence of moves exists for a given board configuration and jump count.

🚀 Technical Approach: Propositional Encoding

The solver translates the board and rules into five distinct types of logical propositions in Conjunctive Normal Form (CNF):

1. Precondition Axioms

Ensures a jump is only possible if the source and "jumped" holes have pegs, and the destination hole is empty.

• Logic: $Jump(A,B,C,I) \implies Peg(A,I) \land Peg(B,I) \land \neg Peg(C,I)$

2. Causal Axioms

Defines the state change after a jump: the source and jumped holes become empty, and the destination hole gains a peg at the next time step.

• Logic: $Jump(A,B,C,I) \implies \neg Peg(A,I+1) \land \neg Peg(B,I+1) \land Peg(C,I+1)$

3. Frame Axioms

Asserts that a hole's state (peg or no peg) remains unchanged unless a relevant jump action occurs at that specific time point. This prevents "spontaneous" changes in the board state.

4. Action Constraints

• No Overlap: Ensures that no two actions can be executed at the same time point.
• Continuous Progress: Ensures at least one valid action is executed at each step to reach the target jump count.

5. Starting State

Specifies the initial truth values for $Peg(H, 0)$ for every hole $H$ on the board based on the input configuration.

🏗 System Architecture

The system is divided into three core components:

• Puzzle2SAT (Front-End): Compiles the board triples and starting state into a list of integer-based CNF clauses suitable for a SAT solver.
• DPLLTop (Solver): An implementation of the DPLL algorithm that performs unit propagation, literal picking, and backtracking search to find a satisfying binding.
• Bindings2Jumps (Back-End): Maps the numerical SAT solution back into human-readable jump sequences (e.g., Jump(2,1,0); Jump(3,0,1)).

📊 Performance

The solver is capable of handling:

• Standard 10-hole and 15-hole triangular boards.
• Complex state-space searches involving thousands of propositions.
• Efficiently identifying "No solution found" for mathematically unattainable board states.

🛠 Tech Stack

• Language: Python 3
• Concepts: Propositional Logic, CNF, SAT Solving, DPLL Algorithm, Backtracking Search, Constraint Satisfaction.

🔧 How to Run

The solver is executed via the PegPuzzle superroutine:

board = [[0,1,2], [1,2,3], [2,3,0], [3,0,1]]
start = [0]
numJumps = 2

# Returns the sequence of moves or "No solution found"
PegPuzzle(board, start, numJumps)