Reactive Search: Web Service for maximum satisfiability

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 (finding whether a formula can be satisfied or not) was the first example of an NP-complete problem (considered among the most difficult to solve).

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

Step 1/2

Define your problem