An Exact Algorithm for Max2Sat
(implemented by Jens Gramm)

The algorithm implemented below solves the Max2Sat problem. For a boolean formula in 2-CNF the Max2Sat problem is to determine the maximum number of simultaneously satisfiable clauses. Moreover, the algorithm computes an assignment satisfying this number of clauses. In the references given below it is shown that the algorithm has a worst case running time of O(1.0970|F|). For further information refer to these references.

Input

You are required to specify a 2-CNF formula in the following format: 

cnf2 <varno> <clano>
<lit1,1> <lit1,2>
<lit2,1> <lit2,2>
.
.
.
<litclano,1> <litclano,2>
Here <varno> and <clano> are strictly positive integers denoting the input formula's number of variables and clauses, respectively. The variables are represented by positive integers from 1 to <varno>. Consequently, the literal <litx,y>, i.e., the yth literal in the xth clause, is given as follows. For the variable x a positive occurrence is denoted by x and a negative occurrence by -x. Empty clauses are not allowed, and no clause is allowed to contain more than two literals. It follows an example of a valid formula: 

cnf2 3 5
1 -2
1 3
-2 -3
2 -1
-3 2
Instead of entering your own input formula you may also generate a random formula by clicking the "Generate Random Instance" button. The random instance contains the specified number of variables and clauses, each clause having two distinct literals.

Running the Algorithm

You are initiating the algorithm by clicking the "Start Algorithm" button. In case you want to stop the once started algorithm prior to its orderly completion, you may do so by clicking the "Interrupt Algorithm" button. Note, however, that after this interruption the shown results are only preliminary ones, i.e., the best ones found up to the point of the completion.

Results

The algorithm outputs the following information:
  • Algorithm Status:
    • Running
    • Interrupted: The algorithm was interrupted by the user. The shown result is, therefore, preliminary and not necessarily optimal.
    • Completed: The algorithm's computations are completed. The shown result is optimal for the given input formula.
    • Error: The algorithm was unable to recognize the input format.
  • Maximum number of satisfied clauses: During the run of the algorithm this number shows the currently best result. Therefore, the overall optimum is displayed after an orderly completion of the algorithm.
  • Number of nodes in the search tree: We count all inner nodes of the search tree in which a branching into at least two subcases is performed. This is a reasonable measure for the size of the search tree. Together with the number of clauses, the algorithm keeps this information updated during its run.
  • Assignment for a maximum number of satisfied clauses: An assignment is shown satisfying the number of clauses given above. It is specified by displaying the variables that are set to true. Every variable that is not displayed is set to false. It is important to note that the algorithm finds only one such assignment, not all of them.

References

J. Gramm. Exact algorithms for Max2Sat and their applications. Diplomarbeit, Universität Tübingen, October 1999 (92 pages).
J. Gramm and R. Niedermeier. Faster exact solutions for Max2Sat. In G. Bongiovanni, G. Gambosi, R. Petreschi (Eds.): Proceedings of the 4th Italian Conference on Algorithms and Complexity (CIAC 2000), Lecture Notes in Computer Science, volume number 1767, 174--186, Rome, Italy, March 2000, Springer.
31.01.2000, For comments and further information contact gramm@informatik.uni-tuebingen.de