SAT_Solver

Implemented a SAT Solver using C++.

Instructions to run

1. Make sure g++ is installed on your system.
2. Move to the directory in termina in which main.cpp is located
3. Run the following commands in order

   g++ main.cpp -o sat
   

   ./sat filePath
   

   where filePath (without inverted commas) is relative path to the input cnf file.
   
   

Code Details

Directory contains the following source code files:

1. main.cpp: contains the driver code.

2. Solver.hpp : header file containing the Solver class

3. Formula.hpp : header file containing the Formula class

4. Utils.hpp : header file containing the STLs and function for calculation of runtime.

Other Files and Notations

Directory contains following files apart from the source code:

1. README.md : This file, containing instructions to run the code and directory structure.

2. input.txt: contains a cnf file, in case of no input provided in arguments, it will be taken by default.

3. tests/ : A folder containing 5 sample test cases. Inputs in the cnf specified form are in test_x.txt and curresponding solutions are in sol_test_x.txt where x is test number.

4. Solution generated by The program will be shown on terminal along with the time taken by program. If SAT, the generated model will also be displayed. The positive number represents that the literal is assigned True value and the negative number represents otherwise.