Hans Kleine Büning

TCS Journal 2024 Journal Article

Classes of propositional UMU formulas and their extensions to minimal unsatisfiable formulas

• Hans Kleine Büning

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.

TCS Journal 2018 Journal Article

Finding read-once resolution refutations in systems of 2CNF clauses

• Hans Kleine Büning
• Piotr Wojciechowski
• K. Subramani

In this paper, we analyze 2CNF formulas from the perspectives of Read-Once resolution (ROR) refutation schemes. We focus on two types of ROR refutations, viz. , variable-once refutation and clause-once refutation. In the former, each variable may be used at most once in the derivation of a refutation, while in the latter, each clause may be used at most once. We show that the problem of checking whether a given 2CNF formula has an ROR refutation is NP-complete, under both schemes. This is surprising, in light of the fact that there exist polynomial time refutation schemes (tree-resolution and DAG-resolution) for 2CNF formulas. On the positive side, we show that 2CNF formulas have copy-complexity 2, which means that any unsatisfiable 2CNF formula has a refutation, in which any clause needs to be used at most twice. The study of resolution refutation schemes is a sub-field of proof complexity, which has received a lot of attention in the literature.

TCS Journal 2017 Journal Article

Foreword

• Kira Adaricheva
• Giuseppe F. Italiano
• Hans Kleine Büning
• György Turán

ECAI Conference 2014 Conference Paper

On the Usage of Behavior Models to Detect ATM Fraud

• Timo Klerx
• Maik Anderka
• Hans Kleine Büning

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.

SAT Conference 2013 Conference Paper

Nested Boolean Functions as Models for Quantified Boolean Formulas

• Uwe Bubeck
• Hans Kleine Büning

Abstract Nested Boolean functions or Boolean programs are an alternative to the quantified Boolean formula (QBF) characterization of polynomial space. The idea is to start with a set of Boolean functions given as propositional formulas and to define new functions as compositions or instantiations of previously defined ones. We investigate the relationship between function instantiation and quantification and present a compact representation of models and countermodels of QBFs with and without free variables as nested Boolean functions. The representation is symmetric with respect to Skolem models and Herbrand countermodels. For a formula with free variables, it can describe both kinds of models simultaneously in one complete equivalence model which can be Skolem or Herbrand depending on actual assignments to the free variables.

AAAI Conference 2012 Conference Paper

Learning Behavior Models for Hybrid Timed Systems

• Oliver Niggemann
• Benno Stein
• Asmir Vodencarevic
• Alexander Maier
• Hans Kleine Büning

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.

SAT Conference 2011 Conference Paper

Transformations into Normal Forms for Quantified Circuits

• Hans Kleine Büning
• Xishun Zhao
• Uwe Bubeck

Abstract We consider the extension of Boolean circuits to quantified Boolean circuits by adding universal and existential quantifier nodes with semantics adopted from quantified Boolean formulas ( \(\mbox{\rm QBF}\) ). The concept allows not only prenex representations of the form \(\forall x_{1}\exists y_{1}. .. \forall x_{n}\exists y_{n}\ c\) where c is an ordinary Boolean circuit with inputs x 1, .. ., x n, y 1, .. ., y n. We also consider more general non-prenex normal forms with quantifiers inside the circuit as in non-prenex \(\mbox{\rm QBF}\), including circuits in which an input variable may occur both free and bound. We discuss the expressive power of these classes of circuits and establish polynomial-time equivalence-preserving transformations between many of them. Additional polynomial-time transformations show that various classes of quantified circuits have the same expressive power as quantified Boolean formulas and Boolean functions represented as finite sequences of nested definitions ( \(\mbox{\rm NBF}\) ). In particular, universal quantification can be simulated efficiently by circuits containing only existential quantifiers if overlapping scopes of variables are allowed.

SAT Conference 2010 Conference Paper

Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN

• Uwe Bubeck
• Hans Kleine Büning

