SAT on Sunday, July 11th

09:00‑10:00 SAT Invited Talk
Location: AT LT2
09:00 Yehuda Naveh
The Big Deal: Applying Constraint Satisfaction Technologies Where it Makes the Difference

In my talk, I will present a few industrial-scale applications of satisfaction technology (constraint programming and satisfiability), all of which are of prime importance to the respective business. The talk will focus on high-end solutions to unique but immense problems. This, as opposed to off-the-shelf solutions which are suitable for more commoditized problems. I argue that the former case is where cuttingedge satisfaction technology can bring the most significant impact. The following is an extended abstract of my talk.

10:30‑12:30 Heuristics
Location: AT LT2
10:30 Stephan Kottler
SAT Solving with Reference Points

Many state-of-the-art SAT solvers use a variant of the VSIDS heuristic to make branching decisions based on the activity of variables or literals. In combination with rapid restarts and phase saving this yields a powerful decision heuristic in practice. However, there are approaches that motivate more in-depth reasoning to guide the search of the SAT solver. But more reasoning often requires more information and comes along with more complex data-structures. This may sometimes even cause strong concepts to be inapplicable in practice.

In this paper we present a suitable data-structure for the DMRP approach (Decision Making with Reference Points). Moreover, we show how DMRP can be combined with CDCL solving to be competitive to state-of-the-art solvers and to even improve on some families of industrial instances.

11:00 Dave Tompkins and Holger Hoos
Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT

We introduce a new conceptual model for representing and designing Stochastic Local Search (SLS) algorithms for the propositional Satisfiability problem (SAT). Our model can can be seen as a generalisation of existing variable weighting, scoring and selection schemes; it is based upon the concept of Variable Expressions (VEs), which use properties of variables to construct dynamic scoring functions. We illustrate how prominent existing SLS algorithms fit within our model and then demonstrate how our model and VEs can be to construct more advanced algorithms and scoring functions. To explore the potential of our model, we introduce the Design Architecture for Variable Expressions (DAVE) that allows users to specify SLS algorithms based on complex dynamic variable scoring via the command line. Using DAVE, we can easily specify rich design spaces of novel SLS algorithms, and subsequently explore these using an automated algorithm configuration tool. We demonstrate that by following this approach, we can achieve improvements over previous state-of-the-art SLS-based SAT solvers on interesting classes of SAT benchmarks.

11:30 Alexander Nadel and Vadim Ryvchin
Assignment Stack Shrinking

Assignment stack shrinking is a technique that is intended to speed up the performance of modern complete SAT solvers. Shrinking was shown to be efficient in SAT'04 competition winners Jerusat and Chaff. However, existing studies lack the details of the shrinking algorithm. In addition, shrinking's performance was not tested in conjunction with the most modern algorithms. This paper provides a detailed description of the shrinking algorithm and proposes an empirically useful enhancement to it. We show that using shrinking is critical for solving well-known industrial benchmark families with the latest versions of Minisat and Eureka.

11:50 Matti Järvisalo and Armin Biere
Reconstructing Solutions after Blocked Clause Elimination

Preprocessing has proven important in enabling efficient Boolean satisfiability (SAT) solving. For many real application scenarios of SAT it is important to be able to extract a full satisfying assignment for original SAT instances from a satisfying assignment for the instances after preprocessing. We show how such full solutions can be efficiently reconstructed from solutions to the conjunctive normal form (CNF) formulas resulting from applying a combination of various CNF preprocessing techniques implemented in the PrecoSAT solver---especially, blocked clause elimination combined with SatElite-style variable elimination and equivalence reasoning.

12:10 Ashish Sabharwal, Bart Selman and Lukas Kroc
An Empirical Study of Optimal Noise and Runtime Distributions in Local Search

