Schedule for: 18w5208 - Theory and Practice of Satisfiability Solving

In this talk, we will present the basic principles of SAT solvers, by focusing on the essential ingredients most of the best SAT solvers embed. The practical applications of SAT solvers have attracted a lot of attention in the recent years, which is probably due to their ability to solve problems encoded in SAT more efficiently than adhoc methods. However, on these problems (where SAT solvers show very good results) the reasons for their efficiency remains largely unknown. We will thus also present a few experimental observations we gathered over the years. This should cast some lights on some of their mode of operation, sometimes counter intuitively, and stimulate further discussions.

Running a SAT solver on an UNSAT formula produces (implicitly or explicitly) a proof that the formula is unsatisfiable, usually expressible in an established formal language called proof system. This observation leads to study SAT solving methods by looking at the generated proofs. I.e., if an UNSAT formula has no short proof in a given proof system, the corresponding SAT solvers cannot solve the formula efficiently.

We introduce the area and the methods of proof complexity, that studies the length and the structure of proofs of UNSAT. In particular we define and discuss Resolution, Polynomial Calculus, Cutting Planes and Extended Resolution, which are the most relevant proof systems for current SAT solver technology.

Since a SAT solver goal is, among other things, to look for proofs as short as possible, we briefly discuss the complexity of efficiently finding such short proofs.

The success of satisfiability solving presents us with an interesting peculiarity: modern solvers can frequently handle gigantic formulas while failing miserably on supposedly easy problems. Their poor performance is typically caused by the weakness of their underlying proof system—resolution. To overcome this obstacle, we need solvers that are based on stronger proof systems. Unfortunately, existing strong proof systems—such as extended resolution or Frege systems—do not seem to lend themselves to mechanization.

We present a new proof system that not only generalizes strong existing proof systems but that is also well-suited for mechanization. The proof system is surprisingly strong, even without the introduction of new variables—a key feature of short proofs presented in the proof-complexity literature. We demonstrate the strength of the new proof system on the famous pigeon hole formulas by providing short proofs without new variables. Moreover, we introduce satisfaction-driven clause learning, a new decision procedure that exploits the strengths of our new proof system and can therefore yield exponential speed-ups compared to state-of-the-art solvers based on resolution.

Many a mathematical proof presents a symmetry argument to bypass an otherwise cumbersome case distinction. Similarly, combinatorial solvers can exploit symmetry to reduce the search space. This talk gives an overview of the techniques used in SAT solving to exploit symmetry properties of the problem at hand.

It covers the topics of symmetry detection - typically via a transformation to graph automorphism though an argument for other approaches can be made; types of symmetry - different types have different needs; static and dynamic symmetry breaking - which remove symmetrical solutions from the solution set; symmetrical learning - which adds a symmetry rule to CDCL's proof system; and completeness of symmetry exploitation techniques - which arguably is the ultimate goal. The talk elaborates on the strengths and weaknesses of each technique, highlighting open questions and future research opportunities.

As a common thread, we discuss the performance of each technique on the SAT encoding of the pigeonhole principle, which -in theory- can be decided in polynomial time using a symmetry argument. In practice however, efficiently deciding the SAT encoding of the pigeonhole principle remains a daunting challenge, as even after decades of research, none of the current techniques is able to fully detect and exploit the available symmetry.

Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive.

In this work we try to shed light on CDCL performance by using theoretical benchmarks. While these are crafted instances, they have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically *easy* in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how successfully they implement efficient proof search.

We report results from extensive experiments with different CDCL parameter configurations on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raises a number of intriguing questions for further study.

This is a presentation of a paper that is published at IJCAI '18.

Finding a maximum clique in a graph is one of the most basic computational problems on graphs. The various applications of this problem has motivated the design of algorithms which today can successfully solve real-world instances with thousands of vertices. However, from a theoretical point a view, it is widely believed that this is a hard problem: in particular that determining whether a graph on n vertices contains a k-clique requires time $n^{\Omega(k)}$. In terms of upper bounds, it is easy to determine this in time roughly $n^k$ by checking if any of the sets of vertices of size k forms a clique.

We analyse the running time of the most successful algorithms used in practice: colour-based branch-and-bound strategies and Östergård's algorithm based on Russian doll search. When analysing such algorithms, it is convenient to view the execution trace as a proof establishing the maximal clique size for the input graph. In particular, if this graph does not have a k-clique, then the trace provides an efficiently verifiable proof in so-called regular resolution of the statement that the graph is k-clique-free. We show that for any $k \ll n^{1/4}$ if the input graph is a k-clique-free random graph sampled from the right distribution then the size of such regular resolution proofs, and hence the running time of these algorithm, is at least $n^{\Omega(k)}$.

Since 2014, several leading theoreticians and experimentalists conducting research on Boolean satisfiability (SAT) solving have been meeting annually to stimulate an increased exchange of ideas between these two communities. The hope has been for for a fruitful interplay between theoretical and experimental research in this area, with the belief that a more vigorous interaction between the two has potential for major long-term impact in computer science and mathematics, as well for applications in industry.

in this fifth meeting of this group, it is appropriate to ask how successful has the interplay between theoretical and experimental research in SAT solving. In this brief talk, I will outline some areas of real progress. At the same, I will argue that progress has been rather mild relative to expectations, and suggest some concrete research directions that could be pursued to advance the theory and engineering of SAT solving.

The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean satisfiability---so-called SAT solvers---and today conflict-driven clause learning (CDCL) solvers are routinely used in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak. A tantalizing solution is to instead use stronger pseudo-Boolean (PB) reasoning (a.k.a. 0-1 integer linear programming), but so far the promise of exponential gains in performance has mostly failed to materialize---the increased theoretical strength seems hard to harness algorithmically, and in many applications CDCL-based methods are still superior.

In this talk, we will discuss conflict-driven search and how to lift it from clauses to pseudo-Boolean linear constraints. We will survey the "classic" method in [Chai and Kuehlmann '05] based on saturation, and then describe a relatively new approach from [Elffers and Nordström '18] instead using division. We will also try to highlight some of the obstacles that remain along the path to truly efficient pseudo-Boolean solvers.

MaxSat is an optimization version of SAT. In particular, the clauses of a CNF are divided into hard and soft clauses where each soft clause has a finite and positive weight. MaxSat is the problem of finding a truth assignment that satisfies a maximum weight of soft clauses while also satisfying all of the hard clauses.

In this talk I will discuss the two most successful approaches to solving MaxSat: using SAT to solve a sequence of SAT formulas derived from the original MaxSat formula and the implicit hitting set approach which uses both SAT and Integer Programming solvers in a hybrid approach. Both approaches utilize the notion of cores which are subsets of soft clauses that are unsat when conjoined with the hard clauses. In the sequence of SAT approaches, discovered cores are used to reformulate the SAT formula that admits models falsifying more soft clauses of the original MaxSat formula. In the most successful of such methods extra variables are introduced into the formula and these play an essential role in the efficiency of the method. In the implicit hitting set approach, in contrast, the original MaxSat formula is unchanged. Instead cores are extracted from it, and hitting sets of the set of extracted cores are computed using integer programming solving. We will contrast the relative strengths of these two approaches, and try to draw some insights into what their relative successes say about the underlying problem. We will also attempt to highlight some further theoretical questions arising from these approaches.

This talk provides a survey of SMT solving with an emphasis on recent developments and directions.

• Integrating Theory Solvers.
  Fundamental to SMT is a method for integrating theory reasoners. The basic approach, based on the Nelson-Oppen combination, has been the backbone of mainstream SMT solvers. It works for signature disjoint theories and an important research direction has been how to tune it, notably for non-convex theories. Integrating theories with shared signatues (such as the theory of lists with a length function) has also received attention, but is not integral to mainstream SMT solvers, yet. The talk will revisit a few of these methods.
• Linear arithmetic and beyond.
  A significant set of SMT use cases require some reasoning about arithmetic. We summarize some highlights in their approaches to solving classes of arithmetical formulas, including linear real, integer, linear real with ReLu, polynomial real, and with recent advances in handling non-linear integer, polynomial GF, and transcendental functions.
• Strings and sequences.
  An active area in the SMT community is in formulating formats for string constraint solving. Several solvers have emerged in the past few years. We touch on the basics of sequence solving from the vantage point of the SMT and logic communities.
• Constrained Horn Clauses (CHC)
  We illustrate how symbolic model checking over push-down systems can be directly reduced to checking satisfiability of constrained Horn clauses, that can be expressed as SMT formulas. Several new approaches for solving CHCs are currently being developed by different groups.

We will give a general introduction into the algorithms and techniques implemented and successfully used in mixed-integer programming solvers and try to point out connections to satisfiability solving. One prime example are interactions between classical diving heuristics and conflict analysis. Diving heuristics exhibit the property that they either succeed in producing a feasible primal solution or return a dual certificate of infeasibility subject to the variable fixings. Although aimed at success, the failure certificates can be analyzed to extract globally valid inequalities that help to reduce the size of the remaining search tree in a very similar fashion as in (UN)SAT solvers.

Inspired by the success of CDCL SAT solvers, recent years have witnessed remarkable progress in Maximum Satisfiability (MaxSAT) solving. Modern MaxSAT engines implement different approaches for exploiting SAT solvers as oracles for NP. Concrete examples include core-guided MaxSAT, but also MaxSAT using Minimum Hitting Sets (MHSes). Recent work has shown that, with a so-called dual rail problem transformation, encodings of the PHP principle can be solved in polynomial time with different MaxSAT solvers. Based on this dual rail encoding and MaxSAT solving, more recent work devised proof systems that were shown to p-simulate Resolution. This talk provides an overview of some of the above results, but also surveys the original practical motivation for developing proof systems exploiting the dual rail encoding and MaxSAT. Finally, the talk summarizes ongoing research directions.

