Symbolic Techniques in Satisfiability Solving

Recent work has shown how to use binary decision diagrams for satisfiability solving. The idea of this approach, which we call symbolic quantifier elimination, is to view an instance of propositional satisfiability as an existentially quantified proposition formula. Satisfiability solving then amounts to quantifier elimination; once all quantifiers have been eliminated, we are left with either 1 or 0. Our goal in this work is to study the effectiveness of symbolic quantifier elimination as an approach to satisfiability solving. To that end, we conduct a direct comparison with the DPLL-based ZChaff, as well as evaluate a variety of optimization techniques for the symbolic approach. In comparing the symbolic approach to ZChaff, we evaluate scalability across a variety of classes of formulas. We find that no approach dominates across all classes. While ZChaff dominates for many classes of formulas, the symbolic approach is superior for other classes of formulas. Once we have demonstrated the viability of the symbolic approach, we focus on optimization techniques for this approach. We study techniques from constraint satisfaction for finding a good plan for performing the symbolic operations of conjunction and of existential quantification. We also study various variable-ordering heuristics, finding that while no heuristic seems to dominate across all classes of formulas, the maximum-cardinality search heuristic seems to offer the best overall performance. ★A preliminary version of the paper was presented in SAT'04. Supported in part by NSF grants CCR-9988322, CCR-0124077, CCR-0311326, IIS-9908435, IIS-9978135, EIA-0086264, ANI-0216467, and by BSF grant 9800096.     

Solving quantified linear arithmetic by counterexample-guided instantiation

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedures for linear real arithmetic and linear integer arithmetic formulas with one quantifier alternation. We discuss extensions of these techniques for handling mixed real and integer arithmetic, and to formulas with arbitrary quantifier alternations. For the latter, we use a novel strategy that handles quantified formulas that are not in prenex normal form, which has advantages with respect to existing approaches. All of these techniques can be integrated within the solving architecture used by typical SMT solvers. Experimental results on standardized benchmarks from model checking, static analysis, and synthesis show that our implementation in the SMT solver cvc4 outperforms existing tools for quantified linear arithmetic.     

The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT

Decidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the recent years. Even though most interval logics turn out to be undecidable, meaningful exceptions exist, such as the logics of temporal neighborhood and (some of) the logics of the subinterval relation. In this paper, we explore a different path to decidability: instead of restricting the set of modalities or imposing severe semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema’s CDT, and we suitably limit the negation depth of modalities. The decidability of the satisfiability problem for the resulting fragment, called CDT_BS, over the class of all linear orders, is proved by embedding it into a well-known decidable quantifier prefix class of first-order logic, namely, Bernays-Schönfinkel class. In addition, we show that CDT_BS is in fact NP-complete (Bernays-Schönfinkel class is NEXPTIME-complete), and we prove its expressive completeness with respect to a suitable fragment of Bernays-Schönfinkel class. Finally, we show that any increase in the negation depth of CDT_BS modalities immediately yields undecidability.     

Guards,Bounds, and Generalized Semantics

Some initial motivations for the Guarded Fragment still seem of interest in carrying its program further. First, we stress the equivalence between two perspectives: (a) satisfiability on standard models for guarded first-order formulas, and (b) satisfiability on general assignment models for arbitrary first-order formulas. In particular, we give a new straightforward reduction from the former notion to the latter. We also show how a perspective shift to general assignment models provides a new look at the fixed-point extension LFP(FO) of first-order logic, making it decidable. Next, we relate guarded syntax to earlier quantifier restriction strategies for achieving effective axiomatizability in second-order logic – pointing at analogies with ‘persistent’ formulas, which are essentially in the Bounded Fragment of many-sorted first-order logic. Finally, we look at some further unexplored directions, including the systematic use of ‘quasi-models’ as a semantics by itself.     

FQUERY III+: A “human-consistent” database querying system based on fuzzy logic with linguistic quantifiers

Using a fuzzy-logic-based calculus of linguistically quantified propositions we present FQUERY III+, a new, more “human-friendly” and easier-to-use implementation of a querying scheme proposed originally by Kacprzyk and Zio kowski to handle imprecise queries including a linguistic quantifier as, e.g. find all records in which most (almost all, much more than 75%, … or any other linguistic quantifier) of the important attributes (out of a specified set) are as desired (e.g. equal to five, more than 10, large, more or less equal to 15, etc.). FQUERY III+ is an “add-on” to Ashton-Tate's dBase III Plus.     

