In
computational complexity theory
In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved ...
, the maximum satisfiability problem (MAX-SAT) is the problem of determining the maximum number of clauses, of a given
Boolean formula in
conjunctive normal form
In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a cano ...
, that can be made true by an assignment of truth values to the variables of the formula. It is a generalization of the
Boolean satisfiability problem
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
, which asks whether there exists a truth assignment that makes all clauses true.
Example
The conjunctive normal form formula
:
is not satisfiable: no matter which truth values are assigned to its two variables, at least one of its four clauses will be false.
However, it is possible to assign truth values in such a way as to make three out of four clauses true; indeed, every truth assignment will do this.
Therefore, if this formula is given as an instance of the MAX-SAT problem, the solution to the problem is the number three.
Hardness
The MAX-SAT problem is
NP-hard, since its solution easily leads to the solution of the
boolean satisfiability problem
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
, which is
NP-complete
In computational complexity theory, a problem is NP-complete when:
# it is a problem for which the correctness of each solution can be verified quickly (namely, in polynomial time) and a brute-force search algorithm can find a solution by trying ...
.
It is also difficult to find an
approximate solution of the problem, that satisfies a number of clauses within a guaranteed
approximation ratio
An approximation is anything that is intentionally similar but not exactly equal to something else.
Etymology and usage
The word ''approximation'' is derived from Latin ''approximatus'', from ''proximus'' meaning ''very near'' and the prefix ' ...
of the optimal solution. More precisely, the problem is
APX
In computational complexity theory, the class APX (an abbreviation of "approximable") is the set of NP optimization problems that allow polynomial-time approximation algorithms with approximation ratio bounded by a constant (or constant-factor ap ...
-complete, and thus does not admit a
polynomial-time approximation scheme
In computer science (particularly algorithmics), a polynomial-time approximation scheme (PTAS) is a type of approximation algorithm for optimization problems (most often, NP-hard optimization problems).
A PTAS is an algorithm which takes an insta ...
unless P = NP.
Weighted MAX-SAT
More generally, one can define a weighted version of MAX-SAT as follows: given a conjunctive normal form formula with non-negative weights assigned to each clause, find truth values for its variables that maximize the combined weight of the satisfied clauses. The MAX-SAT problem is an instance of weighted MAX-SAT where all weights are 1.
Approximation algorithms
1/2-approximation
Randomly assigning each variable to be true with probability 1/2 gives an
expected 2-approximation. More precisely, if each clause has at least variables, then this yields a (1 − 2
−)-approximation. This algorithm can be
derandomized using the
method of conditional probabilities.
(1-1/)-approximation
MAX-SAT can also be expressed using an
integer linear program (ILP). Fix a conjunctive normal form formula with variables
1,
2, ...,
n, and let denote the clauses of . For each clause in , let
+ and
− denote the sets of variables which are not negated in , and those that are negated in , respectively. The variables
of the ILP will correspond to the variables of the formula , whereas the variables
will correspond to the clauses. The ILP is as follows:
The above program can be
relaxed to the following linear program :
The following algorithm using that relaxation is an expected (1-1/
e)-approximation:
# Solve the linear program and obtain a solution
# Set variable to be true with probability
where
is the value given in .
This algorithm can also be derandomized using the method of conditional probabilities.
3/4-approximation
The 1/2-approximation algorithm does better when clauses are large whereas the (1-1/)-approximation does better when clauses are small. They can be combined as follows:
# Run the (derandomized) 1/2-approximation algorithm to get a truth assignment .
# Run the (derandomized) (1-1/e)-approximation to get a truth assignment .
# Output whichever of or maximizes the weight of the satisfied clauses.
This is a deterministic factor (3/4)-approximation.
Example
On the formula
:
where
, the (1-1/)-approximation will set each variable to True with probability 1/2, and so will behave identically to the 1/2-approximation. Assuming that the assignment of is chosen first during derandomization, the derandomized algorithms will pick a solution with total weight
, whereas the optimal solution has weight
.
Solvers
Many exact solvers for MAX-SAT have been developed during recent years, and many of them were presented in the well-known conference on the boolean satisfiability problem and related problems, the SAT Conference. In 2006 the SAT Conference hosted the first MAX-SAT evaluation comparing performance of practical solvers for MAX-SAT, as it has done in the past for the
pseudo-boolean satisfiability problem and the
quantified boolean formula In computational complexity theory, the language TQBF is a formal language consisting of the true quantified Boolean formulas. A (fully) quantified Boolean formula is a formula in quantified propositional logic where every variable is quantified ( ...
problem.
Because of its NP-hardness, large-size MAX-SAT instances cannot in general be solved exactly, and one must often resort to
approximation algorithms
and
heuristics
A heuristic (; ), or heuristic technique, is any approach to problem solving or self-discovery that employs a practical method that is not guaranteed to be optimal, perfect, or rational, but is nevertheless sufficient for reaching an immediate, ...
There are several solvers submitted to the last Max-SAT Evaluations:
*
Branch and Bound
Branch and bound (BB, B&B, or BnB) is an algorithm design paradigm for discrete and combinatorial optimization problems, as well as mathematical optimization. A branch-and-bound algorithm consists of a systematic enumeration of candidate solut ...
based: Clone, MaxSatz (based on
Satz), IncMaxSatz, IUT_MaxSatz, WBO, GIDSHSat.
* Satisfiability based: SAT4J, QMaxSat.
* Unsatisfiability based: msuncore, WPM1, PM2.
Special cases
MAX-SAT is one of the optimization extensions of the
boolean satisfiability problem
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
, which is the problem of determining whether the variables of a given
Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. If the clauses are restricted to have at most 2 literals, as in
2-satisfiability
In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case ...
, we get the
MAX-2SAT problem. If they are restricted to at most 3 literals per clause, as in
3-satisfiability
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
, we get the
MAX-3SAT problem.
Related problems
There are many problems related to the satisfiability of conjunctive normal form Boolean formulas.
*
Decision problem
In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm wheth ...
s:
**
2SAT
In computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied scien ...
**
3SAT
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies ...
* Optimization problems, where the goal is to maximize the number of clauses satisfied:
** MAX-SAT, and the corresponded weighted version
Weighted MAX-SAT
** MAX-SAT, where each clause has exactly variables:
***
MAX-2SAT
***
MAX-3SAT
***
MAXEkSAT
** The partial maximum satisfiability problem (PMAX-SAT) asks for the maximum number of clauses which can be satisfied by any assignment of a given subset of clauses. The rest of the clauses must be satisfied.
** The soft satisfiability problem (soft-SAT), given a set of SAT problems, asks for the maximum number of those problems which can be satisfied by any assignment.
** The minimum satisfiability problem.
* The MAX-SAT problem can be extended to the case where the variables of the
constraint satisfaction problem
Constraint satisfaction problems (CSPs) are mathematical questions defined as a set of objects whose state must satisfy a number of constraints or limitations. CSPs represent the entities in a problem as a homogeneous collection of finite constr ...
belong to the set of reals. The problem amounts to finding the smallest ''q'' such that the ''q''-
relaxed intersection of the constraints is not empty.
See also
*
Boolean Satisfiability Problem
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
*
Constraint satisfaction In artificial intelligence and operations research, constraint satisfaction is the process of finding a solution through
a set of constraints that impose conditions that the variables must satisfy. A solution is therefore a set of values for th ...
*
Satisfiability modulo theories
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvi ...
External links
* http://www.satisfiability.org/
* https://web.archive.org/web/20060324162911/http://www.iiia.csic.es/~maxsat06/
* http://www.maxsat.udl.cat
Weighted Max-2-SAT Benchmarks with Hidden Optimum SolutionsLecture Notes on MAX-SAT Approximation
References
* {{Citation, last = Vazirani , first = Vijay V.
, author-link = Vijay Vazirani
, title = Approximation Algorithms
, year = 2001
, publisher = Springer-Verlag
, isbn = 978-3-540-65367-7
, url = https://doc.lagout.org/science/0_Computer%20Science/2_Algorithms/Approximation%20Algorithms%20%5bVazirani%202010-12-01%5d.pdf
Logic in computer science
Combinatorial optimization
Satisfiability problems