ABSTRACT. Modern CDCL (conflict-driven clause learning) SAT solvers are used for many practical applications. One of the key ingredients of state-of-the-art CDCL solvers are efficient restart schemes. The main contribution of this work is an extensive empirical evaluation of various restart strategies. We show that optimal static restart intervals are not only correlated with the satisfiability status of a certain instance, but also with the more specific problem class of the given benchmark. We further compare uniform restart intervals with the performance of non-uniform restart schemes, such as Luby restarts. Finally, we revisit the dynamic restart strategy used in Glucose and propose a new variant thereof, which is based on the concept of exponential moving averages. The resulting implementation in Lingeling improves state-of-the-art performance in SAT solving.

ABSTRACT. In recent years a lot of effort has been expended in determining if SAT solver performance is predictable. However, the work in this area invariably focuses on individual machines, and often on individual solvers. It is unclear whether predictions made on a specific solver and machine are accurate when translated to other solvers and hardware. In this work we consider five state-of-the-art solvers, 26 machines and 143 feature instances selected from the 2011 to 2014 SAT competitions. Using combinations of solvers, machines and instances we present four results: First, we show that UNSAT instances are more predictable than corresponding SAT instances. Second, we show that the number of cores in a machine has more impact on performance than L2 cache size. Third, we show that instances with fewer reused clauses are more CPU bound than those where clause reuse is high. Finally, we make accurate predictions of solution time for each of the instances considered across a diverse set of machines.

ABSTRACT. Natural computing is a new discipline that aims to develop nature-inspired computers by using physical dynamics and fluctuations of interacting devices. Inspired by the amoeba, which exhibits spatiotemporal oscillatory dynamics and sophisticated computing capabilities, we extracted the essential spatiotemporal dynamics by which the amoeba solves computationally demanding problems. Our dynamical system model, AmoebaSAT, runs on conventional digital computers and functions as an algorithm for searching for a solution to the satisfiability problem (SAT). Moreover, AmoebaSAT can be implemented using nanoelectronic and nanophotonic devices. In this study, performing Monte Carlo simulations using a digital computer, we show that AmoebaSAT outperforms a randomized version of the GSAT algorithm for randomly generated 10000 variable 3-SAT instances. Thus, when implemented using the nanodevices, AmoebaSAT will open up a new computing paradigm that might enable high-speed problem solving with low power consumption.

ABSTRACT. It is said that both intensive and diversified search are important for effective SAT solver. However so far, the balance between intensive search and search diversification are only kept heuristically with some solver’s features. We concern that quantitative balancing of intensive and diversified search leads to more effective SAT solver and propose Search Similarity Index (SSI) to measure the balances by comparison with a pair of searching direction from now. By using SSI, we can evaluate some methods which is assumed its effectiveness is cause of changing search space. And we confirmed that the effectiveness of parallelization is about twice by decreasing searching duplication with SSI on portfolio parallel SAT solver.

ABSTRACT. An approach to model counting based on regular expressions is explored. Model counting is treated as a string counting problem, where the strings encode variable assignments, and is solved generating a regular expression that defines the assignments and calculating how many strings satisfy it. Since this approach depends only on properties of regular expressions, any alphabet can be used, not just the {0,1} alphabet of CNF formulas. An algorithm based on inclusion-exclusion is proposed, and the inclusion-exclusion summation is performed in a special order that exploits the structure of the problem to enable memoization. Indeed, for formulas that don't have any non-disjoint clauses, it is often possible to index the clauses so that the algorithm runs in polynomial time. Since the algorithm's performance is largely dependent on the indexing of the formula, this provides a "backdoor" into the problem based on finding efficient indexing heuristics and algorithms, and the increased generality of the string counting problem can allow for more efficient reductions from other problems in #P.

ABSTRACT. Due to recent advances in maximum satisfiability (MaxSAT) solving techniques, MaxSAT, and especially its weighted partial generalization, are being used for solving an increasing range of Boolean optimization problems. In this paper, we overview various important optimization problems arising from data analysis and machine learning and how they have been recently successfully approached via MaxSAT. Our motivation for this work is three-fold: (i) We aim to highlight important hard real-world optimization problems arising from data analysis and machine learning, representing somewhat atypical applications of SAT-based solver technology. (ii) To address the problem of current lack of heterogeneity in benchmark sets available for evaluating MaxSAT solvers, we provide a benchmark library of MaxSAT instances encoding different data analysis and machine learning problems. (iii) We want to advocate extending the current state-of-the-art MaxSAT solver to natively support real-valued weights for soft clauses. Indeed, in each of the problem domains described, the use of real-valued plays an integral role; more generally, we believe that by directly supporting real-valued weights, MaxSAT could be made a more attractive choice as a Boolean optimization paradigm for a wider base of end-users.

ABSTRACT. Contemporary SAT solvers emit unsatisfiability proofs in the DRAT format to increase confidence in their answers. The state-of-the-art proof verifier drattrim uses backward-checking and deletion information to efficiently check unsatisfiability results. Verifying large proofs still takes as long as solving a formula, and therefore parallelization seems to be a promising approach. However, Heule et al. that parallelization of the backward-checking procedure is difficult since clausal proofs do not include dependency information. In this paper, we present a parallelization approach and a prototypical implementation that scales almost linearly compared to its sequential version.