Constraint Programming (CP) solvers are complex pieces of software with a large surface area for bugs, making it difficult to trust their claims of unsatisfiability or optimality. We make a contribution to the development of a CP unsatisfiability proof checker, which is formally verified in Rocq, by investigating how to develop checkers for individual proof steps. In particular, we develop formally verified checkers that can verify the reasoning performed by alldifferent and cumulative timetable propagators. We also introduce a methodology for supporting other propagators and constraints in the checker. We also contribute a formally verified integer domain representation using what we call perforated intervals. Perforated intervals are designed to efficiently interoperate with atomic constraints, which are at the heart of the CP proof system. They are an important building block for the verification of proof steps that combine previous proof steps to derive new facts, which we also part of our contribution, and are also used in our propagation checkers. Our results demonstrate the feasibility of a CP-native unsatisfiability proof checker and increase the understanding of propagation verification. Our work also provides important building blocks that can be used to support additional constraints and propagators.

As super-resolution methods make it possible to capture images at a resolution beyond the diffraction limit, they have no straightforward measure for optical resolution. Consequently, signal-to-noise ratio-based methods to determine resolution such as Fourier Ring Correlation (FRC) have seen increased
use. We look at a new method, called 1FRC, as it requires only a single image instead of two (2FRC, the original method). It splits each pixel value into two values according to a binomial distribution, producing two images usable in a standard FRC routine. We consider for which noise modalities and conditions
the results are equivalent to using 2FRC. If the image noise is only Poisson-distributed we derive mathematically that 1FRC and 2FRC are equivalent. Using simulations on Siemens star test images we find that the mean squared error between 1FRC and 2FRC curves is small for images containing only Poisson noise and a combination of Poisson and low variance Gaussian noise. However, when
the mean variance ratio 𝜇/𝜎2 (image mean divided by variance of a pixel) is less than one, the 1FRC curve no longer goes to zero at high frequencies, but instead fluctuates at an elevated level. We see that this elevated 1FRC curve level is exactly 1 − 𝜇/𝜎2. For 𝜇/𝜎2 < 0.973 the difference in resolution exceeds one standard deviation of the 1FRC resolution. From this point the Kolmogorov-Smirnov test confidently states that the 1FRC pixel sum distributions are not equal to 2FRC distributions. We also test 1FRC on an experimental dataset made with varying STED intensity. The computed resolution curves fit well to the modified Abbe equation for STED. However, the 1FRC resolutions are up to 30%
better than resolutions obtained using decorrelation analysis.