Pseudo-Boolean Proof Logging for Optimal Classical Planning

We introduce lower-bound certificates for classical planning tasks, which can be used to prove the unsolvability of a task or the optimality of a plan in a way that can be verified by an independent third party. We describe a general framework for generating lower-bound certificates based on pseudo-Boolean constraints, which is agnostic to the planning algorithm used. As a case study, we show how to modify the $A^{*}$ algorithm to produce proofs of optimality with modest overhead, using pattern database heuristics and $h^\textit{max}$ as concrete examples. The same proof logging approach works for any heuristic whose inferences can be efficiently expressed as reasoning over pseudo-Boolean constraints.

Three-Dimensional Coherent Diffractive Imaging of Isolated Faceted Nanostructures

The structure and dynamics of isolated nanosamples in free flight can be directly visualized via single-shot coherent diffractive imaging using the intense and short pulses of X-ray free-electron lasers. Wide-angle scattering images even encode three-dimensional morphological information of the samples, but the retrieval of this information remains a challenge. Up to now, effective three-dimensional morphology reconstructions from single shots were only achieved via fitting with highly constrained models, requiring a priori knowledge about possible geometrical shapes. Here we present a much more generic imaging approach. Relying on a model that allows for any sample morphology described by a convex polyhedron, we reconstruct wide-angle diffraction patterns from individual silver nanoparticles. In addition to known structural motives with high symmetries, we retrieve imperfect shapes and agglomerates which were not accessible previously. Our results open new routes towards true 3D structure determination of single nanoparticles and, ultimately, 3D movies of ultrafast nanoscale dynamics.