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.
Top comments (0)