Generating Homogeneous Sets
- Test on entire problem set, discard insignificant cliques
- Seven significant cliques with threshold 0.125
- Compare with SPCs
- SPCs inside cliques => Homogeneous SPC
- SPC over multiple cliques => Heterogeneous SPC
- Measure ratio of intersection with size of SPC
| SPC
| Homogeneous Subset
| Problems
|
|
| 1
| 2
| 3
| 4
| 5
| 6
| 7
|
|
| SAT_EPR_CNF
| 0.00
| 0.00
| 0.00
| 0.00
| 0.00
| 0.86
| 0.00
| 139
|
| SAT_EPR_FOF
| 0.00
| 0.00
| 0.00
| 0.00
| 0.99
| 0.00
| 0.00
| 83
|
| SAT_RFO_CNF
| 0.03
| 0.00
| 0.00
| 0.00
| 0.00
| 0.57
| 0.00
| 88
|
| SAT_RFO_FOF
| 0.00
| 0.00
| 0.00
| 0.00
| 1.00
| 0.00
| 0.00
| 9
|
| THM_EPR_CNF
| 0.81
| 0.00
| 0.00
| 0.00
| 0.00
| 0.00
| 0.15
| 401
|
| THM_EPR_FOF
| 0.00
| 0.00
| 0.00
| 0.00
| 1.00
| 0.00
| 0.00
| 235
|
| _EQU_FOF
| 0.00
| 0.00
| 0.00
| 0.00
| 0.96
| 0.00
| 0.00
| 323
|
| _NEQ_FOF
| 0.00
| 0.00
| 0.00
| 0.00
| 1.00
| 0.00
| 0.00
| 21
|
| _NEQ_CNF_HRN
| 0.81
| 0.08
| 0.00
| 0.03
| 0.00
| 0.01
| 0.01
| 379
|
| _NEQ_CNF_NHN
| 0.77
| 0.08
| 0.00
| 0.06
| 0.00
| 0.00
| 0.01
| 430
|
| _SEQ_CNF_HRN
| 0.78
| 0.00
| 0.00
| 0.13
| 0.00
| 0.00
| 0.03
| 381
|
| _SEQ_CNF_NHN
| 0.88
| 0.05
| 0.00
| 0.02
| 0.00
| 0.00
| 0.02
| 1194
|
| _PEQ_CNF_NUE
| 0.80
| 0.03
| 0.00
| 0.04
| 0.00
| 0.00
| 0.05
| 122
|
| _PEQ_CNF_UEQ
| 0.00
| 0.00
| 0.85
| 0.00
| 0.00
| 0.00
| 0.00
| 424
|
| Problems
| 2418
| 128
| 359
| 119
| 656
| 174
| 118
| 4229
|
- Techniques good for most CNF theorems
- Techniques good for most FOF problems
- Heterogeneity in SAT_RFO_CNF