In the Maximum Satisfiability (MAX-SAT) problem one looks for an assignment of truth values that maximizes the number of satisfied clauses of a boolean formula in conjunctive normal form.

Let n be the number of variables and m the number of clauses, so that the formula has the following form:

where l_c is the number of literals in clause c and p_cj is a literal, i.e., a propositional variable x_k or its negation , for 1 k n.

MAX-SAT is of considerable interest not only from the theoretical side but also from the practical one. On one hand, the decision version SAT was the first example of an NP-complete problem; moreover MAX-SAT and related variants play an important role in the characterization of different approximation classes like APX and PTAS.

On the other hand, many issues in mathematical logic and artificial intelligence can be expressed in the form of satisfiability or some of its variants, like constraint satisfaction.

The algorithm is described in:

Reactive Search, a history-sensitive heuristic for MAX-SAT R. Battiti & M. Protasi ACM Journal of Experimental Algorithmics Volume 2, Article 2, 1997 Subscribers to JEA can access the paper and software at: http://www.jea.acm.org/1997/BattitiReactive/

The paper is available in gzipped PostScript, 154KB.

---

• Tutorial and Algorithms Description
• Interactive Tool
• Benchmark instances used in the cited paper.

---

Define your problem:

• Max Sat problem file:
• Set the Number of Iterations
• Set Random Seed:

---