A unimodality property of optimal exhaustive prefix codes and retrieval trees over alphabets of varying size

For the case of a set of equally probable words to be encoded, by a coding alphabet in which each new symbol is more costly than the last, it is clear that the average word cost (equivalent to the total in this case) of an exhaustive prefix code varies with the subset chosen from the possible alphabet. The present paper establishes the nature of the variation and discovers the average work length is non-decreasing to a point, and then non-increasing beyond, thus making simple any search for a best alphabet. The above result is established first for an alphabet with costs {1,2,3,…}, which is important in information retrieval applications, then for arbitrary, but strictly increasing costs and for arbitrary, non-decreasing costs.     

1-Inverses for polynomial matrices of non-constant rank

Let p₁, … p_t be polynomials in ⁿ with a variety V of common zeros contained in a suitable open set U. Explicit formulas are provided to construct rational functions λ₁, … λ_s such that Σ_i=1^sp_iλ_i 1, and such that the singularities of the λ_i are contained in U. This result is applied to compute rational functions-valued 1-inverses of matrices with polynomial coefficients, which do not have constant rank, while retaining control over the location of the singularities of the rational functions themselves.     

Complexity of presburger arithmetic with fixed quantifier dimension

It is shown that the decision problem for formulas in Presburger arithmetic with quantifier prefix [?₁?₂ … ? _m ?³] (form odd) and [?₁?₂ … ? _m ?³] (form even) is complete for the class Σ _m ^p of the polynomial-time hierarchy. Furthermore, the prefix type [????] is complete for Σ ₂ ^p , and the prefix type [??] is complete for NP. This improves results (and solves a problem left open) by Grädel [7].     

Experimental numerical studies on a supercomputer of natural convection in an enclosure with localized heating

We present particle simulations of natural convection of a symmetrical, nonlinear, three-dimensional cavity flow problem. Qualitative studies are made in an enclosure with localized heating. The assumption is that particles interact locally by means of a compensating Lennard-Jones type force F, whose magnitude is given by −G/r^p + H/r^q.

In this formula, the parameters G, H, p, q depend upon the nature of the interacting particles and r is the distance between two particles. We also consider the system to be under the influence of gravity. Assuming that there are n particles, the equations relating position, velocity and acceleration at time t_k = kΔt, K = 0, 1, 2, …, are solved simultaneously using the “leap-frog” formulas. The basic formulas relating force and acceleration are Newton's dynamical equations F_i,k = m_ia_i,k, I = 1, 2, 3, …, n, where m_i is the mass of the ith particle.

Extensive and varied computations on a CRAY X - MP/24 are described and discussed, and comparisons are made with the results of others.     

First-Order Logic with Two Variables and Unary Temporal Logic

We investigate the power of first-order logic with only two variables over ω-words and finite words, a logic denoted by FO². We prove that FO² can express precisely the same properties as linear temporal logic with only the unary temporal operators: “next,” “previously,” “sometime in the future,” and “sometime in the past,” a logic we denote by unary-TL Moreover, our translation from FO² to unary-TL converts every FO² formula to an equivalent unary-TL formula that is at most exponentially larger and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is essentially optimal. While satisfiability for full linear temporal logic, as well as for unary-TL, is known to be PSPACE-complete, we prove that satisfiability for FO² is NEXP-complete, in sharp contrast to the fact that satisfiability for FO³ has nonelementary computational complexity. Our NEXP upper bound for FO² satisfiability has the advantage of being in terms of the quantifier depth of the input formula. It is obtained using a small model property for FO² of independent interest, namely, a satisfiable FO² formula has a model whose size is at most exponential in the quantifier depth of the formula. Using our translation from FO² to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.     

Satisfiability problems for propositional calculi

For each fixed set of Boolean connectives, how hard is it to determine satisfiability for formulas with only those connectives? We show that a condition sufficient for NP-completeness is that the functionx Λ ~ y be representable, and that any set of connectives not capable of representing this function has a polynomial-time satisfiability problem.     

A decomposition based algorithm for maximal contractions

This paper proposes a decomposition based algorithm for revision problems in classical propositional logic. A set of decomposing rules are presented to analyze the satisfiability of formulas. The satisfiability of a formula is equivalent to the satisfiability of a set of literal sets. A decomposing function is constructed to calculate all satisfiable literal sets of a given formula. When expressing the satisfiability of a formula, these literal sets are equivalent to all satisfied models of such formula. A revision algorithm based on this decomposing function is proposed, which can calculate maximal contractions of a given problem. In order to reduce the memory requirement, a filter function is introduced. The improved algorithm has a good performance in both time and space perspectives.     

