A self-adaptive multi-engine solver for quantified Boolean formulas

In this paper we study the problem of engineering a robust solver for quantified Boolean formulas (QBFs), i.e., a tool that can efficiently solve formulas across different problem domains without the need for domain-specific tuning. The paper presents two main empirical results along this line of research. Our first result is the development of a multi-engine solver, i.e., a tool that selects among its reasoning engines the one which is more likely to yield optimal results. In particular, we show that syntactic QBF features can be correlated to the performances of existing QBF engines across a variety of domains. We also show how a multi-engine solver can be obtained by carefully picking state-of-the-art QBF solvers as basic engines, and by harnessing inductive reasoning techniques to learn engine-selection policies. Our second result is the improvement of our multi-engine solver with the capability of updating the learned policies when they fail to give good predictions. In this way the solver becomes also self-adaptive, i.e., able to adjust its internal models when the usage scenario changes substantially. The rewarding results obtained in our experiments show that our solver AQME—Adaptive QBF Multi-Engine—can be more robust and efficient than state-of-the-art single-engine solvers, even when it is confronted with previously uncharted formulas and competitors.     

Model generation for quantified formulas with application to test data generation

We present a new model generation approach and technique for solving first-order logic (FOL) formulas with quantifiers in unbounded domains. Model generation is important, e.g., for test data generation based on test data constraints and for counterexample generation in formal verification. In such scenarios, quantified FOL formulas have to be solved stemming, e.g., from formal specifications. Satisfiability modulo theories (SMT) solvers are considered as the state-of-the-art techniques for generating models of FOL formulas. Handling of quantified formulas in the combination of theories is, however, sometimes a problem. Our approach addresses this problem and can solve formulas that were not solvable before using SMT solvers. We present the model generation algorithm and show how to convert a representation of a model into a test preamble for state initialization with test data. A prototype of this algorithm is implemented in the formal verification and test generation tool KeY.     

Ranking function synthesis for bit-vector relations

Ranking function synthesis is a key component of modern termination provers for imperative programs. While it is well-known how to generate linear ranking functions for relations over (mathematical) integers or rationals, efficient synthesis of ranking functions for machine-level integers (bit-vectors) is an open problem. This is particularly relevant for the verification of low-level code. We propose several novel algorithms to generate ranking functions for relations over machine integers: a complete method based on a reduction to Presburger arithmetic, and a template-matching approach for predefined classes of ranking functions based on reduction to SAT- and QBF-solving. The utility of our algorithms is demonstrated on examples drawn from Windows device drivers.     

An abstraction-based decision procedure for bit-vector arithmetic

We present a new decision procedure for finite-precision bit-vector arithmetic with arbitrary bit-vector operations. Such decision procedures are essential components of verifications systems, whether the domain of interest is hardware, such as in word-level bounded model-checking of circuits, or software, where one must often reason about programs with finite-precision datatypes. Our procedure alternates between generating under- and over-approximations of the original bit-vector formula. An under-approximation is obtained by a translation to propositional logic in which some bit-vector variables are encoded with fewer Boolean variables than their width. If the under-approximation is unsatisfiable, we use the unsatisfiable core to derive an over-approximation based on the subset of predicates that participated in the proof of unsatisfiability. If this over- approximation is satisfiable, the satisfying assignment guides the refinement of the previous under-approximation by increasing, for some bit-vector variables, the number of Boolean variables that encode them. We present experimental results that suggest that this abstraction-based approach can be considerably more efficient than directly invoking the SAT solver on the original formula as well as other competing decision procedures. B. Brady, R. E. Bryant, and S. A. Seshia were supported in part by SRC contract 1355.001. This research was also supported in part by the MARCO Gigascale Systems Research Center and by NSF grant CNS-0627734.     

Efficiently solving general weapon-target assignment problem by genetic algorithms with greedy eugenics

A general weapon-target assignment (WTA) problem is to find a proper assignment of weapons to targets with the objective of minimizing the expected damage of own-force asset. Genetic algorithms (GAs) are widely used for solving complicated optimization problems, such as WTA problems. In this paper, a novel GA with greedy eugenics is proposed. Eugenics is a process of improving the quality of offspring. The proposed algorithm is to enhance the performance of GAs by introducing a greedy reformation scheme so as to have locally optimal offspring. This algorithm is successfully applied to general WTA problems. From our simulations for those tested problems, the proposed algorithm has the best performance when compared to other existing search algorithms.     

Drawing Borders Efficiently

A spreadsheet, especially MS Excel, is probably one of the most popular software applications for personal-computer users and gives us convenient and user-friendly tools for drawing tables. Using spreadsheets, we often wish to draw several vertical and horizontal black lines on selective gridlines to enhance the readability of our spreadsheet. Such situations we frequently encounter are formulated as the Border Drawing Problem (BDP). Given a layout of black line segments, we study how to draw it efficiently from an algorithmic view point, by using a set of border styles and investigate its complexity. (i) We first define a formal model based on MS Excel, under which the drawability and the efficiency of border styles are discussed, and then (ii) show that unfortunately the problem is -hard for the set of the Excel border styles and for any reasonable subset of the styles. Moreover, in order to provide potentially more efficient drawing, (iii) we propose a new compact set of border styles and show a necessary and sufficient condition of its drawability.     

