ABSTRACT. Covertly computational insights have influenced the Theory of Evolution from the very start. I shall discuss recent work on some central problems in Evolution that was inspired and informed by computational ideas. Considerations about the performance of genetic algorithms led to a novel theory of the role of sex in Evolution based on the concept of mixability, the population genetic equations describing the evolution of a species can be reinterpreted as a repeated game between genes played through the multiplicative update algorithm, while a theorem on satisfiability can shed light on the emergence of complex adaptations.

ABSTRACT. We present a moderately exponential time polynomial space algorithm for sparse instances of Max SAT. Our algorithms run in time of the form $O(2^{(1-\mu(c))n})$ for instances with $n$ variables and $cn$ clauses. Our deterministic and randomized algorithm achieve $\mu(c) = \Omega(\frac{1}{c^2\log^2 c})$ and $\mu(c) = \Omega(\frac{1}{c \log^3 c})$ respectively. Previously, an exponential space deterministic algorithm with $\mu(c) = \Omega(\frac{1}{c\log c})$ was shown by Dantsin and Wolpert [SAT 2006] and a polynomial space deterministic algorithm with $\mu(c) = \Omega(\frac{1}{2^{O(c)}})$ was shown by Kulikov and Kutzkov [CSR 2007].

Our algorithms have three new features. They can handle instances with (1) weights and (2) hard constraints, and also (3) they can solve counting versions of Max SAT. Our deterministic algorithm is based on the combination of two techniques, width reduction of Schuler and greedy restriction of Santhanam. Our randomized algorithm uses random restriction instead of greedy restriction.