Abstract We extend quantified 2-CNF formulas by also allowing literals over free variables which are exempt from the 2-CNF restriction. That means we consider quantified CNF formulas with clauses that contain at most two bound literals and an arbitrary number of free literals. We show that these \({\it Q2-CNF}^{b}\) formulas can be transformed in polynomial time into purely existentially quantified CNF formulas in which the bound literals are in 2-HORN (∃ 2 − HORN b ). Our result still holds if we allow Henkin-style quantifiers with explicit dependencies. In general, dependency quantified Boolean formulas ( \({\it DQBF}\) ) are assumed to be more succinct at the price of a higher complexity. This paper shows that \({\it DQ2-CNF}^{b}\) has a similar expressive power and complexity as ∃ 2 − HORN b. In the special case that the 2-CNF restriction is also applied to the free variables ( \({\it DQ2-CNF}^{*}\) ), the satisfiability can be decided in linear time.

SAT Conference 2009 Conference Paper

Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits

• Hans Kleine Büning
• Xishun Zhao
• Uwe Bubeck

Abstract We present an extension of Q-Unit resolution for formulas that are not completely in clausal form. This b-unit resolution is applied to different classes of quantified Boolean formulas in which the existential and universal variables satisfy the Horn property. These formulas are transformed into propositional equivalents consisting of only polynomially many subformulas. We obtain compact encodings as Boolean circuits and show that both representations have the same expressive power.

TCS Journal 2008 Journal Article

Computational complexity of quantified Boolean formulas with fixed maximal deficiency

• Hans Kleine Büning
• Xishun Zhao

The paper investigates the computational complexity of quantified Boolean formulas with fixed maximal deficiency. The satisfiability problem for quantified Boolean formulas with maximal deficiency 1 is shown to be solvable in polynomial time. For k ≥ 1, it is shown that true formulas with fixed maximal deficiency k have models in which all Boolean functions can be represented as CNF formulas over at most 2 4 k / 3 universal variables. As a consequence, the satisfiability problem for QCNF formulas with fixed maximal deficiency is in NP and for fixed deficiency the minimal falsity problem is in D P. For two subclasses of quantified Boolean formulas with PSPACE -complete evaluation problem, QEHORN and QE2-CNF, we show that for fixed deficiency the minimal falsity problem can be decided in polynomial time.

SAT Conference 2007 Conference Paper

Bounded Universal Expansion for Preprocessing QBF

• Uwe Bubeck
• Hans Kleine Büning

Abstract We present a new approach for preprocessing Quantified Boolean Formulas ( QBF ) in conjunctive normal form ( CNF ) by expanding a selection of universally quantified variables with bounded expansion costs. We describe a suitable selection strategy which exploits locality of universals and combines cost estimates with goal orientation by taking into account unit literals which might be obtained. Furthermore, we investigate how Q-resolution can be integrated into this method. In particular, resolution is applied specifically to reduce the amount of copying necessary for universal expansion. Experimental results demonstrate that our preprocessing can successfully improve the performance of state-of-the-art QBF solvers on well-known problems from the QBFLIB collection.

SAT Conference 2006 Conference Paper

Dependency Quantified Horn Formulas: Models and Complexity

• Uwe Bubeck
• Hans Kleine Büning

Abstract Dependency quantified Boolean formulas ( DQBF ) extend quantified Boolean formulas with Henkin-style partially ordered quantifiers. It has been shown that this is likely to yield more succinct representations at the price of a computational blow-up from PSPACE to NEXPTIME. In this paper, we consider dependency quantified Horn formulas ( DQHORN ), a subclass of DQBF, and show that the computational simplicity of quantified Horn formulas is preserved when adding partially ordered quantifiers. We investigate the structure of satisfiability models for DQHORN formulas and prove that for both DQHORN and ordinary QHORN formulas, the behavior of the existential quantifiers depends only on the cases where at most one of the universally quantified variables is zero. This allows us to transform DQHORN formulas with free variables into equivalent QHORN formulas with only a quadratic increase in length. An application of these findings is to determine the satisfiability of a dependency quantified Horn formula Φ with |∀| universal quantifiers in time O (| ∀ |·|Φ|), which is just as hard as QHORN -SAT.

SAT Conference 2006 Conference Paper

Minimal False Quantified Boolean Formulas

• Hans Kleine Büning
• Xishun Zhao