Transforming equality logic to propositional logic

We investigate and compare various ways of transforming equality formulas to propositional formulas, in order to be able to solve satisfiability in equality logic by means of satisfiability in propositional logic. We propose equality substitution as a new approach combining desirable properties of earlier methods, we prove its correctness and show its applicability by experiments.     

Simple CAD Construction and its Applications

This paper presents a method for the simplification of truth-invariant cylindrical algebraic decompositions (CADs). Examples are given that demonstrate the usefulness of the method in speeding up the solution formula construction phase of the CAD-based quantifier elimination algorithm. Applications of the method to the construction of truth-invariant CADs for very large quantifier-free formulas and quantifier elimination of non-prenex formulas are also discussed.     

Game Over: The Foci Approach to LTL Satisfiability and Model Checking

Focus games have been shown to yield game-theoretical characterisations for the satisfiability and the model checking problem for various temporal logics. One of the players is given a tool – the focus – that enables him to show the regeneration of temporal operators characterised as least or greatest fixpoints. His strategy usually is build upon a priority list of formulas and, thus, is not positional. This paper defines foci games for satisfiability of LTL formulas. Strategies in these games are trivially positional since they parallelise all of the focus player's choices, thus resulting in a 1-player game in effect. The games are shown to be correct and to yield smaller (counter-)models than the focus games. Finally, foci games for model checking LTL are defined as well.     

Partial words and a theorem of Fine and Wilf revisited

A word of length n over a finite alphabet A is a map from {0,…,n−1} into A. A partial word of length n over A is a partial map from {0,…,n−1} into A. In the latter case, elements of {0,…,n−1} without image are called holes (a word is just a partial word without holes). In this paper, we extend a fundamental periodicity result on words due to Fine and Wilf to partial words with two or three holes. This study was initiated by Berstel and Boasson for partial words with one hole. Partial words are motivated by molecular biology.     

PSL可满足问题的计算复杂度

PSL是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL和分支时序逻辑OBE两部分。由于OBE就是CTL,因此论文重点研究FL逻辑。理论上已证明许多难解的问题都可多项式变换为“可满足性”问题,“可满足性”问题是研究时序逻辑的核心问题之一,并已成为程序验证的一种有力工具;而计算复杂度是“可满足性”问题需要解决的最深刻的方向之一,其研究意义在于它可作为解决一类问题的难度的标准。文中在利用“铺砖模型”基础上,推导并得出FL的“可满足性”问题的计算复杂度为EXPSPACE—hard,这对正确评价解决该问题的各种算法的效率,进而确定对已有算法的改进余地具有重要的指导意义。     

A satisfiability algorithm and average-case hardness for formulas over the full binary basis

We present a moderately exponential time algorithm for the satisfiability of Boolean formulas over the full binary basis. For formulas of size at most cn, our algorithm runs in time ${2^{(1-\mu_{c})n}}$ for some constant μ _c  > 0. As a byproduct of the running time analysis of our algorithm, we obtain strong average-case hardness of affine extractors for linear-sized formulas over the full binary basis.     

Probability logic and optimization SAT: The PSAT and CPA models

Both probabilistic satisfiability (PSAT) and the check of coherence of probability assessment (CPA) can be considered as probabilistic counterparts of the classical propositional satisfiability problem (SAT). Actually, CPA turns out to be a particular case of PSAT; in this paper, we compare the computational complexity of these two problems for some classes of instances. First, we point out the relations between these probabilistic problems and two well known optimization counterparts of SAT, namely Max SAT and Min SAT. We then prove that Max SAT with unrestricted weights is NP-hard for the class of graph formulas, where Min SAT can be solved in polynomial time. In light of the aforementioned relations, we conclude that PSAT is NP-complete for ideal formulas, where CPA can be solved in linear time.     

Infinite words and biprefix codes

Let A be an alphabet and ƒ be a right infinite word on A. If ƒ is not ultimately periodic then there exists an infinite set {v_ii0} of (finite) words on A such that ƒ=v₀v₁…v_i…, {v_ii1} is a biprefix code and v_i≠v_j for positive integers i≠j.