SAT 2014 LNCS PROCEEDINGS: PAPERS WITH ABSTRACTS

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. 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. 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. 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. 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. 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. 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. In 2010, Spence and Van Gelder presented a family of CNF formulas based on combinatorial block designs. They showed empirically that this construction yielded small instances that were orders of magnitude harder for state-of-the-art SAT solvers than other benchmarks of comparable size, but left open the problem of proving theoretical lower bounds. We establish that these formulas are exponentially hard for resolution and even for polynomial calculus, which extends resolution with algebraic reasoning. We also present updated experimental data showing that these formulas are indeed still hard for current CDCL solvers, provided that these solvers do not also reason in terms of cardinality constraints (in which case the formulas can become very easy). Somewhat intriguingly, however, the very hardest instances in practice seem to arise from so-called fixed bandwidth matrices, which are provably easy for resolution and are also simple in practice if the solver is given a hint about the right branching order to use. This would seem to suggest that CDCL with current heuristics does not always search efficiently for short resolution proofs, despite the theoretical results of [Pipatsrisawat and Darwiche 2011] and [Atserias, Fichte, and Thurley2011].

ABSTRACT. We investigate the proof complexity of a class of propositional formulas expressing a combinatorial principle known as the Kneser-Lovasz Theorem. This is a family of propositional tautologies, indexed by an nonnegative integer parameter k that generalizes the Pigeonhole Principle (PHP, obtained for k=1).

We show for all fixed $k$ $2^{\Omega(n)}$ lower bounds on resolution complexity and exponential lower bounds for bounded depth Frege proofs. These results hold even for the more restricted class of formulas encoding Schrijver's strengthening of the Kneser-Lovasz Theorem. On the other hand for the cases $k=2,3$ (for which combinatorial proofs of the Kneser-Lovasz Theorem are known) we give polynomial size Frege (k=2), respectively extended Frege (k=3) proofs. The paper concludes with a brief discussion of the results (that will be presented in a subsequent paper) on the complexity of the general case of the Kneser-Lovasz theorem.

ABSTRACT. Quantified Boolean formula (QBF) evaluation has a broad range of applications in computer science and is gaining increasing attention. Recent progress has shown that for a certain family of formulas Q-resolution, which forms the foundation of learning in modern search-based QBF solvers, is exponentially inferior in proof length to its extended variants: long-distance Q-resolution (LQ-resolution) and Q-resolution with resolution over universal literals (QU-resolution). The relative proof power between LQ-resolution and QU-resolution, however, remains unknown. In this paper, we show their incomparability by exponential separations on two families of QBFs, and further proposes a combination of the two resolution methods to achieve an even more powerful proof system. These results may shed light on solver development with enhanced learning mechanisms. In addition, we show how QBF Skolem/Herbrand certificate extraction can benefit from polynomial LQ-resolution proofs in contrast to their exponential Q-resolution counterparts.

ABSTRACT. Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanation for the hardness of instances in SAT solving. In this paper we aim at a unified view of a number of hardness measures, including different measures of width, space and size.

As our main contribution we obtain combinatorial characterisations of these hardness measures. Our characterisations are both in terms of Prover-Delayer games and of sets of partial assignments with some consistency strength. These unified characterisations allow elegant proofs of relations between the different hardness measures. In particular, we obtain a generalised version of Atserias and Dalmau's result on the relation between resolution width and space from (J. Comput. Syst. Sci. 2008). Our results do not only hold for unsatisfiable instances, but also transfer to the satisfiable case, for which little is known regarding hardness measures.

ABSTRACT. Portfolio approach for parallel SAT solvers is known as the standard parallelization technique. In portfolio, diversification is one of the important factors in order to enable workers (solvers) to conduct a vast search. The diversification is implemented by setting different parameters for each worker in the state-of-the-art parallel portfolio SAT solvers. However, existing diversification can be insufficient because the combination of the parameters is limited, in which two or more workers can search same spaces. For this issue, we propose a novel diversification technique, called community branching. In this method, we assign a different set (or sets) of variables (called a community) to each worker and force them to select these variables as decision variables in early decision levels. In this manner, we can avoid overlaps of search spaces between the workers more intentionally than the existing method. We create a graph, where a vertex is corresponds to a variable and an edge stands for relations in a same clause, and we apply a modularity-based community detection algorithm to it. The variables in a community have strong relationships, and a distributed search for different communities can benefit the whole search. Experimental results shot that we could speedup the existing parallel SAT solvers with our proposal.

