Propositional Satisfiability Problems

Todd Sullivan, Harry Robertson, Pavani Vantimitta
Stanford's Reasoning Methods in Artificial Intelligence Course
Project 1 of 4
Stanford Department of Computer Science

In this project we created a SAT solver. As our project's feedback shows, our implementation was the fastest out of all seven groups!

We were given no starter code for the assignment. We were only given plain text files containing the problem descriptions in conjunctive normal form (as described in the project description).

Technical Report

Member Contributions

The following list details all group contributions. These contributions were not the original tasks assigned to each group member, but were the end result due to each member's abilities and other issues.

  • Harry, Pavani, and I codeveloped all basic features in a rather adhoc manner.
  • I implemented all optimizations described in Section 3.
  • I performed all experiments, collected all data, and organized all results.
  • Pavani wrote the introduction and algorithm descriptions for the report (Sections 1 and 2).
  • I wrote the optimizations section (Section 3).
  • Harry and I discussed the results while Harry wrote the results analysis section of the report (Section 4).
  • Harry edited my portion of the report (Section 3).
  • I edited Pavani's portion of the report (Sections 1 and 2) and Harry's portion of the report (Section 4).
  • Pavani and I converted the Excel-based tables into Annex 1 and Annex 2.
  • I applied all formatting and presentation features to the report and annexes.

Source Code

Since this assignment will be used in future versions of the reasoning methods course, I am not releasing the code at this time.