This paper presents a detailed empirical study of local search for Boolean satisfiability (SAT), highlighting several interesting properties, some of which were previously unknown or had only anecdotal evidence. In particular, we study hard random 3-CNF formulas and provide surprisingly simple analytical fits of the optimal noise level and the runtime at optimal noise, as a function of the clause-to-variable ratio. We also demonstrate that the runtime distributions in the low noise regime have tails that decay in a power-law fashion. This, we believe, is the first time a clear power-law decay has been observed in a local search method. Finally, we discuss ideas for a Markov Chain model for local search that captures this intriguing feature.

14:00‑15:00 FLoC Plenary Talks: tribute to Amir and Robin
Chair: Moshe Vardi
Location: George Square Lecture Theatre
14:00 David Harel (Weizmann Institute of Science)
Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's.
14:30 Gordon Plotkin (University of Edinburgh)
Robin Milner, a Craftsman of Tools for the Mind.
15:30‑17:30 Theory + Combinatorics
Location: AT LT2
15:30 Kazuhisa Makino, Suguru Tamaki and Masaki Yamamoto
An Exact Algorithm for the Boolean Connectivity Problem for k-CNF

We present an exact algorithm for a PSPACE-complete problem, denoted by $\CONN k\SAT$, which asks if the solution space for a given $k$-CNF formula is connected on the $n$-dimensional hypercube. The problem is known to be PSPACE-complete for $k\geq 3$, and polynomial solvable for $k\leq 2$ \cite{GKMP06}. We show that $\CONN k\SAT$ for $k\geq 3$ is solvable in time $O((2-\epsilon_k)^n)$ for some constant $\epsilon_k>0$, where $\epsilon_k$ depends only on $k$, but not on $n$. This result is considered to be interesting due to the following fact shown by \cite{Cal09}: QBF-3-SAT, which is a typical PSPACE-complete problem, is not solvable in time $O((2-\epsilon)^n)$ for any constant $\epsilon>0$, provided that the SAT problem (with no restriction to the clause length) is not solvable in time $O((2-\epsilon)^n)$ for any constant $\epsilon>0$.

16:00 Hadi Katebi, Karem Sakallah and Igor Markov
Symmetry and Satisfiability: An Update

The past few years have seen significant progress in algorithms and heuristics for both SAT and symmetry detection. Additionally, the thesis that some of SAT’s intractability can be explained by the presence of symmetry, and that it can be addressed by the introduction of symmetry-breakling constraints, was tested, albeit only to a rather limited extent. In this paper we explore further connections between symmetry and satisfiability and demonstrate the existence of intractable SAT instances that exhibit few or no symmetries. Specifically, we describe a highly scalable symmetry detection algorithm based on a decision tree that combines elements of group-theoretic computation and SAT-inspired backtracking search, and provide results of its application on the SAT competition benchmarks. For SAT instances with significant symmetry we also compare SAT runtimes with and without the addition of symmetry-breaking constraints.

16:30 Stefan Porschen, Tatjana Schmidt and Ewald Speckenmeyer
Complexity Results for Linear XSAT Problems

We investigate the computational complexity of the exact satisfiability problem (XSAT) restricted to certain subclasses of linear CNF formulas. These classes are defined through restricting the number of occurrences of variables and are therefore interesting because the complexity status does not follow from Schaefer's theorem. Specifically we prove that XSAT remains NP-complete for linear formulas which are monotone and all variables occur exactly l times. We also present some complexity results for exact linear formulas. Concretely, we show that XSAT for this class is NP-complete, in contrast to SAT or NAESAT. This can be also established when clauses have length at least k, for fixed integer k >= 3. However, the XSAT-complexity for exact linear formulas with clause length exactly k remains open, but we provide its polynomial-time behaviour at least for every positive integer k<= 6.

17:00 Olaf Beyersdorff, Arne Meier, Sebastian Mueller, Michael Thomas and Heribert Vollmer
Proof Complexity of Propositional Default Logic

Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen's system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti's enhanced calculus for skeptical default reasoning.