ABSTRACT. Recently Dependency Quantified Boolean Formula (DQBF) has attracted a lot of attention in the SAT community. Intuitively, a DQBF is a natural extension of quantified boolean formula where for each existentially quantified variable, one can specify its set of dependent variables. However, beside the fact that the satisfiability problem is NEXP-complete, not much is known about DQBF.

In this paper we show that surprisingly there is a strong resemblance between DQBF and CNF boolean formulas. More precisely, we show that a DQBF is just a succinctly represented CNF boolean formula in which the information about each clause is encoded inside the matrix of the DQBF and that the number of existentially quantified variables in a DQBF corresponds precisely to the width of the clauses in the CNF formula. Thus, solving DQBF instances is essentially solving SAT instances in CNF. We then present a thorough study on DQBF and show that indeed many classical results on SAT can be lifted up to DQBF, only with exponential blow-up in complexity.

ABSTRACT. MaxSAT is the problem of finding an assignment satisfying the maximum number of clauses in a CNF formula. We consider a natural generalization of this problem to generic sets of polynomials and propose a weighted version of Polynomial Calculus to address this problem. Weighted Polynomial Calculus is a a natural generalization of MaxSAT-Resolution and weighted Resolution that manipulates polynomials with coefficients in a finite field and either weights in N or Z. We show the soundness and completeness of these systems via an algorithmic procedure. Weighted Polynomial Calculus, with weights in N and polymomials with coefficients in F_2, is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in Z, it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.

ABSTRACT. The width complexity measure plays a central role in Resolution and other propositional proof systems like Polynomial Calculus (under the name of degree). The study of width lower bounds is the most extended method for proving size lower bounds, and it is known that for these systems, proofs with small width also imply the existence of proofs with small size. Not much has been studied, however, about the width parameter in the Cutting Planes (CP) proof system, a measure that was introduced by Dantchev and Martin in 2011 under the name of CP cutwidth.

In this paper, we study the width complexity of CP refutations of graph isomorphism formulas. For a pair of non-isomorphic graphs $G$ and $H$, we show a direct connection between the Weisfeiler-Leman differentiation number $\mathsf{WL}(G, H)$ of the graphs and the width of a CP refutation for the corresponding isomorphism formula $\mathrm{Iso}(G, H)$. In particular, we show that if $\mathsf{WL}(G, H) \leq k$, then there is a CP refutation of $\mathrm{Iso}(G, H)$ with width $k$, and if $\mathsf{WL}(G, H) > k$, then there are no CP refutations of $\mathrm{Iso}(G, H)$ with width $k-2$. Similar results are known for other proof systems, like Resolution, Sherali–Adams, or Polynomial Calculus. We also obtain polynomial-size CP refutations from our width bound for isomorphism formulas for graphs with constant WL-dimension.

ABSTRACT. We introduce a new release of our SAT solver Intel(R) SAT Solver. The new release, called IS23, is targeted to solve huge instances beyond the capacity of other solvers. IS23 can use 64-bit clause-indices and store clauses compressedly using bit-arrays, where each literal is normally allocated fewer than 32 bits. As a preliminary result, we show that only IS23 can handle a gigantic trivially satisfiable instance with over 8.5 billion clauses. Then, we demonstrate that IS23 enables a significant improvement in the capacity of our industrial tool for cell placement in physical design, since only IS23 can solve placement instances with up to 4.3 billion clauses. Finally, we show that IS23 is substantially more efficient than other solvers for finding many (10^6) placements on instances with up to 170 million clauses. We use the latter application to demonstrate that variable succession, that is, the order in which the variables are provided to the solver, might have a significant impact on IS23's performance, thereby providing a new dimension to SAT encoding considerations.

ABSTRACT. DRAT is the standard proof format used in the SAT Competition. It is easy to generate but checking proofs often takes even more time than solving the problem. An alternative is to use the LRAT proof system. While LRAT is easier and way more efficient to check, it is more complex to generate directly. Due to this complexity LRAT is not supported natively by any state-of-the-art SAT solver. Therefore Carneiro and Heule proposed the mixed proof format FRAT which still suffers from costly intermediate translation though. We present an extension to the state-of-the-art solver CaDiCaL which is able to generate LRAT natively for all procedures implemented in CaDiCaL. We further present Lrat-Trim, a tool which not only trims and checks LRAT proofs in both ASCII and binary format but also produces clausal cores and has been tested thoroughly. Our experiments on recent competition benchmarks show that our approach reduces time of proof generation and certification substantially compared to competing approaches using intermediate DRAT or FRAT proofs.

ABSTRACT. The backbone of a satisfiable formula is the set of literals that are always true in all its satisfying assignments. Computing the backbone efficiently is able to improve a wide range of SAT-based applications, such as verification, fault localization and product configuration. In this tool paper, we introduce a new backbone extraction tool called CadiBack. It takes advantage of unique features available in our state-of-the-art SAT solver CaDiCaL including transparent inprocessing and using single clause assumption, which have not been evaluated in this context before. In addition, CaDiCaL is enhanced with an improved algorithm to support model rotation by utilizing watched literal data structures. In our comprehensive experiments with a large number of benchmarks, CadiBack solves 60% more instances than the state-of-the-art backbone extraction tool MiniBones. Our tool is publicly available as open source, well documented and easy to extend as well as thoroughly tested through fuzzing, internal correctness checking and cross checking on a large benchmark set.

ABSTRACT. Modern SAT solvers are frequently embedded as sub-reasoning engines into more complex tools for addressing problems beyond the Boolean satisfiability problem. Examples include solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration and counting. In such use cases, the SAT solver is often able to provide relevant information beyond the satisfiability answer. Further, domain knowledge of the embedding system (e.g., symmetry properties or theory axioms) can be beneficial for the CDCL search, but cannot be efficiently represented in clausal form.

In this paper, we propose a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. Our goal is to capture the most essential functionalities that are sufficient to simplify and improve use cases that require a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, we extend CaDiCaL with our interface and evaluate it on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL(T) SAT engine of the SMT solver cvc5.