limo1996 / sat-solver Goto Github PK

One of the main questions of the professors was:
"Why are the dots so spread for larger formulas?"

We should be able to answer that question in a "scientific" way, i.e. something like this:
"The formula on the top of the plot is very difficult to solve, the dpll algorithm needs to make 25 branching steps until it is able to solve the formula.
On the other hand the formula on the bottom is very easy to solve, the dpll algorithm doesn't need to branch at all".

We should come up with a numerical representation of the difficulty of a formula, one suggestion (used above) is to use the maximal branching depth until a solution is found or unsat is proven.
Note that that does not mean we can just count the number of "branches" taken during an execution, we need to associate true and false branches on the same variable and count them as one.
Effectively we need to find the depth of the tree.
But counting the number of branches in total would also be a metric, it would tell us how "bad" the decisions that our algorithm made are. I would suggest we do both...

A good starting point is to change the stderr output in dpll.cpp such that we record the necessary information.
We could then create a python script that reads the stderr output and comes up with the branching depth and the overall number of taken branches.

I suggest that we just do it on the sequential version, as it will be identical to the parallel one (this is a property of the cnf formula).

Looks like our DPLL is not working...
fail_example1.cnf and fail_example2.cnf are examples of such behavior...

encode the cnf formulas as integer arrays and boolean arrays instead of using object structures -> should require a lot less space -> better spacial locality -> faster!

• Move encoding and decoding of model to model class
• change get_model to get_partial_model in CNF.cpp
• implement get_model in CNF.cpp, and move the functionality from send_sat solver there
  Regarding the two last points: yes it's super confusing right now

We should store some runtime measurements in files on euler.
Such that one can then manually download them, run a script and get a nice plot (x-axis: size of formula i.e. number of variables, y-axis: runtime)
There are 3 changes necessary as far as I can see:

1. add information to how large randomly generated formulas are to the file names (overlaps with #8 )
2. measure runtime in parallel_main.cpp and store it in a file
3. write a script that given such files can create the plots

Additionally we should have far more and far larger formulas! -> #8

Whenever I try to run something on Euler on more than 48 cores I get the following error message:

virtual.40d: Queue has been closed. Job not submitted.

Weird...

Here's the full output of main.py:

please enter your nethz_account name : ebjan
Euler parameters:
           num_nodes: [16, 64, 128]
            num_runs: 4
             timeout: 15 [seconds]
 max_overall_runtime: 240 [minutes]
         test_folder: 3-sat_instances_medium
[email protected]'s password: *
to_euler.tar                                                                      100% 1860KB   1.8MB/s   00:00    
Pseudo-terminal will not be allocated because stdin is not a terminal.
[email protected]'s password: *
Generic job.
virtual.40d: Queue has been closed. Job not submitted.
#########################################################
unpacking tar archive...
calling run_me_on_euler.sh...
#########################################################
run_me_on_euler.sh is taking over
including necessary modules...
node counts: 16 64 128
choosing highest node count: 128
submitting compilation and run job to the batch system...
an error occurred during job submission, exiting
#########################################################

in Variable.cpp/Variable.h

Is it valid to have more than one CNF in a file? Parser seems to be able to parse multiple CNFs from one file...

If we want to get more overall performance we should implement CDCL!

We should add an option to the plotting script to add numbers to identify formulas.

An idea on how this might look like:
https://stackoverflow.com/questions/14432557/matplotlib-scatter-plot-with-different-text-at-each-data-point

We should add a command line option to the plotting script that enables the numbers.
For command line option parsing one could use the click python package, example usage is in main.py.

Create a google slides presentation.
I think it should cover the following aspects:

1. how did we start (sequential algorithm that we took over)
2. how did we parallelize it?
3. how did we test it?
4. some initial performance evaluations
5. what do we plan to do next?

As discussed we should iprobe on a different tag.
The exception that I planted seems to be triggered in a couple of cases (13 times out of 840 executions).
Here's the output file from euler:
lsf.o52407426

We need more test-cases!
Small ones and also large ones.
We should store them in the repository such that everyone can run the same tests.

2 things:

1. just generate a lot of them (I would say 100 of size (number of variables) 10, 30, 50, 100, 200 at least)
2. change the names of the test files such that we know how "large" these formulas are (useful for evaluation)

Jan, I think it would be better to move encoding and parsing of formula to CNF class so I can reuse it in Master class (I need to parse final formula and print it). I will push in few minutes data class named State that basically hold array of unsigned ints and its size + getter and setter.

Your methods can looks like:
State CNF::encode(); //cnf will encode itself to State object

CNF cnf = new CNF(State state); // cnf will parse itself from State object
// ---- or -----
CNF cnf = new CNF();
cnf.parse(State state);

What do you think about that?

We have too much folders in main folder. After Mondays presentation we should move all tests to common test folder, rename python_wrapper to scrips, move randomCNF to scripts.