The class UMU consists of propositional formulas which are a union of minimal unsatisfiable formulas (MU formulas). The structural complexity of UMU formulas depends essentially on the type and degree of intertwining of the MU subformulas. Starting from class of formulas that consist only of clause (or variable) disjoint minimal unsatisfiable subformulas, we study various UMU subclasses given by weakening and these conditions. Generalizing an idea from [6], we investigate a characterization of UMU formulas by whether they allow transformation into a MU formula by adding literals and/or clauses. It can be shown that simplicity in constructing of such extensions correlates with the degree of intertwining of the MU subformulas. For UMU formulas, however, we can give only extensions that have an exponential size in the worst case. The question of the existence of short MU combinations of MU-formulas by adding literals and clauses remains open.

Abstract In this paper, we analyze Boolean formulas in conjunctive normal form (CNF) from the perspective of read-once resolution (ROR) refutation schemes. A read-once (resolution) refutation is one in which each clause is used at most once. Derived clauses can be used as many times as they are deduced. However, clauses in the original formula can only be used as part of one derivation. It is well known that ROR is not complete; that is, there exist unsatisfiable formulas for which no ROR exists. Likewise, the problem of checking if a 3CNF formula has a read-once refutation is NP-complete. This paper is concerned with a variant of satisfiability called not-all-equal satisfiability (NAE-satisfiability). A CNF formula is NAE-satisfiable if it has a satisfying assignment in which at least one literal in each clause is set to false. It is well known that the problem of checking NAE-satisfiability is NP-complete. Clearly, the class of CNF formulas which are NAE-satisfiable is a proper subset of satisfiable CNF formulas. It follows that traditional resolution cannot always find a proof of NAE-unsatisfiability. Thus, traditional resolution is not a sound procedure for checking NAE-satisfiability. In this paper, we introduce a variant of resolution called NAE-resolution which is a sound and complete procedure for checking NAE-satisfiability in CNF formulas. The focus of this paper is on a variant of NAE-resolution called read-once NAE-resolution in which each clause (input or derived) can be part of at most one NAE-resolution step. Our principal result is that read-once NAE-resolution is a sound and complete procedure for 2CNF formulas. Furthermore, we provide an algorithm to determine the smallest such NAE-resolution in polynomial time. This is in stark contrast to the corresponding problem concerning 2CNF formulas and ROR refutations. We also show that the problem of checking whether a 3CNF formula has a read-once NAE-resolution is NP-complete.

In this paper, we investigate properties of cutting plane based refutations for a class of integer programs called Horn constraint systems (HCS). Briefly, a system of linear inequalities A * x >= b is called a Horn constraint system, if each entry in A belongs to the set {0,1,-1} and furthermore there is at most one positive entry per row. Our focus is on deriving refutations i.e., proofs of unsatisfiability of such programs using cutting planes as a proof system. We also look at several properties of these refutations. Horn constraint systems can be considered as a more general form of propositional Horn formulas, i.e., CNF formulas with at most one positive literal per clause. Cutting plane calculus (CP) is a well-known calculus for deciding the unsatisfiability of propositional CNF formulas and integer programs. Usually, CP consists of a pair of inference rules. These are called the addition rule (ADD) and the division rule (DIV). In this paper, we show that cutting plane calculus is still complete for Horn constraints when every intermediate constraint is required to be Horn. We also investigate the lengths of cutting plane proofs for Horn constraint systems.

The detection of ATM fraud is a key concern for both financial institutes and bank customers but also for ATM suppliers. This paper deals with the algorithmic learning of an ATM's behavior model given the data stream of status information produced by standard mechatronic devices embedded in modern ATMs. During operation, the observed status information is compared with the learned reference model to detect abnormal behavior—assuming that a significant anomaly is a strong indicator of a fraud attempt. In contrast to previous work on automatic ATM fraud detection, we apply a class of models that also capture the timing behavior, thus covering a broader range of fraud and manipulation. In particular, we present an approach to learn a tailored behavior model, called Probabilistic Deterministic Timed-Transition Automaton, in order to enable the detection of time-based anomalies. We also report on preliminary results of an empirical evaluation using a real-world data set recorded on a public ATM, indicating the practical applicability of our approach.

Because of the direct access to cash and customer data, automated teller machines (ATMs) are the target of manifold attacks and fraud. To counter this problem, modern ATMs utilize specialized hardware security systems that are designed to detect particular types of attacks and manipulation. However, such systems do not provide any protection against future attacks that are unknown at design time. In this paper, we propose an approach that is able to detect known as well as unknown attacks on ATMs and that does not require additional security hardware. The idea is to utilize automatic model generation techniques to learn patterns of normal behavior from the status information of standard devices comprised in an ATM; a significant deviation from the learned behavior is an indicator of a fraud attempt. We cast the identification of ATM fraud as a sequence-based anomaly detection problem, and describe three specific methods that implement our approach. An empirical evaluation using a real-world data set that has been recorded on a public ATM within a time period of nine weeks shows promising results and underlines the practical applicability of the proposed approach.

