SAT-SOLVER

MineSAT is an optimised SAT-Solver that uses the Semantic Tableux as a decision procedure for solving SAT problems.

To use this SAT-Solver,

1. Compile sat_solver.cpp :

g++ -std=c++11 sat_solver.cpp -o minesat

2. Run the binary created and also specify the file containing the SAT problem in DIMACS form and the file in which the output should be emitted :

./minesat sat_in.txt sat_out.txt

3. Note that the input file must be present in the same directory as the binary.
4. The output file is also created in the same directory.
5. The solution of the SAT problem in DIMACS form is published in the specified output file.
6. The solution, the number of steps required and the time taken for computation are printed on the command line interface.

Heuristics:

1. Based on the number of times a literal appears in the SAT problem, each literal is assigned a Frequency Value (FV). The FV for a clause is simply the sum of the FVs of all its literals (a proposition and its negation is considered the same for the purpose of frequency assignment). The clauses are then sorted based on their FV, and the clause having the least FV is decomposed first.

2. Unit Propagation : At each node of the tree, we check for clauses containing just one literal. Say such a clause x exists, then the literal in x is set to true (if it contradicts another literal, the node returns false). Based on the values set by these literals, clauses are either shrunk (if a false literal is present in the clause) or removed (if a literal in the clause is true). This process is recursively performed until no unit clauses remain.

3. While decomposing a clause, the literal having the lowest FV in the clause is processed first.

4. At any node, after performing unit propagation, a literal is selected using heuristic 3 and is set to true and its corresponding subtree is explored, if it returns false, the literal is set to false and the other subtree is explored. If both of them return false, the answer is UNSAT.

Benchmarks :

• 588 steps were required to solve a 9x9 SUDOKU+ from the first assignment and it took 3.77585 seconds to solve.
• 1 step was required to solve a 4x4 SUDOKU+ and it took 0.010606 seconds to solve.
• 117.045, 691.537 and 0.006961 seconds were required to clear uuf175-021, uuf175-033 and uf50-022 benchmarks.