As a measure of proportionality, it could be interesting to be able to compute the smallest quota for which a property like JR, EJR+, core is satisfied. For a committee satisfying the property the quota will be n/k or smaller (with smaller values corresponding to "more representative"), and for failures it will be larger.
For JR and EJR+, it should be possible to find this value in polynomial time by relatively straightforward adaptation of the property checking algorithms (so it is a natural place to start working there). For PJR/EJR/FJR/core, it might be possible to get this value by adding a variable to the ILP and optimizing it.
I'm unsure where this should be put. Conceptually it makes sense as a scoring function. But it could also be part of some extended output of the property checker, or be a separate property.
As a measure of proportionality, it could be interesting to be able to compute the smallest quota for which a property like JR, EJR+, core is satisfied. For a committee satisfying the property the quota will be n/k or smaller (with smaller values corresponding to "more representative"), and for failures it will be larger.
For JR and EJR+, it should be possible to find this value in polynomial time by relatively straightforward adaptation of the property checking algorithms (so it is a natural place to start working there). For PJR/EJR/FJR/core, it might be possible to get this value by adding a variable to the ILP and optimizing it.
I'm unsure where this should be put. Conceptually it makes sense as a scoring function. But it could also be part of some extended output of the property checker, or be a separate property.