Maximum Satisfiability Approach to Game Theory and Network Security
Xiaojuan Liao · Institutional Repositories DataBase (IRDB) · 2014
The problem of determining whether a propositional Boolean formula can be true is called Boolean Satisfiability Problem (SAT).Maximum Satisfiability Problem (MaxSAT), as well as its extensions: partial MaxSAT, weighted MaxSAT, and weighted partial MaxSAT, are optimization versions of the famous SAT problem.To date, there have been a variety of MaxSAT applications such as planning and scheduling.This thesis is concerned with a well-suited way of representing and solving real-world problems with MaxSAT, in terms of multi-agent systems and cryptographic areas.Generally, a propositional Boolean formula is expressed in Conjunction Normal Form (CNF), which is a conjunction of clauses that are disjunctions of literals.A literal is either a positive or negative Boolean variable.Weighted partial MaxSAT (WPM) distinguishes clauses between hard and soft, where each soft clause is associated with a positive weight.The WPM problem is to satisfy all hard clauses and maximize the sum of weights of all the satisfied soft clauses.The fact that WPM only identifies positive weights sometimes becomes impediment to solve problems where positive and negative weights co-exist.To avoid this difficulty, in this thesis, an extended WPM (EWPM) for handling non-zero weights is presented and the relationship between EWPM and WPM solution is examined.The design of EWPM paves the way for a wider range of WPM First of all, I would like to acknowledge the China Scholarship Council (CSC) for awarding me the state scholarship, which covered all my living stipend in Japan during my Ph.D course.Thanks to this scholarship, I could fully devote myself to the research.I would like to thank my