Algorithms, Volume 11, Issue 9 (September 2018) – 14 articles

The satisfiability modulo theories (SMT) problem is to decide the satisfiability of a logical formula with respect to a given background theory. This work studies the counting version of SMT with respect to linear integer arithmetic (LIA), termed SMT(LIA). Specifically, the purpose of this paper is to count the number of solutions (volume) of a SMT(LIA) formula, which has many important applications and is computationally hard. To solve the counting problem, an approximate method that employs a recent Markov Chain Monte Carlo (MCMC) sampling strategy called “flat histogram” is proposed. Furthermore, two refinement strategies are proposed for the sampling process and result in two algorithms, MCMC-Flat^1/2 and MCMC-Flat^1/t, respectively. In MCMC-Flat^1/t, a pseudo sampling strategy is introduced to evaluate the flatness of histograms. Experimental results show that our MCMC-Flat^1/t method can achieve good accuracy on both structured and random instances, and our MCMC-Flat^1/2 is scalable for instances of convex bodies with up to 7 variables. Full article

One of the most recent members of the Paxos family of protocols is Generalized Paxos. This variant of Paxos has the characteristic that it departs from the original specification of consensus, allowing for a weaker safety condition where different processes can have a different views on a sequence being agreed upon. However, much like the original Paxos counterpart, Generalized Paxos does not have a simple implementation. Furthermore, with the recent practical adoption of Byzantine fault tolerant protocols in the context of blockchain protocols, it is timely and important to understand how Generalized Paxos can be implemented in the Byzantine model. In this paper, we make two main contributions. First, we attempt to provide a simpler description of Generalized Paxos, based on a simpler specification and the pseudocode for a solution that can be readily implemented. Second, we extend the protocol to the Byzantine fault model, and provide the respective correctness proof. Full article

The Hamiltonian cycle reconfiguration problem asks, given two Hamiltonian cycles $C_0$ and $C_t$ of a graph G, whether there is a sequence of Hamiltonian cycles $C_0,C_1,\dots ,C_t$ such that $C_i$ can be obtained from $C_{i-1}$ by a switch for each i with $1\le i\le t$ , where a switch is the replacement of a pair of edges $uv$ and $wz$ on a Hamiltonian cycle with the edges $uw$ and $vz$ of G, given that $uw$ and $vz$ did not appear on the cycle. We show that the Hamiltonian cycle reconfiguration problem is PSPACE-complete, settling an open question posed by Ito et al. (2011) and van den Heuvel (2013). More precisely, we show that the Hamiltonian cycle reconfiguration problem is PSPACE-complete for chordal bipartite graphs, strongly chordal split graphs, and bipartite graphs with maximum degree 6. Bipartite permutation graphs form a proper subclass of chordal bipartite graphs, and unit interval graphs form a proper subclass of strongly chordal graphs. On the positive side, we show that, for any two Hamiltonian cycles of a bipartite permutation graph and a unit interval graph, there is a sequence of switches transforming one cycle to the other, and such a sequence can be obtained in linear time. Full article

Semi-supervised learning algorithms have become a topic of significant research as an alternative to traditional classification methods which exhibit remarkable performance over labeled data but lack the ability to be applied on large amounts of unlabeled data. In this work, we propose a new semi-supervised learning algorithm that dynamically selects the most promising learner for a classification problem from a pool of classifiers based on a self-training philosophy. Our experimental results illustrate that the proposed algorithm outperforms its component semi-supervised learning algorithms in terms of accuracy, leading to more efficient, stable and robust predictive models. Full article

We examine the use of deep learning (neural networks) to predict the movement of the S&P 500 Index using past returns of all the stocks in the index. Our analysis finds that the future direction of the S&P 500 index can be weakly predicted by the prior movements of the underlying stocks in the index, but not strongly enough to reject market efficiency. Decomposition of the prediction error indicates that most of the lack of predictability comes from randomness and only a little from nonstationarity. We believe this is the first test of S&P 500 market efficiency that uses a very large information set, and it extends the domain of weak-form market efficiency tests. Full article

Providing model-generated explanations in recommender systems is important to user experience. State-of-the-art recommendation algorithms—especially the collaborative filtering (CF)- based approaches with shallow or deep models—usually work with various unstructured information sources for recommendation, such as textual reviews, visual images, and various implicit or explicit feedbacks. Though structured knowledge bases were considered in content-based approaches, they have been largely ignored recently due to the availability of vast amounts of data and the learning power of many complex models. However, structured knowledge bases exhibit unique advantages in personalized recommendation systems. When the explicit knowledge about users and items is considered for recommendation, the system could provide highly customized recommendations based on users’ historical behaviors and the knowledge is helpful for providing informed explanations regarding the recommended items. A great challenge for using knowledge bases for recommendation is how to integrate large-scale structured and unstructured data, while taking advantage of collaborative filtering for highly accurate performance. Recent achievements in knowledge-base embedding (KBE) sheds light on this problem, which makes it possible to learn user and item representations while preserving the structure of their relationship with external knowledge for explanation. In this work, we propose to explain knowledge-base embeddings for explainable recommendation. Specifically, we propose a knowledge-base representation learning framework to embed heterogeneous entities for recommendation, and based on the embedded knowledge base, a soft matching algorithm is proposed to generate personalized explanations for the recommended items. Experimental results on real-world e-commerce datasets verified the superior recommendation performance and the explainability power of our approach compared with state-of-the-art baselines. Full article

