scholarly journals Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling

10.29007/jhd7 ◽  
2018 ◽  
Author(s):  
Armin Biere
Keyword(s):  
Data Structures ◽  
State Of The Art ◽  
Design Principles ◽  
The State ◽  
Memory Usage ◽  
Design And Implementation ◽  
Sat Solver ◽  
Compact Data Structures ◽  
Cache Efficiency ◽  
Implementation Aspects

One of the design principles of the state-of-the-art SAT solver Lingeling is to use as compact data structures as possible. These reduce memory usage, increase cache efficiency and thus improve run-time, particularly, when using multiple solver instances on multi-core machines, as in our parallel portfolio solver Plingeling and our cube and conquer solver Treengeling. The scheduler of a dozen inprocessing algorithms is an important aspect of Lingeling as well. In this talk we explain these design and implementation aspects of Lingeling and discuss new direction of solver design.

scholarly journals Framework for Generating Configurable SAT Solvers

2011 ◽  
Vol 6 (1) ◽  
pp. 50-59
Author(s):  
Bernardo C. Vieira ◽  
Fabrício V. Andrade ◽  
Antônio O. Fernandes
Keyword(s):  
State Of The Art ◽  
The State ◽  
Equivalence Checking ◽  
Decision Heuristics ◽  
Sat Solvers ◽  
The Third ◽  
Sat Solver ◽  
Run Time

The state-of-the-art SAT solvers usually share the same core techniques, for instance: the watched literals structure, conflict clause recording and non-chronological backtracking. Nevertheless, they might differ in the elimination of learnt clauses, as well as in the decision heuristic. This article presents a framework for generating configurable SAT solvers. The proposed framework is composed of the following components: a Base SAT Solver, a Perl Preprocessor, XML files (Solver Description and Heuristics Description files) to describe each heuristic as well as the set of heuristics that the generated solver uses. This solvers may use several techniques and heuristics such as those implemented in BerkMin, and in Equivalence Checking of Dissimilar Circuits, and also in Minisat. In order to demonstrate the effectiveness of the proposed framework, this article also presents three distinct SAT solver instances generated by the framework to address a complex and challenging industry problem: the Combinational Equivalence Checking problem (CEC).The first instance is a SAT solver that uses BerkMin and Dissimilar Circuits core techniques except the learnt clause elimination heuristic that has been adapted from Minisat; the second is another solver that combines BerkMin and Minisat decision heuristics at run-time; and the third is yet another SAT solver that changes the database reducing heuristic at run-time. The experiments demonstrate that the first SAT solver generated is a faster solver than state-of-the-art SAT solver BerkMin for several instances as well as for Minisat in almost every instance.

A Fresh Look at Zones and Octagons

2021 ◽  
Vol 43 (3) ◽  
pp. 1-51
Author(s):  
Graeme Gange ◽  
Zequn Ma ◽  
Jorge A. Navas ◽  
Peter Schachte ◽  
Harald Søndergaard ◽  
...  
Keyword(s):  
Data Structures ◽  
Program Analysis ◽  
Software Verification ◽  
State Of The Art ◽  
The State ◽  
Bound Constraints ◽  
Data Structures And Algorithms ◽  
Alternative Approaches ◽  
Abstract Domains ◽  
Automated Discovery

Zones and Octagons are popular abstract domains for static program analysis. They enable the automated discovery of simple numerical relations that hold between pairs of program variables. Both domains are well understood mathematically but the detailed implementation of static analyses based on these domains poses many interesting algorithmic challenges. In this article, we study the two abstract domains, their implementation and use. Utilizing improved data structures and algorithms for the manipulation of graphs that represent difference-bound constraints, we present fast implementations of both abstract domains, built around a common infrastructure. We compare the performance of these implementations against alternative approaches offering the same precision. We quantify the differences in performance by measuring their speed and precision on standard benchmarks. We also assess, in the context of software verification, the extent to which the improved precision translates to better verification outcomes. Experiments demonstrate that our new implementations improve the state of the art for both Zones and Octagons significantly.

scholarly journals Science of Analytical Reasoning

2009 ◽  
Vol 8 (4) ◽  
pp. 254-262 ◽  
Author(s):  
William Ribarsky ◽  
Brian Fisher ◽  
William M. Pottenger
Keyword(s):  
Real World ◽  
Visual Analytics ◽  
State Of The Art ◽  
Design Principles ◽  
The State ◽  
Future Research ◽  
Future Directions ◽  
Analytical Reasoning ◽  
Tools And Methods ◽  
Real World Problems

