Pragmatics of SAT

a workshop of the 24nd International Conference on Theory and Applications of Satisfiability Testing

July 5, 2021, 3pm-8pm CEST (online event)

News: May 13, 2021 Date and time set The day and time of the workshop has been decided with the SAT conference and workshops chairs.
News: May 10, 2021 Deadlines shifted by one week The abstract and paper submission deadlines and the notification deadlines have been shifted by one week.
News: March 27, 2021 PoS will be also a virtual event After the success of the fully virtual 2020 edition (more than 70 participants), PoS will also be available online, even if the workshop can be organized physically in Barcelona.

Scientific context

Purpose

The aim of the Pragmatics of SAT (PoS) workshop series is to provide a venue for researchers working on designing and/or applying Boolean satisfiability (SAT) solvers and related solver technologies, including but not restricting to satisfiability modulo theories (SMT), answer set programming (ASP), and constraint programming (CP) as well as their optimization counterparts, to meet, communicate, and discuss latest results.

Background

The success of solver technologies for declarative languages, such as SAT, in the last two decades is mainly due to both the availability of numerous efficient solver implementations and to the growing number of problems that can efficiently be solved through the declarative approach. Designing efficient solvers requires both understanding of the fundamental algorithms underlying the solvers, as well as in-depth insights into how to implement the algorithms for obtaining efficient and robust solvers.

Several competitive events are regularly organized for different declarative solving paradigms, including SAT competitions, QBF evaluations, MaxSAT evaluations, SMT, ASP and CP competitions, etc., to evaluate available solvers on a wide range of problems. The winners of such events set regularly new standards in the area. If the systems themselves are widely spread, many details on their design or in their implementation can only be found in the source code of the systems.

The aim of the workshop is to allow researchers to share both fundamental theoretical insights into practical solvers, as well as new implementation-level insights and 'gory' technical details about their systems that may at times be difficult to publish in the main conferences on the declarative solving paradigms.

History

The first edition of PoS took place during FLoC 2010. The second edition took place before SAT 2011, in Ann Arbor. The third edition took place on June 16, 2012, between the second SAT/SMT Summer School (June 12 to 15) and the SAT conference (June 17-20). The fourth edition took place on July 8, once again between the SAT/SMT summer school and the SAT conference. The fifth edition took place during the Vienna Summer of Logic, just before the SAT conference. The sixth edition took place before the SAT conference, in Austin. The seventh edition took place before the SAT conference, in Bordeaux. The eighth edition, colocated with CP and ICLP, was organized on a more general topic of ``Pragmatics of Constraint Reasoning". The ninth edition took place during the Federated Logic Conference in Oxford. The decade edition took place in Lisbon. The eleventh edition was fully virtual due to COVID19.

The 2021 edition is thus the twelfth edition of the workshop dedicated to the practical aspects of SAT research.

Topics

Main areas of interest include, but are not restricted to:

Programme/Venue

The workshop will take place on July 5, 3pm to 8pm CEST, during the SAT conference in Barcelona. It will be an online event, using zoom technology.

The presentations will be live, not pre-recorded, with the possibility to interact with the speaker during the talk.

Technical Programme

