Decision levels are stable: towards better SAT heuristics

We shed new light on the Literal Block Distance (LBD) and glue-based heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals we define, by a real value between 0 and 1, how sticky they are, basically, how frequently they are set at the same decision level.By means of a careful and detailed experimental setup and analysis, we confirm the following quite surprising fact: given a SAT instance, when running different CDCL SAT solvers on it, no matter their settings or random seeds, the stickiness relation between literals is always very similar, in a precisely defined sense.We analyze how quickly stickiness stabilizes in a run (quite quickly), and show that it is stable even under different encodings of cardinality constraints. We then describe how and why these solid new insights lead to heuristics refinements for SAT (and extensions, such as SMT) and improved information sharing in parallel solvers.

Modified method of parallel matrix sweep

The topic of this paper refers to efficient parallel solvers of block-tridiagonal linear systems of equations. Such systems occur in numerous modeling problems and require usage of high-performance multicore computation systems. One of the widely used methods for solving block-tridiagonal linear systems in parallel is the original block-tridiagonal sweep method. We consider the algorithm based on the partitioning idea. Firstly, the initial matrix is split into parts and transformations are applied to each part independently to obtain equations of a reduced block-tridiagonal system. Secondly, the reduced system is solved sequentially using the classic Thomas algorithm. Finally, all the parts are solved in parallel using the solutions of a reduced system. We propose a modification of this method. It was justified that if known stability conditions for the matrix sweep method are satisfied, then the proposed modification is stable as well.

Efficient discontinuous finite difference meshes for 3-D Laplace–Fourier domain seismic wavefield modelling in acoustic media with embedded boundaries

SUMMARY Simulation of acoustic wave propagation in the Laplace–Fourier (LF) domain, with a spatially uniform mesh, can be computationally demanding especially in areas with large velocity contrasts. To improve efficiency and convergence, we use 3-D second- and fourth-order velocity-pressure finite difference (FD) discontinuous meshes (DM). Our DM algorithm can use any spatial discretization ratio between meshes. We evaluate direct and iterative parallel solvers for computational speed, memory requirements and convergence. Benchmarks in realistic 3-D models and topographies show more efficient and stable results for DM with direct solvers than uniform mesh results with iterative solvers.

Automatic Construction of Parallel Portfolios via Explicit Instance Grouping

Exploiting parallelism is becoming more and more important in designing efficient solvers for computationally hard problems. However, manually building parallel solvers typically requires considerable domain knowledge and plenty of human effort. As an alternative, automatic construction of parallel portfolios (ACPP) aims at automatically building effective parallel portfolios based on a given problem instance set and a given rich configuration space. One promising way to solve the ACPP problem is to explicitly group the instances into different subsets and promote a component solver to handle each of them. This paper investigates solving ACPP from this perspective, and especially studies how to obtain a good instance grouping. The experimental results on two widely studied problem domains, the boolean satisfiability problems (SAT) and the traveling salesman problems (TSP), showed that the parallel portfolios constructed by the proposed method could achieve consistently superior performances to the ones constructed by the state-of-the-art ACPP methods, and could even rival sophisticated hand-designed parallel solvers.