Interpreting linguistically quantified propositions

We discuss the idea of a linguistic quantifier and fuzzy set representations of these objects. We describe two formalisms for evaluating the truth of linguistically quantified propositions such as Most winter days are cold. the first approach is based upon a probabilistic interpretation and the second is based upon a logical interpretation, and uses a generalization of the “and” and “or” operations via OWA operators. We suggest an application of these quantified statements for the representation of the quotient operator in fuzzy relational data bases. © 1994 John Wiley & Sons, Inc.     

高效学习《数据结构》课程

从《数据结构》课程的特点出发,提出了高效学习《数据结构》的几点建议.     

Relatively quantified constraint satisfaction

The constraint satisfaction problem (CSP) is a convenient framework for modelling search problems; the CSP involves deciding, given a set of constraints on variables, whether or not there is an assignment to the variables satisfying all of the constraints. This paper is concerned with the more general framework of quantified constraint satisfaction, in which variables can be quantified both universally and existentially. We study the relatively quantified constraint satisfaction problem (RQCSP), in which the values for each individual variable can be arbitrarily restricted. We give a complete complexity classification of the cases of the RQCSP where the types of constraints that may appear are specified by a constraint language.     

On quantified linear implications

A Quantified Linear Implication (QLI) is an inclusion query over two polyhedral sets, with a quantifier string that specifies which variables are existentially quantified and which are universally quantified. Equivalently, it can be viewed as a quantified implication of two systems of linear inequalities. In this paper, we provide a 2-person game semantics for the QLI problem, which allows us to explore the computational complexities of several of its classes. More specifically, we prove that the decision problem for QLIs with an arbitrary number of quantifier alternations is PSPACE-hard. Furthermore, we explore the computational complexities of several classes of 0, 1, and 2-quantifier alternation QLIs. We observed that some classes are decidable in polynomial time, some are NP-complete, some are coNP-hard and some are \(\boldsymbol{\Pi}_{\textbf 2}^{\textbf P}\) -hard. We also establish the hardness of QLIs with 2 or more quantifier alternations with respect to the first quantifier in the quantifier string and the number of quantifier alternations. All the proofs that we provide for polynomially solvable problems are constructive, i.e., polynomial-time decision algorithms are devised that utilize well-known procedures. QLIs can be utilized as powerful modelling tools for real-life applications. Such applications include reactive systems, real-time schedulers, and static program analyzers.     

Efficiently Certifying Non-Integer Powers

We describe a randomized algorithm that, given an integer a, produces a certificate that the integer is not a pure power of an integer in expected (log a)^1+o(1) bit operations under the assumption of the Generalized Riemann Hypothesis. The certificate can then be verified in deterministic (log a)^1+o(1) time. The certificate constitutes for each possible prime exponent p a prime number q_p, such that a mod q_p is a p^th non-residue. We use an effective version of the Chebotarev density theorem to estimate the density of such prime numbers q_p.     

Efficiently supporting temporal granularities

Granularity is an integral feature of temporal data. For instance, a person's age is commonly given to the granularity of years and the time of their next airline flight to the granularity of minutes. A granularity creates a discrete image, in terms of granules, of a (possibly continuous) time-line. We present a formal model for granularity in temporal operations that is integrated with temporal indeterminacy, or “don't know when” information. We also minimally extend the syntax and semantics of SQL-92 to support mixed granularities. This support rests on two operations, scale and cast, that move times between granularities, e.g., from days to months. We demonstrate that our solution is practical by showing how granularities can be specified in a modular fashion, and by outlining a time- and space-efficient implementation. The implementation uses several optimization strategies to mitigate the expense of accommodating multiple granularities     

Value ordering for quantified CSPs

We investigate the use of value ordering in backtracking search for Quantified Constraint Satisfaction problems (QCSPs). We consider two approaches for ordering heuristics. The first approach is solution-focused and is inspired by adversarial search: on existential variables we prefer values that maximise the chances of leading to a solution, while on universal variables we prefer values that minimise those chances. The second approach is verification-focused, where we prefer values that are easier to verify whether or not they lead to a solution. In particular, we give instantiations of this approach using QCSP-Solve’s pure-value rule Gent et al. (QCSP-solve: A solver for quantified constraint satisfaction problems. In Proceedings of IJCAI, pp. 138–143, 2005). We show that on dense 3-block problems, using QCSP-Solve, the solution-focused adversarial heuristics are up to 50% faster than lexicographic ordering, while on sparse loose interleaved problems, the verification-focused pure-value heuristics are up to 50% faster. Both types are up to 50% faster on dense interleaved problems, with one pure-value heuristic approaching an order of magnitude improvement. This work was supported in part by Microsoft Research through the European PhD Scholarship Programme, and by the Embark Initiative of the Irish Research Council for Science, Engineering and Technology (IRCSET).