Dynamic Initial Weight Assignment for MaxSAT
The Maximum Satisfiability (Maximum Satisfiability (MaxSAT)) approach is the choice, and perhaps the only one, to deal with most real-world problems as most of them are unsatisfiable. Thus, the search for a complete and consistent solution to a real-world problem is impractical due to computational...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2021-03-01
|
| Series: | Algorithms |
| Subjects: | |
| Online Access: | https://www.mdpi.com/1999-4893/14/4/115 |
| _version_ | 1797539358316691456 |
|---|---|
| author | Abdelraouf Ishtaiwi Qasem Abu Al-Haija |
| author_facet | Abdelraouf Ishtaiwi Qasem Abu Al-Haija |
| author_sort | Abdelraouf Ishtaiwi |
| collection | DOAJ |
| description | The Maximum Satisfiability (Maximum Satisfiability (MaxSAT)) approach is the choice, and perhaps the only one, to deal with most real-world problems as most of them are unsatisfiable. Thus, the search for a complete and consistent solution to a real-world problem is impractical due to computational and time constraints. As a result, MaxSAT problems and solving techniques are of exceptional interest in the domain of Satisfiability (Satisfiability (SAT)). Our research experimentally investigated the performance gains of extending the most recently developed SAT dynamic Initial Weight assignment technique (InitWeight) to handle the MaxSAT problems. Specifically, we first investigated the performance gains of dynamically assigning the initial weights in the Divide and Distribute Fixed Weights solver (DDFW+Initial Weight for Maximum Satisfiability (DDFW+InitMaxSAT)) over Divide and Distribute Fixed Weights solver (DDFW) when applied to solve a wide range of well-known unweighted MaxSAT problems obtained from DIMACS. Secondly, we compared DDFW+InitMaxSAT’s performance against three known state-of-the-art SAT solving techniques: YalSAT, ProbSAT, and Sparrow. We showed that the assignment of dynamic initial weights increased the performance of DDFW+InitMaxSAT against DDFW by an order of magnitude on the majority of problems and performed similarly otherwise. Furthermore, we showed that the performance of DDFW+InitMaxSAT was superior to the other state-of-the-art algorithms. Eventually, we showed that the InitWeight technique could be extended to handling partial MaxSAT with minor modifications. |
| first_indexed | 2024-03-10T12:44:55Z |
| format | Article |
| id | doaj.art-cb7845faca004372ac9a2cc3d87097d1 |
| institution | Directory Open Access Journal |
| issn | 1999-4893 |
| language | English |
| last_indexed | 2024-03-10T12:44:55Z |
| publishDate | 2021-03-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Algorithms |
| spelling | doaj.art-cb7845faca004372ac9a2cc3d87097d12023-11-21T13:36:48ZengMDPI AGAlgorithms1999-48932021-03-0114411510.3390/a14040115Dynamic Initial Weight Assignment for MaxSATAbdelraouf Ishtaiwi0Qasem Abu Al-Haija1Department of Data Science and Artificial Intelligence, Faculty of Information Technology, University of Petra, Amman 317, JordanDepartment of Data Science and Artificial Intelligence, Faculty of Information Technology, University of Petra, Amman 317, JordanThe Maximum Satisfiability (Maximum Satisfiability (MaxSAT)) approach is the choice, and perhaps the only one, to deal with most real-world problems as most of them are unsatisfiable. Thus, the search for a complete and consistent solution to a real-world problem is impractical due to computational and time constraints. As a result, MaxSAT problems and solving techniques are of exceptional interest in the domain of Satisfiability (Satisfiability (SAT)). Our research experimentally investigated the performance gains of extending the most recently developed SAT dynamic Initial Weight assignment technique (InitWeight) to handle the MaxSAT problems. Specifically, we first investigated the performance gains of dynamically assigning the initial weights in the Divide and Distribute Fixed Weights solver (DDFW+Initial Weight for Maximum Satisfiability (DDFW+InitMaxSAT)) over Divide and Distribute Fixed Weights solver (DDFW) when applied to solve a wide range of well-known unweighted MaxSAT problems obtained from DIMACS. Secondly, we compared DDFW+InitMaxSAT’s performance against three known state-of-the-art SAT solving techniques: YalSAT, ProbSAT, and Sparrow. We showed that the assignment of dynamic initial weights increased the performance of DDFW+InitMaxSAT against DDFW by an order of magnitude on the majority of problems and performed similarly otherwise. Furthermore, we showed that the performance of DDFW+InitMaxSAT was superior to the other state-of-the-art algorithms. Eventually, we showed that the InitWeight technique could be extended to handling partial MaxSAT with minor modifications.https://www.mdpi.com/1999-4893/14/4/115maximum satisfiabilitystochastic local searchartificial intelligencedynamic local searchoptimization MaxSAT |
| spellingShingle | Abdelraouf Ishtaiwi Qasem Abu Al-Haija Dynamic Initial Weight Assignment for MaxSAT Algorithms maximum satisfiability stochastic local search artificial intelligence dynamic local search optimization MaxSAT |
| title | Dynamic Initial Weight Assignment for MaxSAT |
| title_full | Dynamic Initial Weight Assignment for MaxSAT |
| title_fullStr | Dynamic Initial Weight Assignment for MaxSAT |
| title_full_unstemmed | Dynamic Initial Weight Assignment for MaxSAT |
| title_short | Dynamic Initial Weight Assignment for MaxSAT |
| title_sort | dynamic initial weight assignment for maxsat |
| topic | maximum satisfiability stochastic local search artificial intelligence dynamic local search optimization MaxSAT |
| url | https://www.mdpi.com/1999-4893/14/4/115 |
| work_keys_str_mv | AT abdelraoufishtaiwi dynamicinitialweightassignmentformaxsat AT qasemabualhaija dynamicinitialweightassignmentformaxsat |