2:55pm-3:00pm Introduction to PoS virtual event (rules for speaking, interacting with speaker, etc)
3:00pm-4:00pm Session 1: SAT and applications
3:00pm-3:15pm
MatSat: a matrix-based differentiable SAT solver by Taisuke Sato and Ryosuke Kojima original work
We propose a new approach to SAT solving which solves SAT problems in vector spaces as cost minimization of a differentiable cost function J^{sat}. In our approach, a solution, satisfying assignment, of a SAT problem in n variables is represented by a binary vector u in {0,1} such that J^{sat}(u) = 0. We search for such u in a vector space R^n by cost minimization, i.e., starting from an initial u0, we minimize J^{sat} to zero while iteratively updating u by Newton's method. We implemented our approach as an incomplete matrix-based differentiable SAT solver MatSat. Although existing mainstream SAT solvers decide each bit of a solution assignment one by one, be they of conflict driven clause learning (CDCL) type or of stochastic local search (SLS) type, MatSat fundamentally differs from them in that it changes all variables at once and continuously approaches a solution in a vector space. We conducted experiments to measure the scalability of MatSat with a random 3-SAT problem. In these experiments, we showed that MatSat implemented for GPU can solve the problem with n = 3x10^5 variables, demonstrating the possibility of further acceleration of MatSat by hardware acceleration. We also compared MatSat with nine state-of-the-art CDCL and SLS SAT solvers in terms of execution time by conducting experiments with several random and non-random data sets. In the case of easy random SAT, the performance of MatSat comes between the SLS solvers and the CDCL solvers but is ranked 1st on the difficult one. Similarly, concerning non-random SAT, it shows poor performance for easy cases but outperforms all nine solvers in the difficult case.
Software Benchmarks Slides
3:15pm-3:30pm
Towards CEGAR-based Parallel SAT Solving by Takehide Soh, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura and Katsumi Inoue work in progress
SAT-based methods consist of two steps: (i) encoding step that translates a given problem into a SAT instance, and (ii) solving step that computes a solution using SAT solvers. When speed-up SAT-based methods using parallelization, the use of parallel SAT solvers is promising for improving the step (ii). However, there are sometimes constraints that require a huge number of clauses to encode. Such constraints slow down the step (ii) or abort the SAT-based method at the step (i). In this case, we need a parallelization that takes care of both of the step (i) and (ii). In this paper, we propose a parallel SAT solving based on counterexample guided abstraction refinement (CEGAR). CEGAR is a technique that solves a given problem by iteratively solving abstracted problems that have fewer constraints. The idea is the launch of multiple CEGAR processes and their cooperation by sharing counterexamples. Using Hamiltonian cycle problems as a case study, we show a preliminary result that demonstrates the effectiveness of the proposed parallelization.
Software Benchmarks
3:30pm-3:45pm
A Study of Divide and Distribute Fixed Weights and its Variants by Cayden Codel and Marijn Heule work in progress
Divide and Distribute Fixed Weights (DDFW) is a stochastic local search Boolean satisfiability (SAT) solver that has achieved a high level of performance on select problem instances, including the Pythagorean triples instance for n = 7824. Yet despite its success, DDFW has received little research interest, and its initial results are out of date with respect to more modern SAT benchmarks. To address both those research needs, we examine DDFW in depth and propose modifications to the algorithm based off of ideas from similar SAT solvers such as ProbSAT and SAPS. We then take these modifications and test DDFW against a set of modern hard benchmarks. We present two main findings. The first is a confirmation that a greedy variable selection process in focused search is optimal for DDFW. The second is that it is more effective for unsatisfied clauses to borrow clause weight from its entire neighborhood rather than a singular clause in local minima, as it does in the original algorithm. Using this new strategy, DDFW performs 50% than the original, and this strategy indicates a promising new research direction to investigate for this class of SLS algorithms.
Software Benchmarks Slides
3:45pm-4:00pm
How to Approximate Leximax-optimal Solutions by Miguel Cabral, Mikoláš Janota and Vasco Manquinho original work
Many real-world problems can be modelled as Multi-Objective Combinatorial Optimisation (MOCO) problems. In the multi-objective case, there is not a single optimum value but a set of optima known as Pareto-optima. However, the number of Pareto-optima can be too large to enumerate. Instead, one can compute a minimum Pareto-optimum according to an order. The leximax order selects a Pareto-optimum such that the objective functions with the worst values are penalised the least. Unlike other orders, such as the lexicographic order or the weighted sum order, the leximax order does not favour any objective function at the expense of others. Also, the leximax-optimum has a guaranteed small trade-off between the objective functions. In some real-world MOCO problems, the time to find a solution may be limited and computing a leximax-optimal solution may take too long. In such problems, we search for solutions that can be computed in the given admissible amount of time and that are as close to the leximax-optimum as possible. In other words, we approximate the leximax-optimum. In this paper, we present and evaluate SAT-based algorithms and heuristics for approximating the leximax-optimum of Multi-Objective Boolean Satisfiability problems. The evaluation is performed in the context of the package upgradeability problem, on the set of benchmarks from the Mancoosi International Solver Competition, with combinations of up to five different objective functions.
Benchmarks
4:00pm-4:15pm Virtual break
4:15pm-5:15pm Session 2: Pseudo-Boolean solving and certification
4:15pm-4:30pm
Certifying CNF Encodings of Pseudo-Boolean Constraints by Stephan Gocht, Ruben Martins and Jakob Nordstrom work in progress
The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the conjunctive normal form (CNF) format used for SAT proof logging means that it is hard to extend the method to other, stronger, solving paradigms for combinatorial problems. We show how to instead leverage the cutting planes proof system to provide proof logging for pseudo-Boolean solvers that translate pseudo-Boolean problems (a.k.a 0-1 integer linear programs) to CNF and run CDCL. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.
Software Slides
4:30pm-4:45pm
On Improving the Backjump Level in PB Solvers by Romain Wallon work in progress
Current PB solvers implement many techniques inspired by the CDCL architecture of modern SAT solvers, so as to benefit from its practical efficiency. However, they also need to deal with the fact that many of the properties leveraged by this architecture are no longer true when considering PB constraints. In this paper, we focus on one of these properties, namely the optimality of the so-called first unique implication point (1-UIP). While it is well known that learning the first assertive clause produced during conflict analysis ensures to perform the highest possible backjump in a SAT solver, we show that there is no such guarantee in the presence of PB constraints. We also introduce and evaluate different approaches designed to improve the backjump level identified during conflict analysis by allowing to continue the analysis after reaching the 1-UIP. Our experiments show that sub-optimal backjumps are fairly common in PB solvers, even though their impact on the solver is not clear.
Software Data Slides
4:45pm-5:00pm
Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs by Stephan Gocht and Jakob Nordstrom AAAI'21 paper presentation
The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the conjunctive normal form (CNF) format used for SAT proof logging means that it is hard to extend the method to other, stronger, solving paradigms for combinatorial problems. We show how to instead leverage the cutting planes proof system to provide proof logging for pseudo-Boolean solvers that translate pseudo-Boolean problems (a.k.a 0-1 integer linear programs) to CNF and run CDCL. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.
Software AAAI'21 paper Slides
5:00pm-5:15pm
Branching strategies for solving pseudo-Boolean optimization problems using Integer-programming solvers by Srinivas Tamvada and Elkafi Hassini work in progress
Pseudo-Boolean Optimization problems (PBOs) are an important class of Integer Lin- ear Programming (ILP) problems that arise frequently in industrial applications. While specialized solvers exist for PBOs, ILP solvers can be useful for solving hard PBOs to within a certain integrality gap. This paper incorporates popular PBO branching heuristics into a commercial ILP solver. A novel heuristic called Trigger Equivalence and Domination is developed for speeding up look-ahead based branching. Experiments with hard-to-solve instances indicate that the proposed heuristics are an attractive alternative to conventional strong branching. Testing results from an industrial application are also presented.
Slides
5:15pm-5:30pm Virtual break
5:30pm-6:30pm
Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results by Roberto Sebastiani invited talk
Quantum annealers (QAs) are specialized quantum computers that minimize objective functions over discrete variables by physically exploiting quantum effects. Current QA platforms allow for the optimization of quadratic objectives defined over binary variables (qubits), also known as Ising problems. In the last decade, QA systems as implemented by D-Wave have scaled with Moore-like growth. Current architectures provide >5000 sparsely-connected qubits, and continued exponential growth is anticipated, together with increased connectivity. We explore the feasibility of such architectures for solving SAT and MaxSAT problems as QA systems scale. We develop techniques for effectively encoding SAT –and, with some limitations, MaxSAT– into Ising problems compatible with sparse QA architectures. We provide the theoretical foundations for this mapping, and present encoding techniques that combine offline Satisfiability and Optimization Modulo Theories with on-the-fly placement and routing. Preliminary empirical tests on a current generation D-Wave system support the feasibility of the approach for certain SAT and MaxSAT problems.
6:30pm-6:45pm Virtual break
6:45pm-7:45pm Session 3: Core SAT
6:45pm-7:00pm
Bipartite Perfect Matching Benchmarks by Cayden Codel, Joseph Reeves, Marijn Heule and Randal Bryant original work
The pigeonhole and mutilated chessboard problems are challenging benchmarks for most SAT solvers. Although some solvers employ special techniques that efficiently solve the canonical versions of these two problems, these techniques may fail with even slight problem variations. To evaluate and improve the robustness of SAT solvers, we designed a benchmark family of perfect matching problems on bipartite graphs that generalizes the pigeonhole and mutilated chessboard problems. Our benchmark generator supports various encodings and randomized constructions. Experimental results show that different variations degrade the performance of solvers in unexpected ways. As such, the benchmark family, taken as a whole, provides a good way to reveal the fragility of fine-tuned solving techniques. Tuning against it will encourage more robust solver implementations. We also studied the effect that adding symmetry-breaking clauses has on solver performance. We found that general solvers perform better with additional symmetry-breaking clauses, while some solvers that rely on special solving techniques perform worse.
Benchmarks Slides
7:00pm-7:15pm
The Impact of Bounded Variable Elimination on Pigeonhole Formulas by Joseph Reeves and Marijn Heule original work
Variable elimination is arguably the most important pre- and in-processing technique in state-of-the-art SAT solvers. There are hardly any problems for which variable elimination by substitution, as presented by Eén and Biere in 2005, hurts performance. However, during an experimental study, we observed that variable elimination resulted in substantial slowdowns of the 2020 SAT Competition winner Kissat on pigeonhole formulas. In this paper we evaluated the impact of different variable elimination orderings on solving pigeonhole formulas using recent SAT competition winners. The results show that some solvers are more stable than others, while the formulas obtained by some elimination orderings are consistently more difficult to solve. Further, we implemented static variable decision heuristics in the solver CaDiCaL that outperformed all other solvers.
Software Benchmarks Data Slides
7:15pm-7:30pm
Mining Definitions in Kissat with Kittens by Mathias Fleury and Armin Biere original work
Bounded variable elimination is one of the most important preprocessing techniques in SAT solving. It benefits from discovering functional dependencies in the form of definitions encoded in the CNF. While the original approach relied on syntactic pattern matching our new approach uses cores produced by an embedded SAT solver. In contrast to a similar semantic approach in Lingeling based on BDD algorithms, our new approach is able to generate DRAT proofs. We further discuss design choices for our embedded SAT solver Kitten. Experiments with Kissat show the effectiveness of this approach.
Software Slides
7:30pm-7:45pm
An Experimental Study of Permanently Stored Learned Clauses by Sima Jamali and David original work Mitchell
Modern CDCL SAT solvers learn clauses rapidly, and an important heuristic is the clause deletion scheme. Most current solvers have two (or more) stores of clauses. One has ``valuable'' clauses which are never deleted. Most learned clauses are added to the other, with an aggressive deletion strategy to restrict its size. Recent solvers in the MapleSAT family, have comparatively complex deletion scheme, and perform well. Many solvers store only binary clauses permanently, but MapleSAT family of solvers store clauses with small LBD permanently. We report an experimental study of the permanent clause store in MapleLCMDistChronoBT. We observe that this store can get quite large, but several methods for limiting its size reduced performance. We also show that alternate size and LBD based criteria improve performance, while still having large permanent stores. In particular, saving clauses up to size 8, and adding small numbers of high-centrality clauses, both improved performance, with the best improvement using both methods.
7:45pm-8:00pm Session 4: open discussion
8:00pm Closing

Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results by Roberto Sebastiani

