Project Name: Basic DPLL solver in C++
Project done by Harpreet Dhiman (B20ME035)
...........................................................
solver_giveString.cpp:::: The code is used for custom CNF formula.
Give the CNF formula in product of sums format to the 'string input' and the code prints the solution in the terminal.
This printed solution needs to be further added to output_format.py to get true solution in a list formula.Add the printed solution generated by solver_literal_clauses.cpp or solver_giveString.cpp to the string 'output'.
solver_literals_clauses.cpp:::: The code takes the following as input:
- Number of Literals
- Number of clauses
The code then generates a random CNF formula having the given number of literals and clauses.
Further, it solves the CNF and prints the solutions in the terminal.
This printed solution needs to be further added to the file output_format.py
output_format.py:::: The code gets the true solution in a list of list of string format using the function correct_soln, and stores it in true_soln.
Hence, true_soln is your solution to the CNF formula.
Further, in case the user wants to verify the solution, the function make_vector takes true_soln as input and gives a string, stores it in cpp_vector.
This string cpp_vector can be directly given to the vector vec in the file verify_solution.cpp
verify_solution.cpp:::: The code checks whether the given solution checks the given cnf formula.
First, give the CNF formula whose solution needs verification and store it in the string input.
Then give the solution string obtained from output_format.py to the vector vec.
Now, the code has input string and the solution vector vec.
The code returns 1 if the solution verifies the CNF formula and 0 otherwise.
===================================================================================
For any query/suggestions: please write to Binod Kumar ([email protected])