The Maximum Boolean kSatisfiability Problem


Description:The MAX kSAT problem is a classified NPhard optimization problem. It can be defined as: Input: Output: 

QuestionGiven 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 ANDlogical set of ORlogical clauses. Example:


Problem InstancesIn 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


