Marco Dalla

Benjamin Provan-Bessell, Marco Dalla, Andrea Visentin et al.

Feature extraction is a fundamental task in the application of machine learning methods to SAT solving. It is used in algorithm selection and configuration for solver portfolios and satisfiability classification. Many approaches have been proposed to extract meaningful attributes from CNF instances. Most of them lack a working/updated implementation, and the limited descriptions lack clarity affecting the reproducibility. Furthermore, the literature misses a comparison among the features. This paper introduces SATfeatPy, a library that offers feature extraction techniques for SAT problems in the CNF form. This package offers the implementation of all the structural and statistical features from there major papers in the field. The library is provided in an up-to-date, easy-to-use Python package alongside a detailed feature description. We show the high accuracy of SAT/UNSAT and problem category classification, using five sets of features generated using our library from a dataset of 3000 SAT and UNSAT instances, over ten different classes of problems. Finally, we compare the usefulness of the features and importance for predicting a SAT instance's original structure in an ablation study.

R. Morelli, L. Clissa, M. Dalla et al.

Counting cells in fluorescent microscopy is a tedious, time-consuming task that researchers have to accomplish to assess the effects of different experimental conditions on biological structures of interest. Although such objects are generally easy to identify, the process of manually annotating cells is sometimes subject to arbitrariness due to the operator's interpretation of the borderline cases. We propose a Machine Learning approach that exploits a fully-convolutional network in a binary segmentation fashion to localize the objects of interest. Counts are then retrieved as the number of detected items. Specifically, we adopt a UNet-like architecture leveraging residual units and an extended bottleneck for enlarging the field-of-view. In addition, we make use of weighted maps that penalize the errors on cells boundaries increasingly with overcrowding. These changes provide more context and force the model to focus on relevant features during pixel-wise classification. As a result, the model performance is enhanced, especially in presence of clumping cells, artifacts and confounding biological structures. Posterior assessment of the results with domain experts confirms that the model detects cells of interest correctly. The model demonstrates a human-level ability inasmuch even erroneous predictions seem to fall within the limits of operator interpretation. This qualitative assessment is also corroborated by quantitative metrics as an ${F_1}$ score of 0.87. Despite some difficulties in interpretation, results are also satisfactory with respect to the counting task, as testified by mean and median absolute error of, respectively, 0.8 and 1.