ABSTRACT. (Tentative) In this paper, we present a simple parallel version of Glucose that uses a lazy policy to exchange clauses between cores. By working on the clause exchange policy, we ensure that in the context of many cores, the large number of incoming clauses will not degrade each core performances.

ABSTRACT. Incremental SAT solving under assumptions, introduced in Minisat, is in wide use. However, Minisat's algorithm for incremental SAT solving under assumptions has two main drawbacks which hinder performance considerably. First, it is not compliant with the highly effective and commonly used preprocessor SatELite. Second, all the assumptions are left in the formula, rather than being represented as unit clauses, propagated, and eliminated. Two previous attempts to overcome these problems solve either the first or the second of them, but not both. This paper remedies this situation by proposing a comprehensive solution for incremental SAT solving under assumptions, where SatELite is applied and all the assumptions are propagated. Our algorithm outperforms existing approaches over publicly available instances generated by a prominent industrial application in hardware validation.

ABSTRACT. In 1930s Paul Erdos conjectured that for any positive integer C in any infinite +1 -1 sequence (x_n) there exists a subsequence x_d, x_{2d}, ... , x_{kd} for some positive integers k and d, such that |x_d + x_{2d} + ... + x_{kd}|> C. The conjecture has been referred to as one of the major open problems in combinatorial number theory and discrepancy theory. For the particular case of C=1 a human proof of the conjecture exists; for C=2 a bespoke computer program had generated sequences of length 1124 having discrepancy 2, but the status of the conjecture remained open even for such a small bound. We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solvers, one can obtain a sequence of length 1160 with discrepancy 2 and a proof of the Erdos discrepancy conjecture for C=2, claiming that no sequence of length 1161 and discrepancy 2 exists. We also present our partial results for the case of C=3.

ABSTRACT. This paper presents an application of formal methods to the verification of power management modules in hardware designs. This paper identifies a distinct property of power management module and names it Dominant Controllability. This is a property of a netlist node and a subset of the inputs. The property holds if there exists an assignment to the subset of the inputs such that it sets the node to 0/1 regardless of the values of the rest of the inputs. Verification of power management modules in recent CPU and GPU designs includes hundreds of such properties. Dominant Controllability is different than controllability or random controllability which require only that the node is set to 0/1 by an assignment or random assignment to the inputs. The new application verifies Dominant Controllability using two formal methods: QBF-solver and netlist optimizer. Each method can be use independently or combined by a third algorithm that heuristically selects a method based on their performance in a specific design. The experimental results show that using QBF-solver is significantly faster when Dominant Controllability fails to hold (there is a bug in the design). Dominant Controllability fails when no assignment sets the node to 0/1, or when each such assignment is not dominant over other assignments to the rest of the inputs. In this case QBF-solver is faster because it concludes if Dominant Controllability fails without enumerating the large number of assignments. If the QBF-solver concludes that Dominant Controllability holds, netlist optimizer is used to verify the result, with a linear cost. Our experimental results show that even though using the netlist optimizer is incomplete, it is often successful when the power management module is very simple. The results also show that the third algorithm named Alternating selects the faster method successfully.

ABSTRACT. Dependency Quantified Boolean Formulas (DQBF) extend QBF with Henkin quantifiers, which allow for non-linear dependencies between the quantifiers. This extension is useful in verification problems for incomplete designs such as the partial equivalence checking problem (PEC), where a partial circuit, with some parts left open as ``black boxes'', is compared against a full circuit. The PEC problem is to decide whether the black boxes in the partial circuit can be filled in such a way that the two circuits become equivalent, while respecting that each black box only observes the subset of the signals that are designated as its input. We present a new algorithm that efficiently refutes unsatisfiable DQBF formulas. The algorithm detects situations in which already a subset of the possible assignments of the universally quantified variables suffices to rule out a satisfying assignment of the existentially quantified variables. Our experimental evaluation on PEC benchmarks shows that the new algorithm is a significant improvement both over approximative QBF-based methods, where our results are much more accurate, and over precise methods based on variable elimination, where the new algorithm scales much better in the number of Henkin quantifiers.

