DM841 - Heuristics and Constraint Programming for Discrete Optimization
Assignment 4, Fall 2016 [pdf format]

• This is an obligatory training assignment on local search. It has the main goal of preparing you for the final assignment.
• Throughout the assignments you will set up a developing environment, gain practical experience on the methods discussed in class, try your own ideas on a problem, and carry out the analysis of experimental results. The content of the assignments will also provide elements for discussion in class. You are encouraged to search feedback among your peers, and ask questions in class related to the assignment. Hence, working in pairs is allowed, but the submission must be individual. Instead, in the final assignment collaboration will be not allowed. (Be aware that not only the idea but also how it is implemented is relevant for the final performance of an algorithm – and performance counts in this course!)
• Make sure you have read the following sections before starting to implement anything.
• This assignment is focused on the well known Satisfiability Problem (SAT), see the slides for a definition, and it assumes that the Practice on the Queens problem from the training sessions
  Guided example
  has been finished. The assignment asks to develop a local search solver that will be run on each test instance with a time limit of 20 seconds. The submissions will be compiled and executed online.

Your Tasks

All the points below must be addressed in any order:

1. Model the satisfiability problem in terms of local search
2. Design a basic iterative improvement algorithm with a natural termination in a local optimum. Call this algorithm: sat_ii.
3. Design speedups for the execution of sat_ii and call the new algorithm sat_ii_+.
4. Design stochastic local search algorithms that go beyond local optima and that do not have a natural termination. Examples to consider are: (probabilistic iterative improvement, min conflict heuristic, simulated annealing, tabu search, variable neighborhood search, etc.) Call these algorithms sat_sls_*, where the star indicates a suffix of your choice.
5. Implement sat_ii, sat_ii_+ and sat_sls_*. For this you can use the start package linked below based on EasyLocal.
6. Execute the algorithm sat_ii 30 times and plot the distribution of running times and of solution quality.
7. Show experimentally that sat_ii_+ is indeed more efficient than sat_ii.
8. Compare experimentally your algorithms from point 4. on the given instances when run with a time limit of 20 seconds on a desktop computer equivalent to those in the IMADA terminal room. For each algorithm collect at least 10 runs per instance. Include in the comparison a baseline algorithm consisting in a random restart of your sat_ii_+.
9. Describe in a short report (max 5 pages):
   • your model for your local search approach to SAT
   • all your algorithms sat_ii, sat_ii_+ and sat_sls_* to a level of detail that allows replication
   • the speedups introduced
   • the experimental analysis
   Use proper mathematical formalism and computer science sketches to specify your algorithms. Use R for the analysis of results and the production of graphics and tables.

In addition, the submission system will execute your program and compare it against your peers on new unseen instances. Therefore you should submit your best algorithm early and eventually revise your submission. Before submitting, test your implementation on the IMADA machines.

You must upload your program and report at:

The web page will compile your files, run your program, store and verify the solution and provide an analysis of results for the assessment of your algorithm. You can continue to submit new results until the deadline and it is recommended to try early to submit in order to ensure the format is as required.

Before continuing reading download the SAT package.

Test Instances

Two sets of test instances will be used: satisfiable instances and unsatisfiable instances. The comparison of the sat_sls_* algorithms will be based, on the first class, on the computation time to find a model that satisfies the instance, and, on the second class, on the number of violated clauses that has to be minimized.

In the directory data from the SAT Start package nine instances are made available: three satisfiable instances of size 20, three satisfiable instances of size 250, three unsatisfiable instances of size 250. These instances are training instances and mustbe used for your local tests. On the submission page, your program will be tested on different but similar instances.

In the following it is described the format of these instances.

