# Dynamic Initial Weight Assignment for MaxSAT
## 4 Experimental Results and Analyses
### Problem Sets and the General Problem Structure  
We obtained four sets of problems studied in our research from the SATLIB library and the pigeon hole, the AIM, the jnh, and the uuf set (for more details, see [[https://www.cs.ubc.ca/~hoos/SATLIB/benchmark.html](https://www.cs.ubc.ca/~hoos/SATLIB/benchmark.html)]([https://www.cs.ubc.ca/~hoos/SATLIB/benchmark.html](https://www.cs.ubc.ca/~hoos/SATLIB/benchmark.html)), accessed on 9 March 2021). **pigeon hole problem set:** The pigeon hole problems are based on placing \(n\) number of pigeons in \(n+1\) holes. The set contains five SAT encoded benchmarks that vary in the number of holes from six to ten. The pigeon hole problem set's encoding is as follows: assuming there are \(i\) number of holes and \(j\) number of pigeons that must be placed in \(i\), then \(n+1\) number of clauses are generated to ensure a pigeon is put in some hole, and a group of clauses is added to ensure a pigeon can be put in one single hole only. The resulting number of the clauses is \((n+1)+n*(n*(n+1)/2)\) and \(n*(n+1)\) the number of variables. **AIM problem set:** The aimproblems are randomly generated instances of a three-SAT class. The set contains 24 unsatisfiable instances encoded using a low clause-to-variable ratio, specifically 1.6 and 2.0 ratios for the 50 variable, 100 variable, and 200 variable instances. **jnh problem set:** The jnh 33 unsatisfiable instances obtained from SATLIB are generated as follows: given a number of variables (v), each variable is added to a clause with probability \(1/v\), and literals are negated with probability \(1/2\) (empty and unit clauses are eliminated). The resulting 33 problems contain 100 variables and between 800 and 900 clauses. **uuf problem set:** The uuf (unsatisfiable uniform) problem contains number of variables \(v\) and number of clauses \(k\). Each clause contains three randomly chosen literals from \(2v\) possible literals. Our study obtained the 49 instances of uuf from SATLIB, where each instance contained 200 variables and 1000 clauses. A comprehensive study was carried out to shed light on the structure of the above problem sets via studying the different sizes of clauses and the neighborhoods' sizes in which they were located. Table 1 reflects some of the information taken from the problem structure. In this table, we list the following records for each instance in our problem set: the number of clauses in the problem (\(\#nCls\)), the size of the average neighborhood (\(AvgNeighS\)), the percentage of the total number of clauses that have less than the average size of the neighborhood (\(<AvgNeighS\)), the percentage of the number of clauses that have an equal number of the average neighborhood size (\(=AvgNeighS\)), and the portion of the number of clauses in the instance that have greater than the average number of the average neighborhood size (\(>AvgNeighS\)). This step aimed to find the clauses' variation with small, equal, and large neighborhood sizes. Moreover, whether a large percentage of the clauses have identical or similar neighborhood sizes, this was not the case in our problem structures. In most instances, a general pattern was identified as the clauses having either a smaller or a larger neighborhood than the average neighborhood size of each problem instance. However, the pigeon instances were an exception as all the clauses had a larger than average neighborhood size, as Table 1 illustrates.