There has been progress in the science of analytical reasoning and in meeting the recommendations for future research that were laid out when the field of visual analytics was established. Researchers have also developed a group of visual analytics tools and methods that embody visual analytics principles and attack important and challenging real-world problems. However, these efforts are only the beginning and much study remains to be done. This article examines the state of the art in visual analytics methods and reasoning and gives examples of current tools and capabilities. It shows that the science of visual analytics needs interdisciplinary efforts, indicates some of the disciplines that should be involved and presents an approach to how they might work together. Finally, the article describes some gaps, opportunities and future directions in developing new theories and models that can be enacted in methods and design principles and applied to significant and complex practical problems and data.

scholarly journals Property Directed Reachability for Automated Planning

2014 ◽  
Vol 50 ◽  
pp. 265-319 ◽  
Author(s):  
M. Suda
Keyword(s):  
Model Checking ◽  
State Of The Art ◽  
Automated Planning ◽  
The State ◽  
Experimental Comparison ◽  
Specific Procedure ◽  
Transition Systems ◽  
Planning Algorithm ◽  
Sat Solver ◽  
Recent Method

Property Directed Reachability (PDR) is a very promising recent method for deciding reachability in symbolically represented transition systems. While originally conceived as a model checking algorithm for hardware circuits, it has already been successfully applied in several other areas. This paper is the first investigation of PDR from the perspective of automated planning. Similarly to the planning as satisfiability paradigm, PDR draws its strength from internally employing an efficient SAT-solver. We show that most standard encoding schemes of planning into SAT can be directly used to turn PDR into a planning algorithm. As a non-obvious alternative, we propose to replace the SAT-solver inside PDR by a planning-specific procedure implementing the same interface. This SAT-solver free variant is not only more efficient, but offers additional insights and opportunities for further improvements. An experimental comparison to the state of the art planners finds it highly competitive, solving most problems on several domains.

Effective Design and Implementation of Distributed Business Information Systems

2013 ◽  
Vol 307 ◽  
pp. 451-454
Author(s):  
Pavel Ocenasek
Keyword(s):  
Information Systems ◽  
State Of The Art ◽  
Protocol Design ◽  
Short Introduction ◽  
Business Information Systems ◽  
Design And Implementation ◽  
Business Information ◽  
Payment Protocol ◽  
Implementation Aspects ◽  
Effective Design

This paper deals with the effective design and implementation aspects of distributed business information systems. After a short introduction to the state of the art, it proposes a study on a payment protocol design, which is based on the composition method.

scholarly journals LLMC: Verifying High-Performance Software

2021 ◽  
pp. 690-703
Author(s):  
Freark I. van der Berg
Keyword(s):  
Model Checking ◽  
Data Structures ◽  
High Performance ◽  
State Of The Art ◽  
The State ◽  
State Model ◽  
Test Suite ◽  
Model Checker ◽  
Unit Tests

AbstractMulti-threaded unit tests for high-performance thread-safe data structures typically do not test all behaviour, because only a single scheduling of threads is witnessed per invocation of the unit tests. Model checking such unit tests allows to verify all interleavings of threads. These tests could be written in or compiled to LLVM IR. Existing LLVM IR model checkers like divine and Nidhugg, use an LLVM IR interpreter to determine the next state. This paper introduces llmc, a multi-core explicit-state model checker of multi-threaded LLVM IR that translates LLVM IR to LLVM IR that is executed instead of interpreted. A test suite of 24 tests, stressing data structures, shows that on average llmc clearly outperforms the state-of-the-art tools divine and Nidhugg.

scholarly journals Mobile Augmented Reality in Museums : Towards Enhancing Visitor's Learning Experience

2017 ◽  
Vol 17 (1) ◽  
pp. 21-31 ◽  
Author(s):  
Nehla Ghouaiel ◽  
Samir Garbaya ◽  
Jean-Marc Cieutat ◽  
Jean-Pierre Jessel
Keyword(s):  
Augmented Reality ◽  
Empirical Study ◽  
State Of The Art ◽  
Learning Experience ◽  
The State ◽  
Mobile Augmented Reality ◽  
Work Of Art ◽  
Related Model ◽  
Design And Implementation

This article presents the design and implementation of a handheld Augmented Reality (AR) system called Mobile Augmented Reality Touring System (M.A.R.T.S). The results of experiments conducted during museum visits using this system are also described. These experiments aim at studying how such a tool can transform the visitor's learning experience by comparing it to two widely used museum systems. First, we present the museum's learning experience and a related model which emerged from the state of the art. This model consists of two types of activity experienced by the observer of a work of art: sensitive and analytical. Then, we detail M.A.R.T.S architecture and implementation. Our empirical study highlights the fact that AR can direct visitors' attention by emphasizing and superimposing. Its magnifying and sensitive effects are well perceived and appreciated by visitors. The obtained results reveal that M.A.R.T.S contributes to a worthwhile learning experience.

