 |
MAX-SAT
MAX-SAT
edited by Thomas Stützle and Luis Paquete, INTELLEKTIK
Contents
About MAX-SAT
Given n binary variables x(j), j in N, m
clauses C_i, i in
M, and weights w(i), where N={1,2,... ,n} and M={1,2,
...,m}, the MAX-SAT problem asks to determine a binary tuple
(that is, a 0-1 assignment to each of the binary variables) that
maximizes the sum of the weights of the satisfied clauses. Each clause
is a disjunction of literals l*(j), where a literal is either a
variable x(j) (that is, the variable occurs in positive form) or its
negation neg x(j) (that is, the variable occurs in negative
form). Without loss of generality we assume that at most one of x(j)
and neg x(j) is included in each clause. A clause is satisfied if at
least one of the positive variables contained in the clause is
assigned the value 1 (true) or a negated variable is assigned the
value 0 (false).
Given a set of clauses, MAX-SAT is the problem to find a variable
assignment that maximizes the weight of satisfied clauses. Note that
alternatively, the objective function could have been defined to
minimize the weight of the unsatisfied clauses, as it is often done in
the literature.
If all the weights are equal to one, we call the resulting problem
unweighted MAX-SAT, otherwise we speak of weighted MAX-SAT or simply
MAX-SAT. The unweighted MAX-SAT is important, because a special case
is the SAT problem. The SAT problem is a decision problem that asks
whether a binary tuple can be found that satisfies all clauses
(corresponding to a solution of weight n). The SAT problem is a
central problem in theoretical computer science, artificial
intelligence, mathematical logic, and many applications.
Readings
-
-
R. Battiti and M. Protasi.
Reactive search, a history-based heuristic for MAX-SAT.
ACM Journal of Experimental Algorithmics, 2, 1997.
-
-
R. Battiti and M. Protasi.
Solving MAX-SAT with non-oblivious functions and history-based
heuristics.
In D. Du, J. Gu, and P.M. Pardalos, editors, Satisfiability
problem: Theory and Applications, volume~35 of DIMACS Series on
Discrete Mathematics and Theoretical Computer Science, pages 649--667.
American Mathematical Society, 1997.
-
-
A. Bertoni, P. Campadelli, M. Carpentieri, and G. Grossi.
A genetic model: Analysis and application to MAXSAT.
Evolutionary Computation, 8(3):291--309, 2000.
-
-
B. Borchers and J. Furman.
A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT
problems.
Journal of Combinatorial Optimization, 2(4):299--306, 1999.
-
-
P. Hansen and B. Jaumard.
Algorithms for the maximum satisfiability problem.
Computing, 44:279--303, 1990.
-
-
P. Hansen, B. Jaumard, N. Mladenovic, and A.D. Parreira.
Variable neighbourhood search for maximum weighted satisfiability
problem.
Technical Report G-2000-62, Les Cahiers du GERAD, Group for Research
in Decision Analysis, 2000.
-
-
Y. Jiang, H. Kautz, and B. Selman.
Solving problems with hard and soft constraints using a stochastic
algorithm for MAX-SAT.
In Proceedings of the 1st International Joint Workshop on
Artificial Intelligence and Operations Research, 1995.
-
-
S. Joy, J. Mitchell, and B. Borchers.
A branch and cut algorithm for MAX-SAT and weighted MAX-SAT.
In D. Du, J. Gu, and P.M. Pardalos, editors, Satisfiability
problem: Theory and Applications}, volume 35 of DIMACS Series on
Discrete Mathematics and Theoretical Computer Science, pages 519--536.
American Mathematical Society, 1997.
-
-
D. McAllester, B. Selman, and H. Kautz.
Evidence for invariants in local search.
In Proceedings of the 14th National Conference on Artificial
Intelligence, pages 321--326. AAAI Press / The MIT Press, Menlo Park, CA,
USA, 1997.
-
-
P. Mills and E. Tsang.
Guided local search for solving SAT and weighted MAX-SAT
problems.
In I.P. Gent, H. van Maaren, and T. Walsh, editors, SAT2000 ---
Highlights of Satisfiability Research in the Year 2000, pages 89--106. IOS
Press, Amsterdam, The Netherlands, 2000.
-
-
M.G.C. Resende, L.S. Pitsoulis, and P.M. Pardalos.
Approximate solution of weighted MAX-SAT problems using GRASP.
In D. Du, J. Gu, and P.M. Pardalos, editors, Satisfiability
problem: Theory and Applications, volume 35 of DIMACS Series on
Discrete Mathematics and Theoretical Computer Science, pages 393--405.
American Mathematical Society, 1997.
-
-
A. Roli and C. Blum.
Critical parallelization of local search for MAX-SAT.
In Procedings of AI*IA, 7th Congress of the Italian Association
of Artificial Itnelligence, 2001.
-
-
B. Selman, H.A. Kautz, and B. Cohen.
Noise strategies for improving local search.
In Proceedings of the 12th National Conference on Artificial
Intelligence, pages 337--343. AAAI Press / The MIT Press, Menlo Park, CA,
USA, 1994.
-
-
B. Selman, H. Levesque, and D. Mitchell.
A new method for solving hard satisfiability problems.
In Proceedings of the 10th National Conference on Artificial
Intelligence, pages 440--446. AAAI Press / The MIT Press, Menlo Park, CA,
USA, 1992.
-
-
Y. Shang and B.W. Wah.
Discrete lagrangian-based search for solving MAX-SAT problems.
In Proceedings of the 15th International Joint Conference on
Artificial Intelligence, volume 1, pages 378--383. Morgan Kaufmann
Publishers, San Francisco, CA, USA, 1997.
-
-
M. Yagiura and T. Ibaraki.
Efficient 2 and 3-flip neighborhoods seach algorithms for the MAX
SAT.
In W.-L. Hsu and M.-Y. Kao, editors, Computing and
Combinatorics, volume 1449 of Lecture Notes in Computer Science, pages
105--116. Springer Verlag, Berlin, Germany, 1998.
-
-
M. Yagiura and T. Ibaraki.
Analyses on the 2 and 3-flip neighborhoods for the MAX SAT.
In Journal of Combinatorial Optimization}, 3:95--114, 1999.
Links
|
