Skip to content
/ SAT_2 Public

Project 2 for the `SAT solving' course at the LMU.

Notifications You must be signed in to change notification settings

mkg33/SAT_2

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

64 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Instructions:

Use the 'makefile' to compile the programme.
We also include a script that we have used to test our solver.
To use the runTests.py script, please change the output of the solver (as described in the comments in maph.cpp).

Usage instructions:

Usage: ./maph.out <DIMACS file> selection heuristic:
 <FIRST=0 | RANDOM=1 | DLIS=2 | RDLIS=3 | DLCS=4 | RDLCS=5 | JW=6 | RJW=7 | MOMS=8 | RMOMS=9>

Available selection heuristics:
- FIRST: select the first available literal
- RANDOM: select a random literal
- DLIS: Dynamic Largest Individual Sum
- RDLIS: randomized Dynamic Largest Individual Sum
- DLCS: Dynamic Largest Combined Sum
- RDLCS: randomized Dynamic Largest Combined Sum
- JW: Jeroslow-Wang heuristic
- RJW: randomized Jeroslow-Wang heuristic
- MOMS: Maximum [number of] Occurrences in Minimum [length] Clauses
- RMOMS: randomized Maximum [number of] Occurrences in Minimum [length] Clauses

Note: Although we have implemented pure literal elimination, we quickly found that
it slowed out solver down. So we haven't measured the CPU time with pure literal elimination.

About

Project 2 for the `SAT solving' course at the LMU.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published