natural.
4.3 Fast Variable Partitioning
The next step we try to do is replacing the best found valid partition within 60 seconds by the first-found valid partition to reduce the run-time of variable partition step.
Figure 4.4: First-found valid partition – without minimal UNSAT core refinement
Figures 4.4 and 4.5 show the disjointness and balancedness of the first-found valid partition without and with the minimal UNSAT core refinement process. Every spot in the figures corresponds to a test case from the single- and two-output Ashenhurst decomposition in our experiments. As can be seen, for the partition results without
4.3. Fast Variable Partitioning
Figure 4.5: First-found valid partition – with minimal UNSAT core refinement
minimal UNSAT core refinement, the results of first-found valid partition has fewer points close to the origin compare to the best found variable partition in 60 seconds.
It reveals that our partition technique without minimal UNSAT core refinement may not catch the local optimal solution in the first-found valid partition.
By introducing the minimal UNSAT core refinement process, there are more points close to the origin. That means the partition results are more balancedness and disjointness. After apply the minimal UNSAT core refinement process to the first-found valid partition, there are 37.23% improvement on disjointness but 19.44%
balancedness loss (balancedness from 4.89% to 5.84%). Even though the ratio of balancedness loss seems high, but the actual value of balancedness is still very low.
Since the minimal UNSAT core refinement process improved the quality of
first-4.3. Fast Variable Partitioning
found valid partition, we are now interested in comparing the partition results of first-found valid partition with minimal UNSAT core process with the results of best found partition within 60 seconds without minimal UNSAT core process. One fact we observed is, for partition results of first-found valid partition with minimal UNSAT core process, which shows in Figure 4.5, the quantity of those points close to the origin is even more than the quantity of those in Figure 4.1, which corresponds to the best found partition in 60 seconds without minimal UNSAT core refinement process. It reveals that these two partition efforts have comparable qualities.
We next analyze the number of SAT solving needed between first valid partition with UNSAT core refinement and best partition within 60 seconds without UNSAT core refinement. Recall that in average, we need 3 seed partitions tried to find the first valid partition, in contrast to 1337 seed partitions tried in 60 seconds. In the other hand, the number of SAT solving we need in minimal UNSAT core refinement process is exactly the number of XC variables. The maximum cardinality of XC is no more than the number of input variables (in our experiments, the maximum number of input variables is 308).
The above analysis shows that the disjointness and balancedness of the first-found valid partition with minimal UNSAT core refinement process are comparable to the results of best found partition in 60 seconds without minimal UNSAT core operation. However the number of SAT solving needed is four times less. Hence if the timing cost of the partition process is asked to be small, the minimal UNSAT
4.3. Fast Variable Partitioning
core refinement process is a non-sacrificed procedure in the partition step.
Table 4.3: Variable distribution in different partition efforts
effort XG XH XGH XC
first 0.013 0.087 0.259 0.641 first mini 0.128 0.186 0.261 0.425 60 0.049 0.291 0.261 0.399 60 mini 0.141 0.342 0.262 0.255
Table 4.3 shows the average variable distribution of first-found valid partition and best found partition in 60 seconds. For example, the average XGdistribution is calculated as average|XG|/average|X|. Note that the term “mini” here indicates the results with minimal UNSAT core refinement process. The column XG, XH, and XC indicate the percentage of variables which belong to the variable partition XG, XH and XC, respectively. The column XGH indicates the percentage of variables which belong to either XG or XH partition. From the results, there are more variables strictly in XH than in XG no matter what different partition efforts we applied.
There are almost one fourth of variables can be either in XH or XG, these free variables can be used to establish a more balanced partition. One thing we have to mention here is that, in our experiment, when evaluating disjointness and balanced, we let each XGH variable be either in XH or XG such that the variable partition will be more balanced.
4.3. Fast Variable Partitioning
From Table 4.3, we know the fact that for average disjointness, the first-found valid partition with minimal UNSAT core operation and the best found partition in 60 seconds without minimal UNSAT core operation have almost the same value.
The difference is less than 2.6%. We further use Figure 4.6 to demonstrate that not only for average disjointness but also for the disjointness for every test case, no any partition effort dominates another. The x-axis indicates the disjointness of first-found valid partition with minimal UNSAT core operation. The y-axis is the value for best found partition in 60 seconds without minimal UNSAT core operation. Also, every spot in the figure corresponds to a test case from the single- and two-output Ashenhurst decomposition in our experiments.
Figure 4.6: Comparison of disjointness between different partition efforts
We have mentioned that if the timing cost is asked to be small, the minimal UNSAT core refinement process is a non-sacrificed operation in the partition step.
4.3. Fast Variable Partitioning
Figure 4.7: Comparison of disjointness between different partition efforts
Figure 4.8: Disjointness versus total variables of the best found partition in 60 seconds with minimal UNSAT core operation