Adaptive and non-adaptive minimal realization (MR) fractional order observers (FOO) for linear time-invariant systems (LTIS) of a possibly different derivation order (mixed order observers, MOO) are studied in this paper. Conditions on the convergence and robustness are provided using a general framework which allows observing systems defined with any type of fractional order derivative (FOD). A qualitative discussion is presented to show that the derivation orders of the observer structure and for the parameter adjustment are relevant degrees of freedom for performance optimization. A control problem is developed to illustrate the application of the proposed observers. Full article

Linguistic decision making (DM) is an important research topic in DM theory and methods since using linguistic terms for the assessment of the objective world is very fitting for human thinking and expressing habits. However, there is both uncertainty and hesitancy in linguistic arguments in human thinking and judgments of an evaluated object. Nonetheless, the hybrid information regarding both uncertain linguistic arguments and hesitant linguistic arguments cannot be expressed through the various existing linguistic concepts. To reasonably express it, this study presents a linguistic cubic hesitant variable (LCHV) based on the concepts of a linguistic cubic variable and a hesitant fuzzy set, its operational relations, and its linguistic score function for ranking LCHVs. Then, the objective extension method based on the least common multiple number/cardinality for LCHVs and the weighted aggregation operators of LCHVs are proposed to reasonably aggregate LCHV information because existing aggregation operators cannot aggregate LCHVs in which the number of their hesitant components may imply difference. Next, a multi-attribute decision-making (MADM) approach is proposed based on the weighted arithmetic averaging (WAA) and weighted geometric averaging (WGA) operators of LCHVs. Lastly, an illustrative example is provided to indicate the applicability of the proposed approaches. Full article

The capability of efficiently processing the data streams emitted by nowadays ubiquitous sensing devices enables the development of new intelligent services. Data Stream Processing (DSP) applications allow for processing huge volumes of data in near real-time. To keep up with the high volume and velocity of data, these applications can elastically scale their execution on multiple computing resources to process the incoming data flow in parallel. Being that data sources and consumers are usually located at the network edges, nowadays the presence of geo-distributed computing resources represents an attractive environment for DSP. However, controlling the applications and the processing infrastructure in such wide-area environments represents a significant challenge. In this paper, we present a hierarchical solution for the autonomous control of elastic DSP applications and infrastructures. It consists of a two-layered hierarchical solution, where centralized components coordinate subordinated distributed managers, which, in turn, locally control the elastic adaptation of the application components and deployment regions. Exploiting this framework, we design several self-adaptation policies, including reinforcement learning based solutions. We show the benefits of the presented self-adaptation policies with respect to static provisioning solutions, and discuss the strengths of reinforcement learning based approaches, which learn from experience how to optimize the application performance and resource allocation. Full article

In this paper, a modification to the Polak–Ribiére–Polyak (PRP) nonlinear conjugate gradient method is presented. The proposed method always generates a sufficient descent direction independent of the accuracy of the line search and the convexity of the objective function. Under appropriate conditions, the modified method is proved to possess global convergence under the Wolfe or Armijo-type line search. Moreover, the proposed methodology is adopted in the Hestenes–Stiefel (HS) and Liu–Storey (LS) methods. Extensive preliminary numerical experiments are used to illustrate the efficiency of the proposed method. Full article

Due to the impact of weather forecasting on global human life, and to better reflect the current trend of weather changes, it is necessary to conduct research about the prediction of precipitation and provide timely and complete precipitation information for climate prediction and early warning decisions to avoid serious meteorological disasters. For the precipitation prediction problem in the era of climate big data, we propose a new method based on deep learning. In this paper, we will apply deep belief networks in weather precipitation forecasting. Deep belief networks transform the feature representation of data in the original space into a new feature space, with semantic features to improve the predictive performance. The experimental results show, compared with other forecasting methods, the feasibility of deep belief networks in the field of weather forecasting. Full article

We provide an algorithm to efficiently compute bisimulation for probabilistic labeled transition systems, featuring non-deterministic choice as well as discrete probabilistic choice. The algorithm is linear in the number of transitions and logarithmic in the number of states, distinguishing both action states and probabilistic states, and the transitions between them. The algorithm improves upon the proposed complexity bounds of the best algorithm addressing the same purpose so far by Baier, Engelen and Majster-Cederbaum (Journal of Computer and System Sciences 60:187–231, 2000). In addition, experimentally, on various benchmarks, our algorithm performs rather well; even on relatively small transition systems, a performance gain of a factor 10,000 can be achieved. Full article

The article presents a numerical model of sea wave generation as an implementation of the stochastic process with a spectrum of wave angular velocity. Based on the wave spectrum, a forming filter is determined, and its input is fed with white noise. The resulting signal added to the angular speed of a ship represents disturbances acting on the ship’s hull as a result of wave impact. The model was used for simulation tests of the influence of disturbances on the course stabilization system of the ship. Full article

With the continuous development of optical fiber sensing technology, the Optical Fiber Pre-Warning System (OFPS) has been widely used in various fields. The OFPS identifies the type of intrusion based on the detected vibration signal to monitor the surrounding environment. Aiming at the real-time requirements of OFPS, this paper presents a fast algorithm to accelerate the detection and recognition processing of optical fiber intrusion signals. The algorithm is implemented in an embedded system that is composed of a digital signal processor (DSP). The processing flow is divided into two parts. First, the dislocation processing method is adopted for the sum processing of original signals, which effectively improves the real-time performance. The filtered signals are divided into two parts and are parallel processed by two DSP boards to save time. Then, the data is input into the identification module for feature extraction and classification. Experiments show that the algorithm can effectively detect and identify the optical fiber intrusion signals. At the same time, it accelerates the processing speed and meets the real-time requirements of OFPS for detection and identification. Full article