previous day
all days

View: session overviewtalk overviewside by side with other conferences

10:30-11:00Coffee Break
11:00-12:00 Session 74E: SMT
Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition

ABSTRACT. Program equivalence checking is a fundamental problem in computer science with applications to translation validation and automatic synthesis of compiler optimizations. Modern equivalence checkers employ SMT solvers to discharge proof obligations generated by their equivalence checking algorithm. Equivalence checkers also involve algorithms to infer invariants that relate the intermediate states of the two programs being compared for equivalence. We present a new algorithm, called {\em invariant-sketching} that allows the inference of the required invariants through the generation of counter-examples using SMT solvers. We also present an algorithm, called {\em query-decomposition} that allows effective use of SMT solvers for application to equivalence checking. Both invariant-sketching and query-decomposition help us prove equivalence across program transformations that could not be handled by previous equivalence checking algorithms.

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
SPEAKER: Ahmed Irfan

ABSTRACT. Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its effectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.

12:00-12:30 Session 75B: Tools & Applications I
XORSAT Set Membership Filters
SPEAKER: Sean Weaver

ABSTRACT. Set membership filters are used as a primary test for whether large sets contain a given element. The most common such filter is the Bloom filter. Most pertinent to this article is the recently introduced Satisfiability (SAT) filter. This article proposes the XOR-Satisfiability (XORSAT) filter, a variant of the SAT filter based on random k-XORSAT. Experimental results show that this new filter can be more than 99% efficient (i.e., achieves the information-theoretic limit) while also having a query speed comparable to the standard Bloom filter, making it practical for use with very large data sets.

12:30-14:00Lunch Break
14:00-15:30 Session 76G: Tools & Applications II
ALIAS: A Modular Tool for Finding Backdoors for SAT
SPEAKER: Oleg Zaikin

ABSTRACT. We present ALIAS, a modular tool aimed at finding backdoors for hard SAT instances. Here by a backdoor for a specific SAT solver and SAT formula we mean a set of its variables, all possible instantiations of which lead to construction of a family of subformulas with the total solving time less than that for an original formula. For a particular backdoor, the tool uses the Monte-Carlo algorithm to estimate the runtime of a solver when partitioning an original problem via said backdoor. Thus, the problem of finding a backdoor is viewed as a black-box optimization problem. The tool's modular structure allows to employ state-of-the-art SAT solvers and black-box optimization heuristics. In practice, for a number of hard SAT instances, the tool made it possible to solve them much faster than using state-of-the-art multithreaded SAT-solvers.

PySAT: A Python Toolkit for Prototyping with SAT Oracles

ABSTRACT. Boolean satisfiability (SAT) solvers are at the core of efficient approaches for solving a vast multitude of practical problems. Moreover, albeit targeting an NP-complete problem, SAT solvers are increasingly used for tackling problems beyond NP. Despite the success of SAT in practice, modeling with SAT and more importantly implementing SAT-based problem solving solutions is often a difficult and error-prone task. This paper proposes the PySAT toolkit, which enables fast Python-based prototyping using SAT oracles and SAT-related technology. PySAT provides a simple API for working with a few state-of-the-art SAT oracles and also integrates a number of cardinality constraint encodings, all aiming at simplifying the prototyping process. Experimental results presented in the paper show that PySAT-based implementations can be as efficient as those written in a low-level language.

Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
SPEAKER: Luca Pulina

ABSTRACT. We consider the problem of binary image generation with given properties. This problem arises in a number of practical applications, including generation of artificial porous medium for an electrode of lithium-ion batteries, for composed materials, etc. A generated image represents a porous medium. As such, it is subject to two sets of constraints: topological constraints on the structure and process constraints on the physical process over this structure. To perform image generation we need to define a mapping from a porous medium to its physical process parameters. For a given geometry of a porous medium, this mapping can be done by solving a partial differential equation (PDE). However, embedding a PDE solver into the search procedure is computationally expensive. We use a binarized neural network to approximate a PDE solver. This allows us to encode the entire problem as a logical formula. Our main contribution is that, for the first time, we show that this problem can be tackled using decision procedures. Our experiments show that our model is able to produce random constrained images that satisfy both topological and process constraints.

15:30-16:00Coffee Break
16:00-18:00 Session 78D: Awards & Competitions
Award Ceremony

ABSTRACT. Presentation of the best paper and best student paper awards.

MaxSAT Evaluation 2018
SPEAKER: Ruben Martins
SPEAKER: Luca Pulina
Sparkle SAT Challenge 2018
SPEAKER: Chuan Luo
SAT Competition 2018
SPEAKER: Marijn Heule