Publications

CDCLSym: Introducing effective symmetry breaking in SAT solving

Abstract

SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. Static symmetry breaking is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones.This paper presents a new way to handle symmetries, that avoids the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. Extensive experiments on the benchmarks of last six SAT competitions show that our approach is competitive with the best state-of-the-art static symmetry breaking solutions.

Continue reading

Derived-term automata of multitape expressions with composition

Abstract

Rational expressions are powerful tools to define automata, but often restricted to single-tape automata. Our goal is to unleash their expressive power for transducers, and more generally, any multitape automaton; for instance $(a^+\mathbin{\vert} x + b^+\mathbin{\vert} y)^*$. We generalize the construction of the derived-term automaton by using expansions. This approach generates small automata, and even allows us to support a composition operator.

Continue reading

Advances in utilization of hierarchical representations in remote sensing data analysis

Abstract

The latest developments in sensor design for remote sensing and Earth observation purposes are leading to images always more complex to analyze. Low-level pixel-based processing is becoming unadapted to efficiently handle the wealth of information they contain, and higher levels of abstraction are required. Region-based representations intend to exploit images as collections of regions of interest bearing some semantic meaning, thus easing their interpretation. However, the scale of analysis of the images has to be fixed beforehand, which can be problematic as different applications may not require the same scale of analysis. On the other hand, hierarchical representations are multiscale descriptions of images, as they encompass in their structures all potential regions of interest, organized in a hierarchical manner. Thus, they allow to explore the image at various levels of details and can serve as a single basis for many different further processings. Thanks to its flexibility, the binary partition tree (BPT) representation is one of the most popular hierarchical representations, and has received a lot of attention lately. This article draws a comprehensive review of the most recent works involving BPT representations for various remote sensing data analysis tasks, such as image segmentation and filtering, object detection or hyperspectral classification, and anomaly detection.

Continue reading

Extraction of ancient map contents using trees of connected components

Abstract

Ancient maps are an historical and cultural heritage widely recognized as a very important source of information, but exploiting such maps is complicated. In this project, we consider the Linguistic Atlas of France (ALF), built between 1902 and 1910. This cartographical heritage produces firstrate data for dialectological researches. In this paper, we focus on the separation of the content in layers for facilitating the extraction, the analysis, the visualization and the diffusion of the data contained in these ancient linguistic atlases.

Continue reading

A tutorial on well-composedness

Abstract

Due to digitization, usual discrete signals generally present topological paradoxes, such as the connectivity paradoxes of Rosenfeld. To get rid of those paradoxes, and to restore some topological properties to the objects contained in the image, like manifoldness, Latecki proposed a new class of images, called well-composed images, with no topological issues. Furthermore, well-composed images have some other interesting properties: for example, the Euler number is locally computable, boundaries of objects separate background from foreground, the tree of shapes is well-defined, and so on. Last, but not the least, some recent works in mathematical morphology have shown that very nice practical results can be obtained thanks to well-composed images. Believing in its prime importance in digital topology, we then propose this state-of-the-art of well-composedness, summarizing its different flavours, the different methods existing to produce well-composed signals, and the various topics that are related to well-composedness.

Continue reading

SmartDoc 2017 video capture: Mobile document acquisition in video mode

Abstract

As mobile document acquisition using smartphones is getting more and more common, along with the continuous improvement of mobile devices (both in terms of computing power and image quality), we can wonder to which extent mobile phones can replace desktop scanners. Modern applications can cope with perspective distortion and normalize the contrast of a document page captured with a smartphone, and in some cases like bottle labels or posters, smartphones even have the advantage of allowing the acquisition of non-flat or large documents. However, several cases remain hard to handle, such as reflective documents (identity cards, badges, glossy magazine cover, etc.) or large documents for which some regions require an important amount of detail. This paper introduces the SmartDoc 2017 benchmark (named “SmartDoc Video Capture”), which aims at assessing whether capturing documents using the video mode of a smartphone could solve those issues. The task under evaluation is both a stitching and a reconstruction problem, as the user can move the device over different parts of the document to capture details or try to erase highlights. The material released consists of a dataset, an evaluation method and the associated tool, a sample method, and the tools required to extend the dataset. All the components are released publicly under very permissive licenses, and we particularly cared about maximizing the ease of understanding, usage and improvement.

Continue reading

Derived-term automata of weighted rational expressions with quotient operators

Abstract

Quotient operators have been rarely studied in the context of weighted rational expressions and automaton generation—in spite of the key role played by the quotient of words in formal language theory. To handle both left- and right-quotients we generalize an expansion-based construction of the derived-term (or Antimirov, or equation) automaton and rely on support for a transposition (or reversal) operator. The resulting automata may have spontaneous transitions, which requires different techniques from the usual derived-term constructions.

Continue reading

Benchmarking keypoint filtering approaches for document image matching

Abstract

Reducing the amount of keypoints used to index an image is particularly interesting to control processing time and memory usage in real-time document image matching applications, like augmented documents or smartphone applications. This paper benchmarks two keypoint selection methods on a task consisting of reducing keypoint sets extracted from document images, while preserving detection and segmentation accuracy. We first study the different forms of keypoint filtering, and we introduce the use of the CORE selection method on keypoints extracted from document images. Then, we extend a previously published benchmark by including evaluations of the new method, by adding the SURF-BRISK detection/description scheme, and by reporting processing speeds. Evaluations are conducted on the publicly available dataset of ICDAR2015 SmartDOC challenge 1. Finally, we prove that reducing the original keypoint set is always feasible and can be beneficial not only to processing speed but also to accuracy.

Continue reading

The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results

Abstract

Continue reading

PaInleSS: A framework for parallel SAT solving

Abstract

Over the last decade, parallel SAT solving has been widely studied from both theoretical and practical aspects. There are now numerous solvers that dier by parallelization strategies, programming languages, concurrent programming, involved libraries, etc. Hence, comparing the eciency of the theoretical approaches is a challenging task. Moreover, the introduction of a new approach needs either a deep understanding of the existing solvers, or to start from scratch the implementation of a new tool. We present PaInleSS: a framework to build parallel SAT solvers for many-core environments. Thanks to its genericity and modularity, it provides the implementation of basics for parallel SAT solving like clause exchanges, Portfolio and Divide-and-Conquer strategies. It also enables users to easily create their own parallel solvers based on new strategies. Our experiments show that our framework compares well with some of the best state-of-the-art solvers.

Continue reading