The Maximum Boolean k-Satisfiability Problem

Description:

The MAX k-SAT problem is a classified NP-hard optimization problem. It can be defined as:

Input:
-A Boolean Formula F in CNF wich contains:
- A set U of variables: {P,Q,...}
- A collection C of disjunctive clauses of literals, where a literal is a variable or a negated variable in U.

Output:
-A truth assignment for U.

Question

Given a boolean formula F expressed in CNF (Conjunctive Normal Form), find the truth assignment for the variables of F that maximizes the number of clauses satisfied by this assignment.

One boolean formula is expressed in Conjunctive Normal Form when it's composed by an AND-logical set of OR-logical clauses. Example:

is in CNF

Problem Instances

In order to define an instance of this problem we need to provide all the information about the boolean formula. This means: the number of literals (variables or negated variables) in each clause, the number of clauses of the formula, and the variables (positive or negative) appeared in each clause.

Related Bibliography and Papers

Last Updated: 5/06/03                                                                                                                  For any question or suggestion, click here to contact with us.