Abstract This paper is concerned with the minimal falsity problem MF for quantified Boolean formulas. A QCNF formula (i. e. , with CNF-matrix) is called minimal false, if the formula is false and any proper subformula is true. It is shown that the minimal falsity problem is PSPACE-complete. Then the deficiency of a QCNF formula is defined as the difference between the number of clauses and the number of existentially quantified variables. For quantified Boolean formulas with deficiency one, MF is solvable in polynomial time.

SAT Conference 2005 Conference Paper

Model-Equivalent Reductions

• Xishun Zhao
• Hans Kleine Büning

Abstract In this paper, the notions of polynomial–time model equivalent reduction and polynomial–space model equivalent reduction are introduced in order to investigate in a subtle way the expressive power of different theories. We compare according to these notions some classes of propositional formulas and quantified Boolean formulas. Our results show that classes of theories with the same complexity might have different representation strength under some conjectures which are widely believed to be true in computation complexity theory.

SAT Conference 2005 Conference Paper

Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas

• Uwe Bubeck
• Hans Kleine Büning
• Xishun Zhao

Abstract In this paper, quantified Horn formulas with free variables ( QHORN * ) are investigated. The main result is that any quantified Horn formula Φ of length |Φ| with free variables, |∀| universal quantifiers and an arbitrary number of existential quantifiers can be transformed into an equivalent formula of length O (| ∀ | ·|Φ|) which contains only existential quantifiers. Moreover, it is shown that quantified Horn formulas with free variables have equivalence models where every existential quantifier is associated with a monotone Boolean function. The results allow a simple representation of quantified Horn formulas as purely existentially quantified Horn formulas (∃ HORN * ). An application described in the paper is to solve QHORN * -SAT in O (| ∀ | ·|Φ|) by using this transformation in combination with a linear-time satisfiability checker for propositional Horn formulas.

SAT Conference 2004 Conference Paper

Equivalence Models for Quantified Boolean Formulas

• Hans Kleine Büning
• Xishun Zhao

In this paper, the notion of equivalence models for quantified Boolean formulas with free variables is introduced. The computational complexity of the equivalence model checking problem is investigated in the general case and some restricted cases. We also establish a connection between the structure of some quantified Boolean formulas and the structure of models.

SAT Conference 2003 Conference Paper

On Boolean Models for Quantified Boolean Horn Formulas

• Hans Kleine Büning
• K. Subramani 0001
• Xishun Zhao

Abstract For a Quantified Boolean Formula \(({\it QBF })\) Φ= Qφ, an assignment is a function \(\cal M\) that maps each existentially quantified variable of Φ to a Boolean function, where φ is a propositional formula and Q is a linear ordering of quantifiers on the variables of Φ. An assignment \(\cal M\) is said to be proper, if for each existentially quantified variable y i, the associated Boolean function f i does not depend upon the universally quantified variables whose quantifiers in Q succeed the quantifier of y i. An assignment \(\cal M\) is said to be a model for Φ, if it is proper and the formula \(\phi^{\cal M}\) is a tautology, where \(\phi^{\cal M}\) is the formula obtained from φ by substituting f i for each existentially quantified variable y i. We show that any true quantified Horn formula has a Boolean model consisting of monotone monomials and constant functions only; conversely, if a QBF has such a model then it contains a clause–subformula in \({\it QHORN }\cap {\it SAT }\).

SAT Conference 2003 Conference Paper

Read-Once Unit Resolution

• Hans Kleine Büning
• Xishun Zhao

Abstract Read-once resolution is the resolution calculus with the restriction that any clause can be used at most once in the derivation. We show that the problem of deciding whether a propositional CNF -formula has a read-once unit resolution refutation is NP -complete. In contrast, we prove that the problem of deciding whether a formula can be refuted by read-once unit resolution while every proper subformula has no read-once unit resolution refutation is solvable in quadratic time.

CSL Conference 1999 Conference Paper

An Upper Bound for Minimal Resolution Refutations

• Hans Kleine Büning

Abstract We consider upper bounds for minimal resolution refutations of propositional formulas in CNF. We show that minimal refutations of minimal unsatisfiable formulas over n variables and n + k clauses consist of at most 2 k − 1 n 2 applications of the resolution rule.