• On the satisfiability problem there is an yearly competition http://www.satcompetition.org for both complete and incomplete algorithms. We will conform to the competition input/output requirements (they are described at this page: Benchmark Guidelines and briefly reported here).
  • Input: The benchmark file format will be in a simplified version of the DIMACS format.

    The file can start with comments, that is lines beginning with the characters “c “. Right after the comments, there is the line “p cnf nbvar nbclauses” indicating that the instance is in CNF format; “nbvar” is the exact number of variables appearing in the file; “nbclauses” is the exact number of clauses contained in the file. Then the clauses follow. Each clause is a sequence of distinct non-null numbers between “-nbvar” and “nbvar” ending with 0 on the same line; it cannot contain the opposite literals i and −i simultaneously. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables.

    Example:

    c
    c start with comments
    c
    c 
    p cnf 5 3
    1 -5 4 0
    -1 5 3 4 0
    -3 -4 0
    

  • Output: All lines, according to their first char, must belong to one of the three following categories:
    • comments (any information that authors want to emphasize, such like #backtracks, #flips,... or internal cpu-time), beginning with the two chars “c “
    • solution (satisfiable or not). Only one line of this type is allowed. This line must begin with the two chars “s “ and must be one of the following ones:

      s SATISFIABLE
      s UNSATISFIABLE
      s UNKNOWN
      

    • values of a solution (if any), beginning with the two chars “v “ (to be precised in the following).

    If the solver outputs SATISFIABLE, it must provide a model (or a certificate) that will be used to check the correctness of the answer. I.e., it must provide a 0-terminated sequence of distinct non-contradictory literals that makes every clause of the input formula true. It is NOT necessary to list the literals corresponding to all variables if a smaller amount of literals suffices. The order of the literals does not matter. Arbitrary white space characters, including ordinary white spaces and tabulation characters, are allowed between the literals, as long as the line containing the literals is a values line, i.e. it begins with the two chars “v “.

    For instance, the following outputs are valid for the instances given in example:

    mycomputer:~$ ./mysolver --main::instance myinstance-sat
    c mysolver 6.55957 starting with SATTIMEOUT fixed to 1000s
    c Trying to guess a solution...
    s SATISFIABLE
    v -3 4 -6 18 21 1 -7 0
    c Done (mycputime is 234s).
    

    mycomputer:~$ ./mysolver --main::instance myinstance-unsat
    c mysolver 6.55957 starting with SATTIMEOUT fixed to 1000s
    c Trying to guess a solution...
    c Contradiction found!
    s UNSATISFIABLE
    c Done (mycputime is 2s).
    

• The Input class is already implemented in the starting package. Given the format of the input file, the most trivial way to represent a formula is as a list of clauses, each element of the list pointing at a list that contains the indices of the variables/literals that belong to the clause. The indices of the variables can be negative or positive depending on whether the corresponding literals are negated or not in the clause. In C++ we declare the data structure in the attributes of the class SAT_Input in input.hh as follows:

  // your data members   unsigned nbvar, nbclauses;   vector<vector<int> > formula;

  Of course other representations also more efficient are possible and you are welcome to improve the implementation. It is however common practice to leave code optimization to a later stage. The file reader is implemented as follows:

  // File input.cc #include "input.hh" #include <fstream> #include <cassert> #include <sstream> SAT_Input::SAT_Input(string file_name) {   // Insert the code that reads the input from the file   // and stored it into the data structures of the object   ifstream is(file_name.c_str());   if (!is) {     cerr << "Cannot open file " << file_name << endl;     exit(1);   }   string line;   istringstream iss;   do {     getline(is, line);   } while (line[0] == 'c');   iss.str(line.substr(1,string::npos));   string ch;   iss >> ch >> nbvar >> nbclauses;   formula.resize(nbclauses);   unsigned c = 0;   do {     getline(is, line);     if (line[0] == '%' || line[0] == '0')       break;     iss.clear();     iss.str(line);     int lit;     formula[c].clear();     iss >> lit;     while (lit != 0) {       assert(lit <= static_cast<int>(nbvar) && lit >= -static_cast<int>(nbvar));       formula[c].push_back(lit);       iss >> lit;     }     c++;   } while (true);   assert(c == nbclauses); }

  Note the use of the function push_back for dynamic vectors from the STL. We added assertions to ensure the data are consistent. These assertions can be disabled by defining the variable NDEBUG. A way to do this is by adding a declaration in the Makefile: COMPOPTS = $(COMPOPTS) -DNDEBUG. You should check that the instance is correctly read. To do this there is an implementation of the operator << of the class SAT_Input.

  ostream& operator<<(ostream& os, const SAT_Input& pa) { // Insert the code that write the input object (needed for debugging purposes)   for (unsigned int c=0;c<pa.nbclauses;c++) {     for (unsigned int l=0;l<pa.formula[c].size();l++)       os<<pa.formula[c][l]<<" ";     os<<endl;   }   return os; }

  Once this function is implemented it is possible to check the output using the EasyLocal menu. From the starting menu select (1) Random state then (4) State menu and finally (7) Show input. This should call the friend operator implemented above and print the input data. Of course, the good old way of testing by adding in the code debugging lines that print on standard output relevant data is also a worth practice.

• We can now run our program with:

  xyz --main::instance data/uf20-010.cnf --main::method mymethod
  

  However, nothing is implemented yet for the local search. This is left to you.

Instructions for the Submissions at the Web Page

Start early to test your submission. You can submit as many times as you wish within the deadline. Every new valid submission overwrites the previous submission.

Your archive must uncompress as follows:

• src/ the source files that implement the algorithm
• src/Makefile to compile the sources in src and produce an executable called xyz.
• doc/ where you put a pdf version of the description.
• Makefile the makefile given with the initial package.

Your program will be compiled calling make xyz. Hence make sure that your Makefile is present and that it has the task xyz. Use the same Makefile as the one that has been delivered in the Practice. In particular, make sure that there is the following include:

 include ./make.local

Use make.local to set the path to the EasyLocal library and to the Boost library. The executable file xyz generated in src will be used for the tests. Locally, you are recommended to have additionally the following content, which however you do not need to submit:

• data/ containing the test instances.
• res/ containing your results, the performance measurements
• r/ statistics, data analysis, visualization
• doc/ a description of the algorithms.
• log/ other log files produced by the run of the algorithm

To prepare your submission create an archive as follows:

tar czvf sat.tgz src doc

Any other type of archive will not work.

The programs will run on a machine with ubuntu 14.04.

The executable xyz must run with the default arguments of easylocal. In particular, the instance, the output file and the seed will be specified.

xyz --main::instance ../data/uf20-010.cnf --main::output_file uf20-010.sol --main::seed 1

No other parameter can be specified. If you have any, then you will need to hard code them. You can do this as follows. For main parameters just add in the main file, for example:

method="SD";

For other parameters, pass them to the SearchEngine or Solvers. For example, you will need to set the time limit by passing it to the Parametrized instance of SimpleLocalSearch:

SAT_solver.SetParameter("timeout",20.0);

The program will be killed externally at the time limit if it did not terminate already. Hence make sure you hard code the time limit and that you output in time the best solution found during the search.

All output must go in the standard output and in the output file. Do not create other files. The files must be in ASCII format and the output file must contain the solution certificate in the format described above. The output class to produce the output is already implemented but you need to pass your solution to an object of this class. Your solutions will be verified by an external program. You find this program in your start package. You can compile (make verifier) and use it.

Make sure you report the following three result data:

• solution certificate (in output_file)
• its quality, ie, cost
• the computation time to find it

For example:

xyz --main::instance ../data/uf20-010.cnf  --main::seed 1
v -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 17 18 19 20 0

Cost: 10
Time: 0.00028879

It is important that you use this format and that Time: is the first word in a new line reporting the computation time. To achieve this you can make sure that in your main you have the following lines:

os << out << endl;
os << "Cost: " << result.cost << endl;
os << "Time: " << result.running_time << endl;

Note that the upload and analysis system is still under test and therefore it may have to be fine tuned, hence be patient and contact the teacher if something is not working as it should.