Finish-Up-A-Thon: Teaching DPLL — A Minimal, Traceable C++ SAT Solver

MOULIK CHOUDHARY — Sat, 06 Jun 2026 18:08:54 +0000

This is a submission for the GitHub Finish-Up-A-Thon Challenge

What I Built

Project: SAT Solver (C++): a compact, educational SAT solver that parses DIMACS CNF files and uses a DPLL-based algorithm with unit propagation and pure-literal elimination.
Project Link: SAT Solver

Scope: Command-line tool that reads CNF files, determines satisfiability, and prints a satisfying assignment when found.

Key features: robust DIMACS parsing, three-state assignments (TRUE/FALSE/UNASSIGNED), DPLL backtracking, unit propagation, pure-literal elimination, explanation trace mode, step-by-step interactive trace, and trace export to file.

Why it matters: This repo is a small, teachable implementation of a fundamental algorithm in logic and theoretical CS — useful for students learning SAT solving, debugging CNF problems, or demonstrating algorithmic decision tracing.

Demo

Live demo (local):
Build and run locally:
Build: make or build.bat
Run a sample: .sat_solver.exe test\sample.cnf
Explanation run: .sat_solver.exe --explain test\sample.cnf
Step-by-step: .sat_solver.exe --step test\unit_propagation.cnf
Write trace: .sat_solver.exe --explain --trace-out trace.txt test\pure_literal.cnf

Screenshot:

The Comeback Story

Before: The project had a working solver core but limited DIMACS validation, no interactive trace, and no easy build/test helpers.

What I changed:
Strengthened parser: strict p cnf header checks, literal range validation, header/clauses count warnings, and graceful inference if header missing.
Added user-facing features: --explain trace mode, --step interactive mode (pauses after each logged step), and --trace-out to export traces.
Added developer convenience: Makefile, build.bat, and run_tests.ps1 to build and run test CNFs easily.

Improved documentation: updated README.md with new flags and usage examples.

Impact: The solver is now more robust for classroom demos and easier to build/test across platforms. Students can follow decision traces live or export runs for analysis.

My Experience with GitHub Copilot

How Copilot helped: Copilot suggested idiomatic C++ patterns and small refactorings while I implemented parser validation and trace export. It sped up routine tasks (e.g., string formatting, logging snippets) and helped prototype the step-mode interaction.
Human + AI workflow: I used Copilot as a coding assistant and then verified and adapted suggestions manually — ensuring correctness and adding precise error messages and tests.
Takeaway: Copilot is most valuable for accelerating boilerplate and surfacing implementation ideas; final correctness and UX decisions still require human review.

DEV Community: MOULIK CHOUDHARY

DPLL Demystified — A Traceable C++ SAT Solver