# 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

 TextBook Computers and Intractability: A Guide to the Theory of Np-Completeness by Michael R. Garey, David S. Johnson TextBook How to Solve It: Modern Heuristics by Zbigniew Michalewicz, David B. Fogel URL OR LIBRARY - J.E. Beasley http://mscmga.ms.ic.ac.uk/jeb/orlib/satinfo.html URL SATLIB - The Satisfiability Library http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/#intro URL A compendium of NP optimization problems http://www.nada.kth.se/~viggo/problemlist/compendium.html

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