(either x₁ is false or x₂ is false or x₃ is true), and
(either x₁ is false or x₂ is false or x₄ is true), and
....

In order to use our tool, the above instance must be described in a file (let's call it example.cnf), with the following lines:

c Example of a .cnf file with 5 variables and 4 clauses
p cnf 5 4
-1 -2  3  0  
-1 -2  4  0
-1 -2  5  0
-3 -4 -5  0

where:

• the line beginning with `c` (the first line) is a comment,
• the line beginning with `p` describes the file format (cnf), the number of variables (5) and the number of clauses (4)
• the subsequent lines describe the clauses (one line for each clause, with a list of literals terminated by `0`, and `-` in front of an index when a literal corresponds to a negated variable).

The above file must be saved in your local machine and then submitted to our solver by typing its name in the appropriate input field.

Your file will then be transferred over the Internet to our machine, our solver will be activated and, after a certain waiting time, the best truth assignment found during the entire search will be returned to you. All intermediate data, including your input file, will be cancelled.

Warning: the present code works only with MAX-3-SAT and MAX-4-SAT instances (all clauses have the same number of literals, 3 or 4, respectively)
The processing times for large instances (say 1000 variables, 10,000 clauses and 100,000 iterations) can be of some minutes (depending also on the machine load).

Let us assume that the assignment x = (1 1 1 1 1) is reached by OB local search.
It is immediate to check that x = (1 1 1 1 1) is an oblivious local optimum with one unsatisfied clause (clause-4).
While OB stops here, a possible sequence to reach the global optimum starting from x is the following:

1. x₁ is set to false
2. x₃ is set to false