226 citations · 240 across the 10 of their papers we have counts for
11 papers
Disjoint Partial Enumeration without Blocking Clauses
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
A basic algorithm for enumerating disjoint propositional models (disjoint AllSAT) is based on adding blocking clauses incrementally, ruling out previously found models. On the one…
Stratified Certification for k-Induction
Emily Yu, Nils Froleyks, Armin Biere +1
Our recently proposed certification framework for bit-level k-induction-based model checking has been shown to be quite effective in increasing the trust of verification results ev…
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
Mathias Fleury, Armin Biere
We give a first account of our new parallel SAT solver Gimsatul. Its key feature is to share clauses physically in memory instead of copying them, which is the method of other stat…
On Enumerating Short Projected Models
Sibylle Möhle, Roberto Sebastiani, Armin Biere
Propositional model enumeration, or All-SAT, is the task to record all models of a propositional formula. It is a key task in software and hardware verification, system engineering…
Revisiting Decision Diagrams for SAT
Tom van Dijk, Rüdiger Ehlers, Armin Biere
Symbolic variants of clause distribution using decision diagrams to eliminate variables in SAT were shown to perform well on hard combinatorial instances. In this paper we revisit…
Blocked Clauses in First-Order Logic
Benjamin Kiesl, Martin Suda, Martina Seidl +2
Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees t…
Local Redundancy in SAT: Generalizations of Blocked Clauses
Benjamin Kiesl, Martina Seidl, Hans Tompits +1
Clause-elimination procedures that simplify formulas in conjunctive normal form play an important role in modern SAT solving. Before or during the actual solving process, such proc…
Concurrent Cube-and-Conquer
Peter van der Tak, Marijn J. H. Heule, Armin Biere
Recent work introduced the cube-and-conquer technique to solve hard SAT instances. It partitions the search space into cubes using a lookahead solver. Each cube is tackled by a con…
Covered Clause Elimination
Marijn Heule, Matti Järvisalo, Armin Biere
Generalizing the novel clause elimination procedures developed in [M. Heule, M. Järvisalo, and A. Biere. Clause elimination procedures for CNF formulas. In Proc. LPAR-17, volume 63…
Two sources are better than one for increasing the Kolmogorov complexity of infinite sequences
Marius Zimand
The randomness rate of an infinite binary sequence is characterized by the sequence of ratios between the Kolmogorov complexity and the length of the initial segments of the sequen…
Linear Encodings of Bounded LTL Model Checking
Armin Biere, Keijo Heljanko, Tommi Junttila +2
We consider the problem of bounded model checking (BMC) for linear temporal logic (LTL). We present several efficient encodings that have size linear in the bound. Furthermore, we…