A SAT solving project for the Vrije Universiteit 2021 course Knowledge and Data.
'dlcs' : 'Dynamic largest combined sum'
'dlis' : 'Dynamic largest individual sum'
'jw' : 'Jeroslow-Wang one-sided'
'jwtwo' : 'Jeroslow-Wang two-sided'
'mams' : 'DLIS plus MOMS'
'moms' : 'Maximum occurence in clauses of minimum size'
'random' : 'Random with equal weights'
'weighted' : 'Random with weighting by amount of occurences'Python version >= 3.7.
Optionally the requirements Pebble == 4.6.3 and pandas == 1.3.4 have to be met if you wish to run run_experiment.py. The main program is provided in SAT.py which does not have any additional requirements.
To install both optional packages just run:
pip install -r requirements.txtTo do a single SAT solve and get its results run:
python SAT.py PATH_TO_DIMACS_FILE --heuristic HEURISTICThe resulting answer will be stored in PATH_TO_DIMACS_FILE_n.out
Replace PATH_TO_DIMACS_FILE with a string to where the SAT in DIMACS format can be found. As an example sudoku-example_NxN.txt are provided.
Replace HEURISTIC with the heuristic to use (default random). Supported heuristics are: ['dlcs', 'dlis', 'jw', 'jwtwo', 'mams', 'moms', 'random', 'weighted']. Additionally the heuristic can be suffixed with either _pos or _neg to force a True or False assignment respectively. So then the heuristic given becomes e.g. random_neg.
Add --runs n if you wish to run and solve the solver n times. Each solution will be seperately stored.
Add --profile if you wish to get a cProfile report about the exact function runtimes and amount of calls.