Authors: Timur Ibrayev, Nikhil Sunil Chhabria
| Directory | Description |
|---|---|
| main.cpp | Main file |
| data_types.h | SAT namespace definition |
| parse_cnf.h | Parser for input .cnf file |
| sat_solver.h | DPLL algorithm with randomization and geometric restarts (RGR) heuristic |
| benchmarks/uniform_random_3-sat/ | Uniform Random 3-SAT (each folder is named as sat/unsat_<number of variables>_<number of clauses>, and has 3 instances, named 01.cnf, 02.cnf, and 03.cnf) |
| benchmarks/dimacs_benchmark_instances/aim/ | Artificially generated Random 3-SAT (each folder is named as sat/unsat_<number of variables>_<number of clauses>, and has 3 instances, named 01.cnf, 02.cnf, and 03.cnf) |
| benchmarks/dimacs_benchmark_instances/phole/ | Pigeon hole problem (3 instances, named 01.cnf, 02.cnf, and 03.cnf, all unsatisfiable) |
| doc/ | Documentation |
g++ main.cpp -o mySAT
-
Without RGR heuristic:
mySAT <file name>- Example:
mySAT benchmarks/uniform_random_3-sat/sat_50_218/01.cnf
- Example:
-
With RGR heuristic (default values):
mySAT <file name> --enable_restarts- Example:
mySAT benchmarks/uniform_random_3-sat/sat_50_218/01.cnf --enable_restarts
- Example:
-
With RGR heuristic (user-defined values):
mySAT <file name> --enable_restarts <k value>(integer) <a value>(float)- Example:
mySAT benchmarks/uniform_random_3-sat/sat_50_218/01.cnf --enable_restarts 90 1.4
- Example: