Schedule for: 18w5208 - Theory and Practice of Satisfiability Solving
Beginning on Sunday, August 26 and ending Friday August 31, 2018
All times in Oaxaca, Mexico time, CDT (UTC-5).
Sunday, August 26 | |
---|---|
14:00 - 23:59 | Check-in begins (Front desk at your assigned hotel) |
19:30 - 22:00 | Dinner (Restaurant Hotel Hacienda Los Laureles) |
20:30 - 21:30 | Informal gathering (Hotel Hacienda Los Laureles) |
Monday, August 27 | |
---|---|
07:30 - 08:45 | Breakfast (Restaurant at your assigned hotel) |
08:45 - 09:00 | Introduction and Welcome (Conference Room San Felipe) |
09:00 - 10:00 |
Laurent Simon: Towards an (experimental) understanding of SAT Solvers ↓ 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. (Conference Room San Felipe) |
10:00 - 11:00 |
Massimo Lauria: Introduction to Proof Complexity for SAT practitioner ↓ 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. (Conference Room San Felipe) 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. |
11:00 - 11:30 | Coffee Break (Conference Room San Felipe) |
11:30 - 12:30 |
Marijn Heule: Computable 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. (Conference Room San Felipe) 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. |
12:30 - 13:15 | Presentation of participants (Conference Room San Felipe) |
13:20 - 13:30 | Group Photo (Hotel Hacienda Los Laureles) |
13:30 - 14:30 | Lunch (Restaurant Hotel Hacienda Los Laureles) |
14:30 - 16:00 | Siesta (Conference Room San Felipe) |
16:00 - 16:30 | Coffee Break (Conference Room San Felipe) |
16:30 - 17:30 |
Jo Devriendt: Symmetry in SAT - a quest for pigeonhole ↓ 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. (Conference Room San Felipe) 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. |
17:30 - 18:00 |
Stephan Gocht: Seeking Practical CDCL Insights from Theoretical SAT Benchmarks ↓ 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. (Conference Room San Felipe) 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. |
18:00 - 18:30 |
Susanna de Rezende: Clique Is Hard for State-of-the-Art Algorithms ↓ 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. (Conference Room San Felipe) 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)}$. |
18:30 - 19:00 |
Moshe Vardi: Boolean Satisfiability: Theory and Engineering ↓ 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. (Conference Room San Felipe) 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. |
19:00 - 21:00 | Dinner (Restaurant Hotel Hacienda Los Laureles) |
Tuesday, August 28 | |
---|---|
07:30 - 09:00 | Breakfast (Restaurant at your assigned hotel) |
09:00 - 10:00 |
Jakob Nordstrom: Towards Faster Conflict-Driven Pseudo-Boolean 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. (Conference Room San Felipe) 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. |
10:00 - 11:00 |
Fahiem Bacchus: MaxSat, successful solution techniques and some questions they raise. ↓ 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. (Conference Room San Felipe) 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. |
11:00 - 11:30 | Coffee Break (Conference Room San Felipe) |
11:30 - 12:30 |
Nikolaj Bjorner: SMT solving - foundations and directions ↓ This talk provides a survey of SMT solving with an emphasis on recent developments and directions.
(Conference Room San Felipe)
|
12:30 - 13:30 |
Ambros Gleixner: Computational Mixed-Integer Programming ↓ 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. (Conference Room San Felipe) |
13:30 - 14:30 | Lunch (Restaurant Hotel Hacienda Los Laureles) |
14:30 - 16:00 | Siesta (Conference Room San Felipe) |
16:00 - 16:30 | Coffee Break (Conference Room San Felipe) |
16:30 - 17:00 |
Joao Marques-Silva: Towards MaxSAT-Based Proof Systems ↓ 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. (Conference Room San Felipe) |
17:00 - 17:30 |
Nina Narodytska: Formal Analysis of Deep Binarized Neural Networks ↓ 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. (Conference Room San Felipe) |
17:30 - 18:00 |
Daniel Le Berre: Pseudo-Boolean Optimization ↓ 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. (Conference Room San Felipe) |
18:00 - 18:30 |
Marc Vinyals: Proof Systems for Pseudo-Boolean Solving ↓ 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? (Conference Room San Felipe) 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. |
18:30 - 19:00 |
Sam Buss: The (un)reasonable (in)effectiveness of theory for Sat solvers ↓ 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. (Conference Room San Felipe) |
19:00 - 20:30 | Dinner (Restaurant Hotel Hacienda Los Laureles) |
20:30 - 22:00 |
Demo session, discussion on empirical evaluation ↓ 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 (Conference Room San Felipe) |
Wednesday, August 29 | |
---|---|
07:30 - 09:00 | Breakfast (Restaurant at your assigned hotel) |
09:00 - 10:00 |
Mikoláš Janota: Advances in QBF Solving ↓ 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. (Conference Room San Felipe) |
10:00 - 11:00 |
Olaf Beyersdorff: QBF Proof Complexity ↓ 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. (Conference Room San Felipe) 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. |
11:00 - 11:30 | Coffee Break (Conference Room San Felipe) |
11:30 - 12:30 |
Klas Markström: Random k-sat. A review and some new results. ↓ 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. (Conference Room San Felipe) 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. |
12:30 - 13:30 | Lunch (Restaurant Hotel Hacienda Los Laureles) |
13:30 - 19:00 | Free Afternoon (Oaxaca) |
19:00 - 21:00 | Dinner (Restaurant Hotel Hacienda Los Laureles) |
Thursday, August 30 | |
---|---|
07:30 - 09:00 | Breakfast (Restaurant at your assigned hotel) |
09:00 - 10:00 |
Manuel Kauers: Gröbner bases and applications ↓ 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. (Conference Room San Felipe) |
10:00 - 11:00 |
Susan Margulies: Hilbert's Nullstellensatz, Grobner Bases, and NP-Complete Problems ↓ 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. (Conference Room San Felipe) |
11:00 - 11:30 | Coffee Break (Conference Room San Felipe) |
11:30 - 12:30 |
Rahul Santhanam: A Survey on Worst-Case Complexity of SAT ↓ 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. (Conference Room San Felipe) |
12:30 - 13:00 |
Kristin Yvonne Rozier: MAX-SAT for Temporal Logics ↓ 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! (Conference Room San Felipe) 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. |
13:00 - 13:30 |
Ruben Martins: Conflict-Driven Synthesis ↓ 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. (Conference Room San Felipe) 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. |
13:30 - 14:30 | Lunch (Restaurant Hotel Hacienda Los Laureles) |
14:30 - 16:00 | Siesta (Conference Room San Felipe) |
16:00 - 16:30 | Coffee Break (Conference Room San Felipe) |
16:30 - 17:00 |
Martina Seidl: The Symmetry Rule for Quantified Boolean Formulas ↓ 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). (Conference Room San Felipe) 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. |
17:00 - 17:30 |
Antonina Kolokolova: The Proof Complexity of SMT Solvers ↓ 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. (Conference Room San Felipe) 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. |
17:30 - 18:00 |
Nathan Mull: On CDCL-based Proof Systems with the Ordered Decision Strategy ↓ 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. (Conference Room San Felipe) 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. |
18:00 - 18:30 |
Maria Luisa Bonet: Algorithms beyond Resolution using MaxSAT ↓ 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. (Conference Room San Felipe) |
18:30 - 19:00 | Laurent Simon: A few results, questions, and pitfalls in the experimental study of SAT solvers (Conference Room San Felipe) |
19:00 - 21:00 | Dinner (Restaurant Hotel Hacienda Los Laureles) |
Friday, August 31 | |
---|---|
07:30 - 09:00 | Breakfast (Restaurant at your assigned hotel) |
09:00 - 09:30 |
Kuldeep Meel: CrystalBall: Gazing in the Black Box of SAT Solving ↓ 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? (Conference Room San Felipe) 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) |
09:30 - 10:00 | Vijay Ganesh: Machine Learning for SAT Solvers (Conference Room San Felipe) |
10:00 - 10:30 |
Aina Niemetz: From Local Search to Quantifier Elimination for Bit-Vectors in SMT ↓ 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. (Conference Room San Felipe) |
10:30 - 11:00 | Coffee Break (Conference Room San Felipe) |
11:00 - 11:30 |
Albert Atserias: Circular (Yet Sound) Proofs ↓ 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. (Conference Room San Felipe) |
11:30 - 12:00 |
Alexander Knop: Hard Satisfiable Formulas for Splittings by Linear Combinations ↓ 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. (Conference Room San Felipe) |
12:00 - 14:00 | Lunch (Restaurant Hotel Hacienda Los Laureles) |