Understanding properties of deep neural networks is an important challenge in deep learning. Deep learning networks are among the most successful artificial intelligence technologies that is making impact in a variety of practical applications. However, many concerns were raised about `magical' power of these networks. It is disturbing that we are really lacking of understanding of the decision making process behind this technology. Therefore, a natural question is whether we can trust decisions that neural networks make. One way to address this issue is to define properties that we want a neural network to satisfy. Verifying whether a neural network fulfills these properties sheds light on the properties of the function that it represents. In this work, we take the verification approach. Our goal is to design a framework for analysis of properties of neural networks. We start by defining a set of interesting properties to analyze. Then we focus on Binarized Neural Networks that can be represented and analyzed using well-developed means of Boolean Satisfiability and Integer Linear Programming. One of our main results is an exact representation of a binarized neural network as a Boolean formula. We also discuss how we can take advantage of the structure of neural networks in the search procedure.

Very often, problems modeled using pseudo-Boolean constraints are optimization problems, not satisfaction problems. Because of the very efficient SAT solvers available, many of those optimization problems can be solved by reusing those solvers as black boxes. In this talk, we will provide some insights about the reason of the success of the black box approaches, some of their limitations, and raise open problems to design more efficient Boolean optimizers.

Pseudo-Boolean solvers that generalize the CDCL algorithm and reason within the cutting planes proof system can have a theoretical advantage with respect to solvers that just translate the problem and apply the standard CDCL algorithm, which is limited to resolution. In practice, however, results are mixed. Do we need a better theory, better solvers, or both?

One key observation is that implementation constraints limit solvers to a subset of inference rules. In this talk we identify subsystems of cutting planes that arise from these limited rules and we classify them, showing in particular that pseudo-Boolean solvers are limited to resolution if their input is encoded adversarially.

Guided by these theoretical insights we craft formulas that lie within the limits of pseudo-Boolean solvers and test them in practice. Alas, current solvers perform terribly on these benchmarks, but we can at least extract concrete obstacles for upcoming solvers to overcome.

Joint work with Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, and Jakob Nordström.

There is an increasing interplay between practical implementations of Sat Solvers and theoretical results about proof complexity. In some cases, theory can be useful for understanding or designing Sat solvers, but the connections are not as strong as might be wished for. This talk will discuss these issues, and make some suggestions for further research directions both for theoreticians and for practitioners.

Practical research on Satisfiability Solving requires tools. This session is dedicated to present the tools used by the participants (solvers, benchmarks generators, frameworks, visualization of experimental results, etc) and discuss the good practices of empirical evaluation in Satisfiability Solving. Programme - PySAT: Joao Marques Silva - Testing and debugging solvers: Mathias Preiner - CDCL insights from theory benchmarks website: Stephan Gocht - Presentation of MIPLIB: Ambros Gleixner

In this talk I will review the recent progress in the solving of Quantified Boolean Formulas (QBF). The initial research on QBF solving focused on extending SAT technology. However, in the recent approaches SAT solvers are used in a black-box fashion and the search space is pruned by stronger constraints than just clauses. The study of QBF has also revealed a number of limitations of the existing technology. Recent results show that some of these limitations can be tackled by applying Machine Learning at the semantic level.

This talk will give an overview of the relatively young field of QBF proof complexity, explaining QBF proof systems (including QBF resolution, Frege and beyond). We will explore the simulation order of different QBF calculi and how they correspond to ideas in QBF solving.

A particular focus of the talk will be on lower bound techniques for QBF systems and in particular new ideas, which do not just lift propositional hardness, but exploit hardness stemming from quantifier dependencies.

In this talk I will both give a review of the behaviour of random k-sat formulae and present some new variations on the problem. In the study of random K-sat one constructs a k-sat formula with n variables and m clauses at random. When m is small the formula is most often satisfiable and when m i large it is most likely unsatisfiable. We also know that there is a sharp transition between these to cases, often referred to as a phase transition. Empirically is has been observed that sat-solvers have a peak in their typically running time when m is close to this phase transition, and a longer number of conjectures has been made about this behaviour.

I will review what is now known from mathematical results and also discuss how well, or badly, some of the old conjectures and observations have held up against both mathematics and recent, far more extensive, experiments. I will also mention some recent work on unbalanced versions of k-sat which display interesting behaviours.

At a Dagstuhl meeting a few years ago, I gave a tutorial lecture about Groebner bases whose emphasis was on their defining properties and the classical algorithms for computing them. In this year's tutorial, I will focus more on what we can do with Groebner bases and polynomial ideal theory. The plan is to cover some of the standard situations in which Groebner bases are helpful, as well as some recent joint work with Armin Biere and Daniela Ritirc on using Groebner bases for circuit verification.

Combinatorial problems can be represented elegantly and efficiently by systems of polynomial equations. Those systems are either feasible or infeasible, depending on whether or not the underlying combinatorial property is present or not present. In this general survey talk, we will explore the infeasible polynomial systems and their associated combinatorial Nullstellensatz certificates, and we will also explore the feasible polynomial systems and their associated Grobner bases. Along the way, we will highlight some natural questions that arise and identify specific advantages/disadvantages of these methods. We will also suggest open problems and further research directions whenever possible.

I will survey work on exact algorithms for SAT, analyzed by their worst-case complexity. I will mention some of the algorithmic paradigms and methods of analysis used, and propose several directions for further research.

Aerospace operational concepts are often specified with timelines; we find the Boolean variables and propositional clauses of traditional propositional SAT laid out over time. Therefore, we capture these industrial requirements in Linear Temporal Logic; we must efficiently check LTL satisfiability in order to assure correctness of these requirements before we use them for further analysis, such as model checking or runtime monitoring. When sets of requirements are not satisfiable, the natural question from the system designers is: how many of these features can I have? This is the MAX-SAT question for LTL and it is an open challenge!

Once a system is verified in design time, built, and deployed, we need runtime verification over the current mission execution to ensure it adheres to the set of requirements during operation. We often specify such runtime requirements in Mission-time Linear Temporal Logic (MLTL), which adds bounds to the temporal operators of LTL and changes the shape of the satisfiability and MAX-SAT problems. We highlight promising directions for the satisfiability and MAX-SAT questions for temporal logics via decompositions that utilize Boolean SAT solvers.

Program synthesis is expanding rapidly and getting a lot of attention from both industry and academia. The goal of program synthesis is to find a program that satisfies the user intent expressed in the form of some specification. Program synthesis has proven to be useful to both end-users and programmers. For instance, program synthesis has been used to automate tedious tasks that arise in everyday life, such as string manipulations in spreadsheets or data wrangling tasks in R. Program synthesis has also been used for improving programmer productivity by automatically completing parts of a program or helping programmers use complex APIs.

In this talk, I will present a new conflict-driven program synthesis framework that is capable of learning from past mistakes. Given a program that violates the desired specification, our synthesis algorithm identifies the root cause of the conflict and learns new lemmas that can prevent similar mistakes in the future. We have implemented a general purpose CDCL-style program synthesizer called Neo and evaluate it in two different application domains, namely data wrangling in R and functional programming over lists. Our experiments demonstrate an order of magnitude improvement when using conflict-driven learning and opens a new research direction that can push the boundaries of program synthesis.

One of the oldest and weakest calculi for quantified Boolean formulas (QBF) is Q-Resolution. It consists of two rules: the resolution rule similar as in propositional logic and the universal reduction rule. In its most basic variant, resolution is allowed only over existential variables. More powerful proof systems can be obtained by allowing resolution over the universal variables as well or by introducing so-called long-distance resolution. Separations are shown by using the well-investigated formulas introduced by Kleine Buening and other (the so-called KBKF formulas).

In this talk, we enrich the (relatively weak) QBF resolution calculus with the Symmetry Rule that exploits symmetries of the input formula. With this simple rule, we obtain separations to powerful QBF calculi by showing that the KBKF formulas and extensions become easy when the symmetry rule may be used.

The resolution proof system has been enormously helpful in deepening our understanding of conflict-driven clause-learning (CDCL) SAT solvers. In the interest of providing a similar proof complexity-theoretic analysis of satisfiability modulo theories (SMT) solvers, we introduce a generalization of resolution called Res(T). We show that many of the known results comparing resolution and CDCL solvers lift to the SMT setting, such as the result of Pipatsrisawat and Darwiche showing that CDCL solvers with ``perfect'' non-deterministic branching and an asserting clause-learning scheme can polynomially simulate general resolution. We also describe a stronger version of Res(T), Res*(T), capturing SMT solvers allowing introduction of new literals.

We analyze the theory EUF of equality with uninterpreted functions, and show that the Res*(EUF) system is able to simulate an earlier calculus introduced by Bjorner and De Moura for the purpose of analyzing DPLL(EUF). Further, we show that Res*(EUF) (and thus SMT algorithms with clause learning over EUF, new literal introduction rules and perfect branching) can simulate the Frege proof system, which is well-known to be far more powerful than resolution. Finally, we prove under the Exponential Time Hypothesis (ETH) that any reduction from EUF to SAT (such as the Ackermann reduction) must, in the worst case, produce an instance of size at least n log n from an instance of size n.

It has been well-established that CDCL SAT solvers with restarts can simulate general resolution. However, these results require that the solver use a highly nondeterministic or sufficiently random decision strategy. Our goal is to understand the impact of more explicit decision strategies on the theoretical strength of CDCL. Since decisions strategies used in practice are somewhat complicated, we instead focus on the simpler ordered decision strategy: when the solver has to choose a variable to assign, it must choose the smallest unassigned variable according to some underlying order. This strategy was studied by Beame et. al. (2002) in the context of DLL without clause learning. It is still possible for unit propagation to assign variables out of order, which is what makes this situation more subtle and non-trivial.

Our motivating question is the following: is there a family of unsatisfiable formulas that possess polynomial size resolution refutations but require super-polynomial time for CDCL using the ordered decision strategy? We present preliminary results towards this end. First, we show that CDCL with the ordered decision strategy and the so-called DECISION learning scheme is no more powerful than ordered resolution. Second, we show that CDCL with the ordered decision strategy and a somewhat powerful learning scheme we call FIRST-L (similar to FirstNewCut introduced by Beame et. al. (2004)) is equivalent to general resolution, given it can ignore unit clauses and conflicts. This result may be interpreted as demonstrating that mandatory unit propagation or conflict analysis is, in some sense, necessary to positively answer our the question above.

To aid this work, we also present a model and language for discussing CDCL-based proof systems. This is not meant to be novel and is heavily influenced by previous works. But rather than being faithful to practical SAT-solver implementations, the goal of our model is highlighting possible non-standard sources of nondeterminism. It allows for clear and concise mathematical statements about CDCL-based proof systems and better represents the landscape of potential CDCL variants.

Conflict-driven clause learning (CDCL) is at the core of the success of modern SAT solvers. In terms of propositional proof complexity, CDCL has been shown as strong as general resolution. Improvements to SAT solvers can be realized either by improving existing algorithms, or by exploiting proof systems stronger than CDCL. Recent work proposed an approach for solving SAT by reduction to dual-rail MaxSAT. The proposed reduction coupled with MaxSAT resolution represents a new proof system, DRMaxSAT, which was shown to enable polynomial time refutations of pigeonhole formulas, in contrast with either CDCL or general resolution. This paper investigates the DRMaxSAT proof system, and shows that DRMaxSAT p-simulates general resolution, that $AC_0$- Frege+PHP p-simulates DRMaxSAT, and that DRMaxSAT can not p-simulate neither $AC_0$-Frege+PHP nor the cutting planes proof system.

Boolean satisfiability is a fundamental problem in computer science with a wide range of applications including planning, configuration management, and design and verification of software and hardware systems. The annual SAT competition continues to witness impressive improvements in the performance of the winning SAT solvers largely thanks to the development of new heuristics arising out of intensive collaborative research in the SAT community. The modern SAT solvers achieve scalability and robustness with complex heuristics that are challenging to understand and explain. Consequently, the development of new algorithmic insights has been largely restricted to "expert intuitions" and evaluation of the new insights have been restricted to performance measurement in terms of the runtime of solvers or a proxy for the runtime of solvers. In this context, one may ask: whether it is possible to develop a framework to provide white-box access to the execution of SAT solver, which can aid the end user (i.e., a SAT solver developer) to synthesize algorithmic heuristics for modern SAT solvers?

The primary focus of our project is precisely such a framework, which we call CrystalBall. More precisely, we propose to view modern CDCL solvers as a composition of prediction engines for different tasks such as branching, clause memory management, and restarts. In this talk, I will introduce CrystalBall and some promising preliminary results that we have obtained.

(Joint work with Mate Soos and Raghav Kulkarni)

Many applications in hardware and software verification rely on Satisfiability Modulo Theories (SMT) solvers for bit-precise reasoning. For solving quantifier-free bit-vector formulas, current state-of-the-art is a technique called bit-blasting, which eagerly translates a given formula into propositional logic (SAT). Bit-blasting is efficient in practice, but may not scale if the input size can not be reduced sufficiently during preprocessing. For quantified bit-vector logics, the majority of solvers employ instantiation-based techniques, which aim to find conflicting ground instances of quantified formulas. For that, it is crucial to select good instantiations for the universal variables, or else the solver may be overwhelmed by the number of ground instances generated. In this talk I will present a complete propagation-based local search approach for quantifier-free bit-vector formulas. It utilizes conditional inverse value computation on concrete assignments for down-propagation. Computing inverse values of bit-vector operators is not always possible, but we can derive conditions that precisely characterize when bit-vector constraints are invertible. We utilized syntax-guided synthesis techniques to aid in establishing these conditions and verified them independently by using several SMT solvers. I will show how such invertibility conditions can be embedded into quantifier instantiations using Hilbert choice expressions.

We introduce a new way of composing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs circular. We show that, for all sets of standard inference rules, circular proofs are sound. For Frege we show that circular proofs can be converted into tree-like ones with at most polynomial overhead. For Resolution the translation can no longer be a Resolution proof because, as we show, the pigeonhole principle has circular Resolution proofs of polynomial size. Surprisingly, as proof systems for deriving clauses from clauses, Circular Resolution turns out to be equivalent to Sherali-Adams, a proof system for reasoning through polynomial inequalities that has linear programming at its base. As corollaries we get: 1) polynomial-time (LP-based) algorithms that find circular Resolution proofs of constant width, 2) examples that separate circular from dag-like Resolution, such as the pigeonhole principle and its variants, and 3) exponentially hard cases for circular Resolution. This is joint work with Massimo Lauria.

Itsykson and Sokolov in 2014 introduced the class of DPLL(xor) algorithms that solve Boolean satisfiability problem using the splitting by linear combinations of variables modulo 2. This class extends the class of DPLL algorithms that split by variables. DPLL(xor) algorithms solve in polynomial time systems of linear equations modulo 2 that are hard for DPLL, PPSZ and CDCL algorithms. Itsykson and Sokolov have proved first exponential lower bounds for DPLL(xor) algorithms on unsatisfiable formulas. In the talk, we discuss several subclasses of DPLL(xor) algorithms and explain lower bounds for one of them.