-
Notifications
You must be signed in to change notification settings - Fork 1
/
README
50 lines (34 loc) · 1.42 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
1) How to run SAT solver
make
./saturday <testcase>
2) Members in group and the division of work
Aaron Shim
Qingyang Chen
Pair programmed
3) Extensions
- randomization of recursive branching
- restarting backtrack when over cutoff
- generalized optimization on literal choice
- clause trimming
- logical solving before complete search
4) Time taken
About 15 hours each
5) Programming language
C++
6) Biggest challenge
Everytime we wrote an optimization, it would break. Because we would have to
figure out how many cases were actually broken, we appreciated having our
automated test script check that we sufficiently debugged each extension back to
a baseline functionality before moving on.
7) Udder stuff
Our solver performs comparatively to MiniSAT, and beats MiniSAT on certain cases.
We wrote a testing script that can compare the speeds of any two SAT solvers.
There were many other extensions and microextensions we wanted to implement, or
did implement but discarded afterwards.
To run our testing script:
1) Install minisat
2) Run ./test (see script for parameters or changing the SAT solver to test against minisat)
Complete list of options can be found by running ./test --help
Some of the highlights include testing against custom executables by passing in the -e flag
(Hence, this test script will work against any other SAT solver contender compiled to an
executable that takes in a file input as a command line argument.)