SAT

A time series dissimilarity measure based on minimum jump costs

Tipo de Publicación:

Journal Article

Origen:

Journal article (Submitted)

Palabras clave:

Time series; Similarity measures; Experimental comparison; Classification

Resumen:

Time series are ubiquitous, and a measure to assess their similarity is a core part of many computational systems. Classical time series similarity measures based on dynamic time warping or the edit distance remain as the best general-purpose options, but their accuracies still leave much room for improvement. Here we propose a new approach to time series similarity based on the costs of iteratively jumping (or moving) between the sample values of two time series. We show that this approach can be very competitive when compared against the aforementioned classical measures. In fact, extensive experiments show that it can be statistically significantly superior for a number of data sources. Since the approach is also intuitive and computationally simple, we foresee its application as an alternative off-the-shelf tool to be used in time series retrieval, clustering, or classification systems.

Towards Industrial-Like Random SAT Instances

Tipo de Publicación:

Conference Paper

Origen:

Proc. of the 21st Int. Joint Conf. on Artificial Intelligence, IJCAI'09, AAAI Press, Pasadena, California, p.387-392 (2009)

Palabras clave:

SAT

Resumen:

We focus on the random generation of SAT instances that have computational properties that are similar to real-world instances. It is known that industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. This is not possible, in general, with classical randomly generated instances. We provide different generation models of SAT instances, extending the uniform and regular 3-CNF models. They are based on the use of non-uniform probability distributions to select variables. Our last model also uses a mechanism to produce clauses of different lengths as in industrial instances. We show the existence of the phase transition phenomena for our models and we study the hardness of the generated instances as a function of the parameters of the probability distributions. We prove that, with these parameters we can adjust the difficulty of the problems in the phase transition point. We measure hardness in terms of the performance of different solvers. We show how these models will allow us to generate random instances similar to industrial instances, of interest for testing purposes.

Measuring the Hardness of SAT Instances

Tipo de Publicación:

Conference Paper

Origen:

Proc. of the 23th AAAI Conference on Artificial Intelligence, AAAI-08, AAAI Press, Chicago, USA, p.222-228 (2008)

Palabras clave:

SAT

Resumen:

The search of a precise measure of what hardness of SAT instances means for state-of-the-art solvers is a relevant research question. Among others, the space complexity of tree-like resolution (also called hardness), the minimal size of strong backdoors and of cycle-cutsets, and the treewidth can be used for this purpose. We propose the use of the tree-like space complexity as a solid candidate to be the best measure for solvers based on DPLL. To support this thesis we provide a comparison with the other mentioned measures. We also conduct an experimental investigation to show how the proposed measure characterizes the hardness of random and industrial instances.

Distribuir contenido