الفهرس 
On the weighted partial maximum satis ability problem
ABSTRACTOnly 14 pages are availabe for public view
 |  | from | 211 |  |  |
| | | from | 211 | | |
Abstract
This thesis is concerned with the Weighted Partial Maximum Satis- ability problem (WPMax-SAT). Let z = zS{u222A}zH be a Boolean formula such that zS = {(C1, w1), . . . , (Cs, ws)} and zH = {(Cs+1, {u221E}), . . . , (Cs+h, {u221E})}, Ci, (1 {u2264} i {u2264} s + h) are clauses and wj, (1 {u2264} j {u2264} s + h) (called weights) is either a natural number or {u221E}. The WPMax-SAT problem for z is nding an assignment that satis es all the hard clauses and maximizes the sum of the weights of the soft clauses. We dis- cuss four aspects of WPMax-SAT. The rst is the computational complexity of the problem from the classical and the parametrized perspectives. Secondly, the two solving techniques of WPMax-SAT: branch and bound and SAT-based methods. Third, our experimental investigation on a number of selected solvers. Finally, the applica- tions of WPMax-SAT in real-life.