ABSTRACT. Modern CDCL SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. It is clear that these solvers somehow exploit the structure of real-world instances. How- ever, to-date there have been few results that precisely characterise this structure. In this paper, we provide evidence that the community structure of real-world SAT instances is correlated with the running time of CDCL SAT solvers. It has been known for some time that real-world SAT instances, viewed as graphs, have natural communities in them. A community is a sub-graph of the graph of a SAT instance, such that this sub-graph has more internal edges than outgoing to the rest of the graph. The community structure of a graph is often characterised by a quality metric called Q. Intuitively, a graph with high-quality community structure (high Q) is easily separable into smaller communities, while the one with low Q is not. We provide three results based on empirical data which show that community structure of real-world industrial instances is a better predictor of the running time of CDCL solvers than other commonly considered factors such as variables and clauses. First, we show that there is a strong correlation between the Q value and Literal Block Distance metric of quality of conflict clauses used in clause-deletion policies in Glucose-like solvers. Second, using regression analysis, we show that the the number of communities and the Q value of the graph of real-world SAT instances is more predictive of the running time of CDCL solvers than traditional metrics like number of variables or clauses. Finally, we show that randomly-generated SAT instances with 0.05 ≤ Q ≤ 0.13 are dramatically harder to solve for CDCL solvers than otherwise.

ABSTRACT. We propose Q(D)-resolution, a proof system for Quantified Boolean Formulas. Q(D)-resolution is a generalization of Q-resolution parameterized by a dependency scheme D. This system is motivated by the generalization of the QDPLL algorithm using dependency schemes implemented in the solver DepQBF. We prove soundness of Q(D)-resolution for a dependency scheme D that is strictly more general than the standard dependency scheme; the latter is currently used by DepQBF. This result is obtained by proving correctness of an algorithm that transforms Q(D)-resolution refutations into Q-resolution refutations and could be of independent practical interest. We also give an alternative characterization of resolution-path dependencies in terms of directed walks in a formula's implication graph which admits an algorithmically more advantageous treatment.

ABSTRACT. We present novel approaches to detect cardinality constraints expressed in CNF. The first approach is based on a syntactic analysis of specific data structures used to represent binary and ternary clauses, whereas the second approach is based on a semantic analysis by unit propagation.

The syntactic approach computes an approximation of the cardinality constraints AtMost-$1$ and AtMost-$2$ constraints very fast, whereas the semantic approach has the property to be generic, i.e. it can detect cardinality constraints AtMost-$k$ for any $k$, at a higher computation cost.

Our experimental results suggest that the syntactic approach is efficient at recovering AtMost-$1$ and that the semantic one is efficient at recovering AtMost-$2$ cardinality constraints.

ABSTRACT. Stochastic Local Search (SLS) is considered to be one of the best solving technique for randomly generated problems and more recently also has shown great promise for several types of hard combinatorial problems. Within this work, we provide a thorough analysis of different implementation variants of SLS solvers on random and on hard combinatorial problems. By analyzing existing SLS implementations, we are able to discover new improvements inspired by CDCL solvers, which can speed up the search of all types of SLS solvers. Further, our analysis reveals that multilevel break values of variables can be easily computed and used within the decision heuristic. By augmenting the probSAT solver with the new heuristic, we are able to reach new state-of-the-art performance on several types of SAT problems, especially on those with long clauses. We further provide a detailed analysis of the clause selection policy used in focused search SLS solvers.

ABSTRACT. Blocked clause elimination is a powerful technique in SAT solving. In recent work, it has been shown that it is possible to decompose any propositional formula into two subsets (blocked sets) such that both can be solved by blocked clause elimination. We extend this work in several ways. First, we prove new theoretical properties of blocked sets. We then present additional and improved ways to efficiently solve blocked sets. Further, we propose novel decomposition algorithms for faster decomposition or which produce blocked sets with desirable attributes. We use decompositions to reencode CNF formulas and to obtain circuits, such as AIGs, which can then be simplified by algorithms from circuit synthesis and encoded back to CNF. Our experiments demonstrate that these techniques can increase the performance of the SAT solver Lingeling on hard to solve application benchmarks.