CSL Conference 1991 Conference Paper

Subclasses of Quantified Boolean Formulas

• Andreas Flögel
• Marek Karpinski
• Hans Kleine Büning

Abstract Using the results of a former paper of two of the authors [KaKB 90], for certain subclasses of quantified Boolean formulas it is shown, that the evaluation problems for these classes are coNP-complete. These subclasses can be seen as extensions of Horn and 2-CNF formulas. Further it is shown that the evaluation problem for quantified CNF formulas remains PSPACE-complete, even if at most one universal variable is allowed in each clause.

CSL Conference 1989 Conference Paper

Loop Detection in Propositional Prolog Programs

• Hans Kleine Büning
• Ulrich Löwen
• Stefan Schmitgen

Abstract We are interested in loop detection in knowledge based systems because loops are one of the problems when formalizing knowledge. Since rule-based systems are widely used and backward chaining in rule-based systems and the Prolog inference-strategy for logic programs can be compared, we consider loop detection in propositional Prolog-programs. First we present an algorithm which decides for a given Prolog-program π and a query γ, whether the answer is yes, no or loop. We prove that this algorithm needs linear time in the length of π∧γ. This is possible by setting a flag for each atom occuring in π, which reflects the actual state of this atom during the refutation. We show that the algortihm can be extended to Prolog-programs π c with cut. Further we show that the problem to decide, whether there exists a query for a given Prolog-program (including cut) which leads to a looping derivation, is NP-complete. Allowing assert and retract in a propositional Prolog-program we show that the loop-problem is undecidable. In this case it is even undecidable whether we obtain a looping refutation for a given question γ and a Prolog-program π ar.

I&C Journal 1989 Journal Article

Optimizing propositional calculus formulas with regard to questions of deducibility

• Hans Kleine Büning
• Ulrich Löwen

We consider propositional calculus formulas α and are interested in the complexity of deciding α ¦= γ for a clause γ. We investigate the problem whether efficiency of an algorithm deciding α ¦= γ can be improved by learning from queries γ′ having been answered by the algorithm before. So we are looking for an optimized formula opt(α), which is obtained from α by adding suitable consequences. We restrict ourselves to the following aspects of this optimization problem: first, we query for (k + 1)-clauses allowing the addition of at most k-clauses. We prove that this problem is coNP-complete. Second, we analyze various resolution strategies. We establish a lower bound for the number of clauses which must be added to obtain an optimized formula. Finally, we investigate optimization aspects of SLD resolution.

TCS Journal 1989 Journal Article

Projections of vector addition system reachability sets are semilinear

• Hans Kleine Büning
• Theodor Lettmann
• Ernst W. Mayr

The reachability sets of Vector Addition Systems of dimension six or more can be non-semilinear. This may be one reason why the inclusion problem (as well as the equality problem) for reachability sets of vector addition systems in general is undecidable, even though the reachability problem itself is known to be decidable. We show that any one-dimensional projection of the reachability set of an arbitrary vector addition system is semilinear, and hence “simple”.

CSL Conference 1988 Conference Paper

On the Computational Complexity of Quantified Horn Clauses

• Marek Karpinski
• Hans Kleine Büning
• Peter H. Schmitt

Abstract A polynomial time algorithm is presented for the evaluation problem for quantified propositional Horn clauses. This answers an open problem posed by Itai and Makowski in (IM 87).

TCS Journal 1980 Journal Article

The reachability problem for Petri nets and decision problems for Skolem arithmetic

• Egon Börger
• Hans Kleine Büning

We show that the decision problem for the class C 0 of all closed universal Horn formulae in prenex conjunctive normal form of extended Skolem arithmetic without equality (i. e. first order formulae built up from the multiplication sign, constants for the natural numbers and free occuring predicate symbols) is exponentially time bounded equivalent to the reachability problem for Petri nets if restricted to the class of formulae with (a) only monadic predicate symbols, with (b) only binary disjunctions in the quantifier free matrix and (c) without terms containing a variable more than once. We show that leaving out one of the restrictions (a) to (c) yields classes of formulae whose decision problem can assume any prescribed recursively enumerable complexity in terms of many-one degrees of unsolvability.