ABSTRACT. In this paper we propose a structural parameter of CNF formulas and use it to identify instances of weighted {\sc MaxSAT} and {\sc \#SAT} that can be solved in polynomial time. Given a CNF formula we say that a set of clauses is precisely satisfiable if there is some complete assignment satisfying these clauses only. Let the $\mathtt{ps}$-value of the formula be the number of precisely satisfiable sets of clauses. Applying the notion of branch decompositions to CNF formulas and using $\mathtt{ps}$-value as cut function, we define the $\mathtt{ps}$-width of a formula. For a formula given with a decomposition of polynomial $\mathtt{ps}$-width we show dynamic programming algorithms solving weighted {\sc MaxSAT} and {\sc \#SAT} in polynomial time. Combining with results of 'Belmonte and Vatshelle, Graph classes with structured neighborhoods and algorithmic applications, {\sc Theor. Comput. Sci.} 511: 54-65 (2013)' we get polynomial-time algorithms solving weighted {\sc MaxSAT} and {\sc \#SAT} for some classes of structured CNF formulas. For example, we get $\bigoh(n^4)$ algorithms for formulas having a linear ordering of variables and clauses such that for any variable $x$ occurring in clause $C$, if $x$ appears before $C$ then any variable between them also occurs in $C$, and if $C$ appears before $x$ then $x$ occurs also in any clause between them. Note that the class of incidence graphs of such formulas do not have bounded clique-width.

ABSTRACT. A number of MaxSat algorithms are based on the idea of generating unsatisfiable cores. A common approach is to use these cores to construct cardinality (or pseudo-boolean) constraints that are then added to the formula. Each iteration extracts a core from the modified formula. Hence, the cores generated are not just cores of the original formula, they are cores of more complicated formulas. The effectiveness of core based algorithms for MaxSat is strongly affected by the structure of the cores of the original formula. Hence it is natural to ask the question: how are the cores found by these algorithms related to the cores of the original formula? In this paper we provide a formal characterization of this relationship. Our characterization allows us to identify a possible inefficiency in these algorithms. Hence, finding ways to address it may lead to performance improvements in these state-of-the-art MaxSat algorithms.

ABSTRACT. Minimal Unsatisfiable Subsets (MUSes) and Minimal Correction Subsets (MCSes) are essential tools for the analysis of unsatisfiable formulas. MUSes and MCSes find a growing number of applications, that include abstraction refinement in software verification, type debugging, software package management and software configuration, among many others. In some applications, there can exist preferences over which clauses to include in computed MUSes or MCSes, but also in computed Maximal Satisfiable Subsets (MSSes). Moreover, different definitions of preferred MUSes, MCSes and MSSes can be considered. This paper revisits existing definitions of preferred MUSes, MCSes and MSSes of unsatisfiable formulas, and develops a preliminary characterization of the computational complexity of computing preferred MUSes, MCSes and MSSes. Moreover, the paper investigates which of the existing algorithms and pruning techniques can be applied for computing preferred MUSes, MCSes and MSSes. Finally, the paper shows that the computation of preferred sets can have significant impact in practical performance.

ABSTRACT. Recent work introduced an effective method to extract reduced unsatisfiable cores of CNF formulas as a by-product of validating clausal proofs emitted by conflict-driven clause learning SAT solvers. In this paper, we demonstrate that this method for trimming CNF formulas can also benefit state-of-the-art tools for the computation of a Minimal Unsatisfiable Subformula (MUS). Furthermore, we propose a number of techniques that improve the quality of trimming, and demonstrate a significant positive impact on the performance of MUS extractors from the improved trimming.

ABSTRACT. Today's SAT solvers have an enormous importance and impact in many practical settings. They are used as efficient back-end to solve many NP-complete problems. However, many reasoning problems are located at the second level of the Polynomial Hierarchy or even higher, and hence polynomial-time transformations to SAT are not possible, unless the hierarchy collapses. In certain cases one can break through these complexity barriers by fixed-parameter tractable (fpt) reductions which exploit structural aspects of problem instances in terms of problem parameters. Recent research established a general theoretical framework that supports the classification of parameterized problems on whether they admit such an fpt-reduction to SAT or not. We use this framework to analyze some problems that are related to Boolean satisfiability. We consider several natural parameterizations of these problems, and we identify for which of these an fpt-reduction to SAT is possible. The problems that we look at are related to minimizing an implicant of a DNF formula, minimizing a DNF formula, and satisfiability of quantified Boolean formulas.

ABSTRACT. Maximum Independet Set (MIS) is a well-known NP-hard graph problem, tightly related with other well known NP-hard graph problems, namely Minimum Vertex Cover (MVC) and Maximum Clique (MaxClq). This paper introduces a novel reduction of MIS into Minimum Satisfiability (MinSAT). Besides providing an alternative approach for solving MIS, the proposed reduction serves as a simpler alternative proof of the NP-hardness of MinSAT. The reduction naturally maps the vertices of a graph into clauses, without requiring the inclusion of hard clauses. Moreover, it is shown that the proposed reduction uses fewer variables and clauses than the existing alternative of mapping MIS into Maximum Satisfiability (MaxSAT). The paper develops a number of optimizations to the basic reduction, which significantly reduce the total number of variables used. The experimental evaluation considered the reductions described in the paper as well as existing state-of-the-art approaches. The results show that the proposed approaches based on MinSAT are competitive with existing approaches.

ABSTRACT. Simplification techniques for conjunctive normal form (CNF) formulas, used before (i.e., in preprocessing) and during (i.e., in inprocessing) search for satisfiability, have proven integral in speeding up SAT solvers in practice. Formula simplification tends to come with a price: in practice, the stronger the technique in terms of achieved simplification, the more costly in terms of computational effort it is to apply until fixpoint. However, formal understanding of the time complexity of different preprocessing techniques is rather limited at present. In this paper, we prove time-complexity lower bounds for different probing-based CNF simplification techniques, focusing on failed literal elimination and related techniques. More specifically, we show that improved algorithms for these simplification techniques would imply that the Strong Exponential Time Hypothesis (i.e., CNF-SAT is not solvable in time $2^{\epsilon n}$ for any $\epsilon<1$) is false.

ABSTRACT. Inspired by the recent work on parallel SAT solving, we present a lightweight approach for concurrently solving quantified Boolean formulas (QBFs). In particular, our approach abstains from globally exchanging information between working processes, but keeps learnt information only locally. To this end, we equipped the state-of-the-art QBF solver DepQBF with assumption-based reasoning and integrated it in our novel solver MPIDepQBF as backend solver. Extensive experiments on standard computers as well as on the supercomputer Tsubame show the impact of our approach.

ABSTRACT. The DRAT-trim tool is a satisfiability proof checker based on the new DRAT proof format. Unlike its predecessor, DRUP-trim, all presently known SAT solving and preprocessing techniques can be validated using DRAT-trim. Checking time of a proof is comparable to the running time of the corresponding solver. Memory usage is also similar to solving memory consumption, which overcomes a major hurdle of resolution-based proof checkers. The DRAT-trim tool can emit trimmed formulas, optimized proofs, and new TraceCheck$^+$ dependency graphs. We describe the output that is produced, what optimizations have been made to check RAT clauses, and potential applications of the tool.

ABSTRACT. We implement an online judge for evaluating correctness of reductions between NP-complete problems. The site has a list of exercises asking for a reduction between two given problems. Internally, the reduction is evaluated by means of a set of tests. Each test consists of an input of the first problem and gives rise to an input of the second problem through the reduction. The correctness of the reduction, that is, the preservation of the answer between both problems, is checked by applying additional reductions to SAT and using a state-of-the-art SAT solver. In order to represent the reductions, we have defined a new programming language called REDNP. On one side, REDNP has specific features for describing typical concepts that frequently appear in reductions, like graphs and clauses. On the other side, we impose severe limitations to REDNP in order to avoid malicious submissions, like the ones with an embedded SAT solver.

ABSTRACT. This paper presents Open-WBO, a new MaxSAT solver. Open-WBO has two main features. First, it is an open-source solver that can be easily modified and extended. Most MaxSAT solvers are not available in open-source, making it hard to extend and improve current MaxSAT algorithms. Second, Open-WBO may use any MiniSAT-like solver as the underlying SAT solver. As many other MaxSAT solvers, Open-WBO relies on successive calls to a SAT solver. Even though new techniques are proposed for SAT solvers every year, for many MaxSAT solvers it is hard to change the underlying SAT solver. With Open-WBO, advances in SAT technology will result in a free improvement in the performance of the solver. In addition, the paper uses Open-WBO to perform an evaluation on the impact of different SAT solvers in the performance of MaxSAT algorithms.