ABSTRACT. In this paper we present new methods for deciding the satisfiability of formulas involving integer polynomial constraints. In previous work we proposed to solve SMT(NIA) problems by reducing them to SMT(LIA): non-linear monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. When variables do not have finite domains, artificial ones can be introduced by imposing a lower and an upper bound, and made iteratively larger until a solution is found (or the procedure times out). For the approach to be practical, unsatisfiable cores are used to guide which domains have to be relaxed (i.e., enlarged) from one iteration to the following one. However, it is not clear then how large they have to be made, which is critical.

Here we propose to guide the domain relaxation step by analyzing minimal models produced by the SMT(LIA) solver. Namely, we consider two different cost functions: the number of violated artificial domain bounds, and the distance with respect to the artificial domains. We compare these approaches with other techniques on benchmarks coming from constraint-based program analysis and show the potential of the method. Finally, we describe how one of these minimal-model-guided techniques can be smoothly adapted to deal with the extension Max-SMT of SMT(NIA) and then applied to program termination proving.

ABSTRACT. We present an encoding of pseudo-Boolean constraints based on decomposition with respect to a residual number system. We illustrate that careful selection of the base for the residual number system, and when bit-blasting modulo arithmetic, results in a powerful approach when solving hard pseudo-Boolean constraints. We demonstrate, using a range of pseudo-Boolean constraint solvers, that the obtained constraints are often substantially easier to solve.

ABSTRACT. Message Passing (MP) has been presented in a unified and consistent notational frame in \cite{gableske}. The paper explained the product-based MP framework (PMPF) and various MP heuristics (BP, SP, and several interpolations). The paper concluded, that an increased flexibility of MP heuristics (in the form of tuneable parameters) leads to a tuneable MP algorithm that can be helpful to solve a wide variety of different CNFs. Based on this work, the paper at hand makes three contributions. First, we extend the PMPF regarding flexibility based on theoretical insights from the Ising Model \cite{ising}. As an immediate result, this extended PMPF (ePMPF) provides new possibilities for parameter tuning. Second, the ePMPF will also allow us to uncover various theoretical connections between well-known variable and value ordering heuristics for SAT (Zero-first, One-first, occurrence-based heuristics). We show, that these heuristics can be understood as special cases of Message Passing. Third, we show that the ePMPF provides numerous possibilities to tightly integrate Message Passing with various aspects of the CDCL search paradigm.

ABSTRACT. In this paper we introduce two distributions for the Max-2-SAT problem similar to the uniform distributions of satisfiable CNFs and the planted distribution for the decision version of SAT. In both cases there is a parameter p, 0<= p<= 1/4d, where d is the clause-to-variable ratio (density) of the formula, such that formulas chosen according to both distributions are p-satisfiable, that is, at least (3/4d+p)n clauses can be satisfied. In the planted distribution this happens for a fixed assignment, while for the p-satisfiable distribution formulas are chosen uniformly from the set of all p-satisfiable formulas.

Following Coja-Oghlan, Krivelevich, and Vilenchik (2007) we establish a connection between the probabilities of events under the two distributions. Then we consider the case when p is sufficiently large, p=r\sqrt{d\log d} and r>3/2. We present an algorithm that in the case of the planted distribution for any e>0 with high probability finds an assignment satisfying at least (3/4d+p-e)n clauses. For the p-satisfiable distribution for every d there is e(d) (which is a polynomial in d of degree depending on r) such that the algorithm with high probability finds an assignment satisfying at least (3/4d+p-e(d))n clauses. It does not seem this algorithm can be converted into an expected polynomial time algorithm finding a p-satisfying assignment.

Also we use the connection between the planted and uniform p-satisfiable distributions to evaluate the number of clauses satisfiable in a random (not p-satisfiable) 2-CNF. We find the expectation of this number, but do not improve the existing concentration results.

ABSTRACT. We show that the propositional model counting problem #SAT for CNF- formulas with hypergraphs that allow a disjoint branches decomposition can be solved in polynomial time. We show that this class of hypergraphs is incomparable to hypergraphs of bounded incidence cliquewidth which were the biggest class of hypergraphs for which #SAT was known to be solvable in polynomial time so far. Furthermore, we present a polynomial time algorithm that computes a disjoint branches decomposition of a given hypergraph if it exists and rejects otherwise. Finally, we show that some slight extensions of the class of hypergraphs with disjoint branches decompositions lead to intractable #SAT, leaving open how to generalize the counting result of this paper.

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. 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. 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. 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.