The at-most-k constraint is ubiquitous in combinatorial problems, and numerous SAT encodings are available for the constraint. Prior experiments have shown the competitiveness of the sequential-counter encoding for k $>$ 1, and have excluded the parallel-counter encoding, which is more compact that the binary-adder encoding, from consideration due to its incapability of enforcing arc consistency through unit propagation. This paper presents an experiment that shows astounding performance of the binary-adder encoding for the at-most-k constraint.
Barcelogic（巴塞罗逻辑公司）；Technische Universität Berlin（柏林工业大学）；Monash University（莫纳什大学）
Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encodings to Boolean satisfiability (SAT) format of conjunctive normal form perform poorly in problems with these constraints in comparison with SAT modulo theories (SMT), lazy clause generation (LCG) or mixed integer programming (MIP) solvers. In this paper we explore and categorize SAT encodings for linear integer constraints. We define new SAT encodings based on multi-valued decision diagrams, and sorting networks. We compare…
In the last two decades, modal and description logics have been applied to numerous areas of computer science, including knowledge representation, formal verification, database theory, distributed computing and, more recently, semantic web and ontologies. For this reason, the problem of automated reasoning in modal and description logics has been thoroughly investigated. In particular, many approaches have been proposed for efficiently handling the satisfiability of the core normal modal logic K(m), and of its notational variant, the description logic ALC. Although simple in structure, K(m)/AL…
Ben Gurion University of the Negev（本古里安大学）；Cadence Design Systems（楷登电子设计系统公司）；The University of Melbourne（墨尔本大学）
We present an approach to propagation based solving, Boolean equi-propagation, where constraints are modelled as propagators of information about equalities between Boolean literals. Propagation based solving applies this information as a form of partial evaluation resulting in optimized SAT encodings. We demonstrate for a variety of benchmarks that our approach results in smaller CNF encodings and leads to speed-ups in solving times.
We present an executable formally verified SAT encoding of classical AI planning. We use the theorem prover Isabelle/HOL to perform the verification. We experimentally test the verified encoding and show that it can be used for reasonably sized standard planning benchmarks. We also use it as a reference to test a state-of-the-art SAT-based planner, showing that it sometimes falsely claims that problems have no solutions of certain lengths.
One of the effective model checking methods is to utilize the efficient decision procedure of SAT (or SMT) solvers. In a SAT-based model checking, a system and its property are encoded into a set of logic formulas and the safety is checked based on the satisfiability of the formulas. As the encoding methods are improved and crafted (e.g., k-induction and IC3/PDR), verifying their correctness becomes more important. This research aims at a formal verification of the SMC methods using the Coq proof assistant. Our contributions are twofold: (1) We specify the basic encoding methods, k-induction a…
Cardinality constraints are important in many Sat problems; previous studies provide contradictory conclusions about the best encoding to use. Here, three encodings are compared: Sinz's sequential-counter, Bailleux and Boufkhad's tree-based, and Ab\'ıo and coworkers' sort-based approaches. The sequential-counter approach is found to be the fastest of these for a range of related, combinatorial test cases. All encodings permit multiple solutions in the auxiliary variables for a single solution to the main variables; the numbers of multiple solutions can be very large, and might impede a Sat sol…
Concurrent systems are notoriously difficult to analyze, and technological advances such as weak memory architectures greatly compound this problem. This has renewed interest in partial order semantics as a theoretical foundation for formal verification techniques. Among these, symbolic techniques have been shown to be particularly effective at finding concurrency-related bugs because they can leverage highly optimized decision procedures such as SAT/SMT solvers. This paper gives new fundamental results on partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency.…
Satisfiability Testing (SAT) techniques are well-established in classical computing where they are used to solve a broad variety of problems, e.g., in the design of classical circuits and systems. Analogous to the classical realm, quantum algorithms are usually modelled as circuits and similar design tasks need to be tackled. Thus, it is natural to pose the question whether these design tasks in the quantum realm can also be approached using SAT techniques. To the best of our knowledge, no SAT formulation for arbitrary quantum circuits exists and it is unknown whether such an approach is feasi…
Department of Computer Science, University of Oxford（牛津大学计算机科学系）；INESC-ID / Instituto Superior Técnico, Universidade de Lisboa（里斯本大学高等技术学院/INESC-ID（里斯本大学工程与计算机科学研究所））
Pseudo-Boolean constraints, also known as 0-1 Integer Linear Constraints, are used to model many real-world problems. A common approach to solve these constraints is to encode them into a SAT formula. The runtime of the SAT solver on such formula is sensitive to the manner in which the given pseudo-Boolean constraints are encoded. In this paper, we propose generalized Totalizer encoding (GTE), which is an arc-consistency preserving extension of the Totalizer encoding to pseudo-Boolean constraints. Unlike some other encodings, the number of auxiliary variables required for GTE does not depend o…
We present BEE, a compiler which enables to encode finite domain constraint problems to CNF. Using BEE both eases the encoding process for the user and also performs transformations to simplify constraints and optimize their encoding to CNF. These optimizations are based primarily on equi-propagation and on partial evaluation, and also on the idea that a given constraint may have various possible CNF encodings. Often, the better encoding choice is made after constraint simplification. BEE is written in Prolog and integrates directly with a SAT solver through a suitable Prolog interface. We dem…
A Pseudo-Boolean (PB) constraint is a linear arithmetic constraint over Boolean variables. PB constraints are convenient and widely used in expressing NP-complete problems. We introduce a new, two step, method for transforming PB constraints to propositional CNF formulas. The first step involves re-writing each PB constraint as a conjunction of PB-Mod constraints. The advantage is that PB-Mod constraints are easier to transform to CNF. In the second step, we translate each PB-Mod constraints, obtained in the previous step, into CNF. The resulting CNF formulas are small, and unit propagation ca…
The reactive synthesis problem is to compute a system satisfying a given specification in temporal logic. Bounded synthesis is the approach to bound the maximum size of the system that we accept as a solution to the reactive synthesis problem. As a result, bounded synthesis is decidable whenever the corresponding verification problem is decidable, and can be applied in settings where classic synthesis fails, such as in the synthesis of distributed systems. In this paper, we study the constraint solving problem behind bounded synthesis. We consider different reductions of the bounded synthesis …
As systems become ever more complex, verification becomes more main stream. Event-B and Alloy are two formal specification languages based on fairly different methodologies. While Event-B uses theorem provers to prove that invariants hold for a given specification, Alloy uses a SAT-based model finder. In some settings, Event-B invariants may not be proved automatically, and so the often difficult step of interactive proof is required. One solution for this problem is to validate invariants with model checking. This work studies the encoding of Event-B machines and contexts to Alloy in order to…
This paper introduces a propositional encoding for lexicographic path orders in connection with dependency pairs. This facilitates the application of SAT solvers for termination analysis of term rewrite systems based on the dependency pair method. We address two main inter-related issues and encode them as satisfiability problems of propositional formulas that can be efficiently handled by SAT solving: (1) the combined search for a lexicographic path order together with an \emph{argument filtering} to orient a set of inequalities; and (2) how the choice of the argument filtering influences the…
We study the precise computational complexity of deciding satisfiability of first-order quantified formulas over the theory of fixed-size bit-vectors with binary-encoded bit-widths and constants. This problem is known to be in EXPSPACE and to be NEXPTIME-hard. We show that this problem is complete for the complexity class AEXP(poly) -- the class of problems decidable by an alternating Turing machine using exponential time, but only a polynomial number of alternations between existential and universal states.
This paper investigates approaches to parallelizing Bounded Model Checking (BMC) for shared memory environments as well as for clusters of workstations. We present a generic framework for parallelized BMC named Tarmo. Our framework can be used with any incremental SAT encoding for BMC but for the results in this paper we use only the current state-of-the-art encoding for full PLTL. Using this encoding allows us to check both safety and liveness properties, contrary to an earlier work on distributing BMC that is limited to safety properties only. Despite our focus on BMC after it has been trans…