scholarly journals Studies on River Training

Water ◽  
2020 ◽  
Vol 12 (11) ◽  
pp. 3100
Author(s):  
Erik Mosselman
Keyword(s):  
The Netherlands ◽  
Case Studies ◽  
State Of The Art ◽  
Low Cost ◽  
Vegetation Management ◽  
The State ◽  
Special Issue ◽  
Design And Implementation ◽  
River Training ◽  
And Behavior

This editorial regards a Special Issue of Water on river training. It introduces five papers in a framework of history, fundamentals, case studies and future. Four papers result from decades of experience with innovation, planning, design and implementation of river training works on rivers in Colombia, the Rhine branches in the Netherlands and the Brahmaputra-Jamuna River in Bangladesh. A fifth paper reviews the state-of-the-art in predicting and influencing the formation and behavior of river bars. The editorial argues that the future lies in more flexible river training, using a mix of innovative permanent structures and recurrent interventions such as dredging, sediment nourishment, vegetation management and low-cost temporary structures.

scholarly journals Improving Clairvoyant: reduction algorithm resilient to imbalanced process arrival patterns

2020 ◽  
Author(s):  
Jerzy Proficz ◽  
Krzysztof M. Ocetkiewicz
Keyword(s):  
State Of The Art ◽  
The State ◽  
Memory Usage ◽  
Reduction Algorithm ◽  
Arrival Times ◽  
Fold Reduction ◽  
Improved Performance ◽  
Algorithm Implementation

AbstractThe Clairvoyant algorithm proposed in “A novel MPI reduction algorithm resilient to imbalances in process arrival times” was analyzed, commented and improved. The comments concern handling certain edge cases in the original pseudocode and description, i.e., adding another state of a process, improved cache friendliness more precise complexity estimations and some other issues improving the robustness of the algorithm implementation. The proposed improvements include skipping of idle loop rounds, simplifying generation of the ready set and management of the state array and an about 90-fold reduction in memory usage. Finally an extension enabling process arrival times (PATs) prediction was added: an additional background thread used to exchange the data with the PAT estimations. The performed tests, with a dedicated mini-benchmark executed in an HPC environment, showed correctness and improved performance of the solution, with comparison to the original or other state-of-the-art algorithms.

scholarly journals BIRD: Engineering an Efficient CNF-XOR SAT Solver and Its Applications to Approximate Model Counting

2019 ◽  
Vol 33 ◽  
pp. 1592-1599 ◽  
Author(s):  
Mate Soos ◽  
Kuldeep S. Meel
Keyword(s):  
Probabilistic Reasoning ◽  
State Of The Art ◽  
Fundamental Problem ◽  
Approximate Model ◽  
Affirmative Answer ◽  
The State ◽  
Boolean Formula ◽  
Wide Range ◽  
Model Counting ◽  
Sat Solver

Given a Boolean formula φ, the problem of model counting, also referred to as #SAT is to compute the number of solutions of φ. Model counting is a fundamental problem in artificial intelligence with a wide range of applications including probabilistic reasoning, decision making under uncertainty, quantified information flow, and the like. Motivated by the success of SAT solvers, there has been surge of interest in the design of hashing-based techniques for approximate model counting for the past decade. We profiled the state of the art approximate model counter ApproxMC2 and observed that over 99.99% of time is consumed by the underlying SAT solver, CryptoMiniSat. This observation motivated us to ask: Can we design an efficient underlying CNF-XOR SAT solver that can take advantage of the structure of hashing-based algorithms and would this lead to an efficient approximate model counter? The primary contribution of this paper is an affirmative answer to the above question. We present a novel architecture, called BIRD, to handle CNF-XOR formulas arising from hashingbased techniques. The resulting hashing-based approximate model counter, called ApproxMC3, employs the BIRD framework in its underlying SAT solver, CryptoMiniSat. To the best of our knowledge, we conducted the most comprehensive study of evaluation performance of counting algorithms involving 1896 benchmarks with computational effort totaling 86400 computational hours. Our experimental evaluation demonstrates significant runtime performance improvement for ApproxMC3 over ApproxMC2. In particular, we solve 648 benchmarks more than ApproxMC2, the state of the art approximate model counter and for all the formulas where both ApproxMC2 and ApproxMC3 did not timeout and took more than 1 seconds, the mean speedup is 284.40 – more than two orders of magnitude.

Sign in / Sign up

Export Citation Format

Share Document