-
Certified MaxSAT Preprocessing
Authors:
Hannes Ihalainen,
Andy Oertel,
Yong Kiam Tan,
Jeremias Berg,
Matti Järvisalo,
Jakob Nordström
Abstract:
Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-hard optimization problems, but ensuring correctness of MaxSAT solvers has remained an important concern. For SAT, this is largely a solved problem thanks to the use of proof logging, meaning that solvers emit machine-verifiable proofs…
▽ More
Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-hard optimization problems, but ensuring correctness of MaxSAT solvers has remained an important concern. For SAT, this is largely a solved problem thanks to the use of proof logging, meaning that solvers emit machine-verifiable proofs of (un)satisfiability to certify correctness. However, for MaxSAT, proof logging solvers have started being developed only very recently. Moreover, these nascent efforts have only targeted the core solving process, ignoring the preprocessing phase where input problem instances can be substantially reformulated before being passed on to the solver proper. In this work, we demonstrate how pseudo-Boolean proof logging can be used to certify the correctness of a wide range of modern MaxSAT preprocessing techniques. By combining and extending the VeriPB and CakePB tools, we provide formally verified, end-to-end proof checking that the input and preprocessed output MaxSAT problem instances have the same optimal value. An extensive evaluation on applied MaxSAT benchmarks shows that our approach is feasible in practice.
△ Less
Submitted 26 April, 2024;
originally announced April 2024.
-
Visual Analysis of Multiple Dynamic Sensitivities along Ascending Trajectories in the Atmosphere
Authors:
Christoph Neuhauser,
Maicon Hieronymus,
Michael Kern,
Marc Rautenhaus,
Annika Oertel,
Rüdiger Westermann
Abstract:
Numerical weather prediction models rely on parameterizations for subgrid-scale processes, e.g., for cloud microphysics. These parameterizations are a well-known source of uncertainty in weather forecasts that can be quantified via algorithmic differentiation, which computes the sensitivities of prognostic variables to changes in model parameters. It is particularly interesting to use sensitivitie…
▽ More
Numerical weather prediction models rely on parameterizations for subgrid-scale processes, e.g., for cloud microphysics. These parameterizations are a well-known source of uncertainty in weather forecasts that can be quantified via algorithmic differentiation, which computes the sensitivities of prognostic variables to changes in model parameters. It is particularly interesting to use sensitivities to analyze the validity of physical assumptions on which microphysical parameterizations in the numerical model source code are based. In this article, we consider the use case of strongly ascending trajectories, so-called warm conveyor belt trajectories, known to have a significant impact on intense surface precipitation rates in extratropical cyclones. We present visual analytics solutions to analyze interactively the sensitivities of a selected prognostic variable, i.e. rain mass density, to multiple model parameters along such trajectories. We propose a visual interface that enables to a) compare the values of multiple sensitivities at a single time step on multiple trajectories, b) assess the spatio-temporal relationships between sensitivities and the shape and location of trajectories, and c) a comparative analysis of the temporal development of sensitivities along multiple trajectories. We demonstrate how our approach enables atmospheric scientists to interactively analyze the uncertainty in the microphysical parameterizations, and along the trajectories, with respect to a selected prognostic variable. We apply our approach to the analysis of convective trajectories within the extratropical cyclone "Vladiana", which occurred between 22-25 September 2016 over the North Atlantic.
△ Less
Submitted 29 September, 2022; v1 submitted 2 May, 2022;
originally announced May 2022.
-
Augmenting Visual Place Recognition with Structural Cues
Authors:
Amadeus Oertel,
Titus Cieslewski,
Davide Scaramuzza
Abstract:
In this paper, we propose to augment image-based place recognition with structural cues. Specifically, these structural cues are obtained using structure-from-motion, such that no additional sensors are needed for place recognition. This is achieved by augmenting the 2D convolutional neural network (CNN) typically used for image-based place recognition with a 3D CNN that takes as input a voxel gri…
▽ More
In this paper, we propose to augment image-based place recognition with structural cues. Specifically, these structural cues are obtained using structure-from-motion, such that no additional sensors are needed for place recognition. This is achieved by augmenting the 2D convolutional neural network (CNN) typically used for image-based place recognition with a 3D CNN that takes as input a voxel grid derived from the structure-from-motion point cloud. We evaluate different methods for fusing the 2D and 3D features and obtain best performance with global average pooling and simple concatenation. On the Oxford RobotCar dataset, the resulting descriptor exhibits superior recognition performance compared to descriptors extracted from only one of the input modalities, including state-of-the-art image-based descriptors. Especially at low descriptor dimensionalities, we outperform state-of-the-art descriptors by up to 90%.
△ Less
Submitted 16 July, 2020; v1 submitted 29 February, 2020;
originally announced March 2020.
