Optimization Benchmarking

The MAX-3SAT Example

Here we use the optimizationBenchmarking.org framework to investigate the results of some simple algorithms applied to the MAX-3SAT problem.

1. Example Structure

This example is structured as follows

  1. The archive results.zip contains the results of six simple hill climbing setups with different operators and restart policies on the selected MAX-3SAT problem instances.
  2. The archive results-meatadata-1.0.zip contains the meta data about the algorithm setups, benchmark instances, and measurement dimensions. This data tells the system what algorithm parameter values were applied in the experiments, what features the benchmark instances have, and what the structure of the result text files is.
  3. The file evaluation.xml contains an example evaluation definition. We apply a set of different modules and configurations.
  4. The file configForIEEEEtran.xml is a configuration that applies evaluation.xml to the results and renders the output as LaTeX document styled according to IEEEtran.cls into a folder named reports/LaTeX/IEEEtran/.
  5. The file configForLNCS.xml is a configuration that applies evaluation.xml to the results and renders the output as LaTeX document styled according to LLNCS.cls into a folder named reports/LaTeX/LNCS/.
  6. The file configForSigAlternate.xml is a configuration that applies evaluation.xml to the results and renders the output as LaTeX document styled according to sig-alternate.cls into a folder named reports/LaTeX/SigAlternate/.
  7. The file configForXHTML.xml is a configuration that applies evaluation.xml to the results and renders the output as XHTML document into a folder named reports/XHTML/.
  8. The file configForExport.xml is a configuration that applies evaluation.xml to the results and renders the output as text (for import into other tools) into a folder named reports/export/.
  9. The archive benchmarks.zip contains some benchmark instances for the MAX-3SAT problem from the popular SATLIB benchmark instance set. This is just for information, you don’t need that for the automatic evaluation of the experiments.
  10. The archive sources.zip contains some simple Java “solvers” to solve these MAX-3SAT instances. These “solvers” (notice the quotes) are not an attempt to actually solve the problems well - they are quite stupid and primitive. But they are easy to understand, which is the goal of the example. They also illustrate how data can be gathered in log files which can later be loaded into the evaluator. This is just for information, you don’t need that for the automatic evaluation of the experiments.

2. The MAX-3SAT Problem

MAX-3SAT is an optimization problem where we want to find a way to satisfy a Boolean function of a specific structure. “Satisfy” means to find a setting for its (Boolean) input values so that its (Boolean) output becomes true. If there is no such setting, well, at least we want to make as many of its components (“clauses”) to become true. The Boolean functions considered here are in conjunctive normal form, meaning they are an and combination of several smaller ors. Moreover, each of these ors has exactly three inputs, which come from the inputs or negated inputs of the overall formula. In particular, such a formula f(x1, x2, x3, x4) could look like

f(x1, x2, x3, x4) = (x1 or x2 or (not x3)) and (x2 or (not x3) or x4) and ((not x1) or x2 or (not x4))

This formula has four variables (x1, x2, x3, and x4) and three clauses. If can become true if x2 is true (as it appears in each or without negation), in which case the other variables don’t matter. For problems more variables and clauses, it becomes much harder to find a solution or to find the variable setting making the most clauses become true. Matter of fact, MAX-3SAT is NP-hard.

As benchmark problems for our Maximum 3 Satisfiability example, we use some instances from the well-known SATLib obtained from http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html [1], as we describe in the README.md file in the benchmark folder.

3. Benchmark Problems for the MAX-3SAT Example

As benchmark problems for our Maximum 3 Satisfiability example, we use some instances from the well-known SATLib obtained from http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html [1].

3.1. Selected Instances

In particular, we pick the first ten instances of each of the following uniform random 3-SAT benchmark sets:

  1. uf20-91: 20 variables, 91 clauses - first 10 of 1000 instances, all satisfiable, all MAX 3-SAT
  2. uf50-218: 50 variables, 218 clauses - first 10 of 1000 instances, all satisfiable, all MAX 3-SAT
  3. uf75-325: 75 variables, 325 clauses - first 10 of 100 instances, all satisfiable
  4. uf100-430: 75 variables, 325 clauses - first 10 of 100 instances, all satisfiable, all MAX 3-SAT
  5. uf125-538: 100 variables, 430 clauses - first 10 of 1000 instances, all satisfiable, all MAX 3-SAT
  6. uf150-645: 150 variables, 645 clauses - first 10 of 100 instances, all satisfiable, all MAX 3-SAT
  7. uf175-753 175 variables, 753 clauses - first 10 of 100 instances, all satisfiable, all MAX 3-SAT
  8. uf200-860: 200 variables, 860 clauses - first 10 of 100 instances, all satisfiable, all MAX 3-SAT
  9. uf225-960: 225 variables, 960 clauses - first 10 of 100 instances, all satisfiable, all MAX 3-SAT
  10. uf250-1065: 250 variables, 1065 clauses - first 10 of 100 instances, all satisfiable, all MAX 3-SAT

3.2. Instance Features

Our instances have two features:

  1. The number of variables
  2. The number of clauses (which here is a function of the number of variables)

References

  1. Holger H. Hoos and Thomas Stützle: SATLIB: An Online Resource for Research on SAT. In: Ian P.Gent, Hans van Maaren, and Tobi Walsh, editors, SAT 2000, pp.283-292, Amsterdam, The Netherlands: IOS Press, 2000. SATLIB is available online at www.satlib.org.

[home] • [status] • [atom feed] • [rss feed]

Contact: Dr.  Thomas Weise, http://www.it-weise.de, tweise@ustc.edu.cn