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:

• techniques for debugging or certifying solvers
• visualisation of benchmarks structure
• monitoring solver behaviour
• evaluation of solvers
• efficient data structures
• domain specific encodings
• taking into account multi-core technology
• domain specific heuristics
• new application of constraint-based technologies
• new use cases of constraint-based technologies
• system/library description
• solver API
• constraint solving and machine learning

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 Preprint
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 SAT'22 paper
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 SAT'22 paper
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 Mitchell original work 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

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.

Bio Roberto Sebastiani is Professor of Artificial Intelligence, Automated Reasoning and Formal Methods at Dipartimento di Ingegneria e Scienza dell'Informazione (DISI), Università di Trento, Italy. His main research topics are Automated Reasoning (in particular SAT, SMT and OMT), Formal Verification (in particular, model checking) and their applications. Roberto built his first SAT-based system in 1993, has built various automated reasoning tools for various logics and has been an active member of the creation of the SMT framework. In 2006, he organized with Byron Cook the Pragmatics of Decision Procedures in Automated Reasoning workshop at FLoC, which inspired PoS for the next FLoC in 2010.

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:

• Original papers describing original work on a topic of the workshop, including papers whose focus might be too narrow to be published in a conference. Short original papers, approximately 6-8 pages in length, including system descriptions of SAT and related solver technologies are also welcome.
• Work-in-progress papers describing less mature work on a topic of the workshop, to gather feedback from the community. It may include papers submitted to conferences or journals, which should be clearly stated in the paper.
• Presentation-only papers describing a work on a topic of the workshop recently accepted or published to another conference or a journal, but that the community may have missed (including, e.g., domain-specific applications of declarative solvers at the respective domain-specific conferences). Submissions to this category will be evaluated only on their relevance to the workshop.

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

• Abstract submission deadline: May 9 16, 2021 (soft, submit ASAP)
• Paper submission deadline: May 16 23, 2021
• Notification to authors: June 6 13, 2021
• Final version due: June 27, 2021
• Workshop: July 5, 2021

Programme Committee

• Jeremias Berg, University of Helsinki / HIIT
• Armin Biere, Johannes Kepler University Linz
• Marijn Heule, Carnegie Mellon University
• Hidetomo Nabeshima, University of Yamanashi
• Alexey Ignatiev, Monash University
• Matti Jarvisalo, University of Helsinki chair
• Daniel Le Berre, University of Artois - CNRS chair
• Kuldeep Meel, National University of Singapore
• Aina Niemetz, Stanford University
• Olivier Roussel, University of Artois - CNRS
• Romain Wallon, École Polytechnique

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