Model-based anomaly detection in technical systems is an important application field of artificial intelligence. We consider discrete event systems, which is a system class to which a wide range of relevant technical systems belong and for which no comprehensive model-based anomaly detection approach exists so far. The original contributions of this paper are threefold: First, we identify the types of anomalies that occur in discrete event systems and we propose a tailored behavior model that captures all anomaly types, called probabilistic deterministic timed-transition automata (PDTTA). Second, we present a new algorithm to learn a PDTTA from sample observations of a system. Third, we describe an approach to detect anomalies based on a learned PDTTA. An empirical evaluation in a practical application, namely ATM fraud detection, shows promising results.

Software composition has been studied as a subject of state based planning for decades. Existing composition approaches that are efficient enough to be used in practice are limited to sequential arrangements of software components. This restriction dramatically reduces the number of composition problems that can be solved. However, there are many composition problems that could be solved by existing approaches if they had a possibility to combine components in very simple non-sequential ways.

A tailored model of a system is the prerequisite for various analysis tasks, such as anomaly detection, fault identification, or quality assurance. This paper deals with the algorithmic learning of a system’s behavior model given a sample of observations. In particular, we consider real-world production plants where the learned model must capture timing behavior, dependencies between system variables, as well as mode switches—in short: hybrid system’s characteristics. Usually, such model formation tasks are solved by human engineers, entailing the well-known bunch of problems including knowledge acquisition, development cost, or lack of experience. Our contributions to the outlined field are as follows. (1) We present a taxonomy of learning problems related to model formation tasks. As a result, an important open learning problem for the domain of production system is identified: The learning of hybrid timed automata. (2) For this class of models, the learning algorithm HyBUTLA is presented. This algorithm is the first of its kind to solve the underlying model formation problem at scalable precision. (3) We present two case studies that illustrate the usability of this approach in realistic settings. (4) We give a proof for the learning and runtime properties of HyBUTLA.

Q-Learning is a widely used method for dealing with reinforcement learning problems. To speed up learning and to exploit gained experience more efficiently it is highly beneficial to add generalization to Q-Learning and thus enabling the transfer of experience to unseen but similar states. In this paper, we report on improvements for GNG-Q, a combination of Q-Learning and growing neural gas (GNG). It solves reinforcement learning problems with continuous state spaces and simultaneously learns a proper approximation of the state space by starting with a coarse resolution that is gradually refined based on information achieved during learning. We introduce the Interpolating GNG-Q (IGNG-Q) that uses distance-based interpolation between learned Q-vectors, adjust the update rule, suggest a new refinement strategy and propose a new criterion to decide when a refinement is necessary. Furthermore, we argue that this criterion offers an implicit local stopping condition for changes made to the approximation. Additionally, we employ eligibility traces to speed up learning. The improved method is evaluated in continuous state spaces and the results are compared with several approaches from literature. Our experiments confirm that the modifications highly improve the efficiency of the approximation and that IGNG-Q is well competitive with existing methods.

The increasing complexity of today's production systems and the variety of model-based approaches to their monitoring, diagnosis and testing emphasize the importance of the modeling step. Modeling is mostly done manually, in a costly and time-consuming way. In this paper, an alternative that comes from the learning theory is given: an automated procedure for identifying behavior models from recorded observations. Assuming the system's structure is known, the algorithm presented here is capable of learning behavior models for its components. The algorithm accounts for probabilistic, timing, discrete and continuous aspects of the given system, using the modeling formalism of hybrid automata. The practical usability of identified models is demonstrated using an anomaly detection application for a real production system.

We propose a new mutation operator - the biased mutation operator (BMO) -for evolution strategies, which is capable of handling problems for constrained fitness landscapes. The idea of our approach is to bias the mutation ellipsoid in relation to the parent and therefore lead the mutations into a beneficial direction self-adaptively. This helps to improve the success rate to reproduce better offspring. Experimental results show this bias enhances the solution quality within constrained search domains. The number of the additional strategy parameters used in our approach equals to the number of dimensions of the problem. Compared to the correlated mutation, the BMO needs much less memory and supersedes the computation of the rotation matrix of the correlated mutation and the asymmetric probability density function of the directed mutation.

No abstract available.

Multiparent crossovers have been validated their outperformance on several optimization problems. However, there are two issues to be considered - the number of parents and the disruptiveness caused by multiple parents. We present a tabu multiparent genetic algorithm (TMPGA) to address these two issues by integrating tabu search into the mating of multiparent genetic algorithms. TMPGA utilizes the tabu restriction and the aspiration criterion to sift selected parents in consideration of population diversity and selection pressure. Furthermore, the resulting mating validity further adjusts the number of parents participating in a mating. Experiments are conducted with four common test functions. The results indicate that TMPGA can achieve better performance than both two-parent GA and multiparent GA with the diagonal crossover.

We consider polynomial time bounded reductions, in particular between k – SAT, SAT and SAT*, in order to obtain the minimal number of variables. As an example we prove that SAT and Unique SAT have, for deterministic algorithms, the same upper bound of the form O( Π c n) for some c > 1, where n is the number of variables of Π. We show that k – Unique SAT is not harder than k – SAT, but not easier than k(r) – SAT (formulas in k – CNF with at most r positive or negative clauses). Finally we present a proof that for each problem in NTlME(n) there is a polynomial reduction to SAT such that the number of variables in f(Π) is only O(n) improving Schnorr–Cook's reduction with O(n log n) variables.