Roberto Sebastiani

Invited talk, July 5, 5:30pm-6:30pm CEST Quantum annealers (QAs) are specialized quantum computers that minimize objective functions over discrete variables by physically exploiting quantum effects. Current QA platforms allow for the optimization of quadratic objectives defined over binary variables (qubits), also known as Ising problems. In the last decade, QA systems as implemented by D-Wave have scaled with Moore-like growth. Current architectures provide >5000 sparsely-connected qubits, and continued exponential growth is anticipated, together with increased connectivity. We explore the feasibility of such architectures for solving SAT and MaxSAT problems as QA systems scale. We develop techniques for effectively encoding SAT –and, with some limitations, MaxSAT– into Ising problems compatible with sparse QA architectures. We provide the theoretical foundations for this mapping, and present encoding techniques that combine offline Satisfiability and Optimization Modulo Theories with on-the-fly placement and routing. Preliminary empirical tests on a current generation D-Wave system support the feasibility of the approach for certain SAT and MaxSAT problems.

This invited talk will be based on the material available in the following paper, plus a few more recent developments.

            Zhengbing Bian, Fabián A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti:
            Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results. Inf.
            Comput. 275: 104609 (2020)
            
Available online at https://doi.org/10.1016/j.ic.2020.104609. Preprint available at the presenter's publication web page.

Registration

Registration for the workshop is available on the main conference web site. Registration is free but mandatory.

Submission

The workshop welcomes three categories of papers:

Each submission will be reviewed by at least three members of the programme committee.

The papers must be submitted electronically through EasyChair as a PDF file using the EasyChair proceedings style. Each submission is limited to 14 pages, plus references.

Authors should provide enough information and/or data for reviewers to confirm any performance claims. This includes links to a runnable system, access to benchmarks, reference to a public performance results, etc.

Unlike previous editions, there will be no workshop proceedings.

High-quality original papers will be selected by the PC for fast-track reviewing for potential publication in Journal on Satisfiability, Boolean Modeling and Computation (JSAT), subject to a second formal review process.

Important dates

Programme Committee

Contact

For any questions related to the workshop, the preferred solution to contact the organizers is to send an email to pos at pragmaticsofsat.org.

Matti Järvisalo                               Daniel Le Berre
University of Helsinki                        Universite d'Artois
Department of Computer Science / HIIT         CNRS
P.O. Box 68, FI-00014, Finland                Rue Jean Souvraz SP 18 62307 Lens FRANCE
https://www.cs.helsinki.fi/u/mjarvisa/        http://www.cril.fr/~leberre