SAT on Wednesday, July 14th

09:00‑10:00 SAT Invited Tutorial
Location: AT LT2
09:00 Daniel Kroening
A Primer on the Algorithmic Aspects of Satisfiability Modulo Theories
10:30‑12:30 Optimization + SAT Usage
Location: AT LT2
10:30 Vasco Manquinho, Ruben Martins and Inês Lynce
Improving Unsatisfiability-based Algorithms for Boolean Optimization

Recently, several unsatisfiability-based algorithms have been proposed for Maximum Satisfiability (MaxSAT) and other Boolean Optimization problems. These algorithms are based on being able to iteratively identify and relax unsatisfiable sub-formulas with the use of fast Boolean satisfiability solvers. It has been shown that this approach is very effective for several classes of instances, but it can perform poorly on others for which classical Boolean optimization algorithms find it easy to solve. This paper proposes the use of Pseudo-Boolean Optimization (PBO) solvers as a preprocessor for unsatisfiability-based algorithms in order to increase its robustness. Moreover, the use of constraint branching, a well-known technique from Integer Linear Programming, is also proposed into the unsatisfiability-based framework. Experimental results show that the integration of these features in an unsatisfiability-based algorithm results in an improved and more effective solver for Boolean optimization problems.

11:00 Denis Pankratov and Allan Borodin
On the Relative Merits of Simple Local Search Methods for the Max Sat Problem

Abstract. Algorithms based on local search are popular techniques for solving many optimization problems including the maximum satisfiability problem (MAXSAT). With regard to MAXSAT, the state of the art in performance seems to be variants of maxwalksat (MWS), a stochastic local search method. Local search methods are conceptually simple, and they often provide near optimal solutions. In contrast, it is relatively rare that local search algorithms are analyzed with respect to the worst-case approximation ratios. In the first part of the paper, we build on Mastrolilli and Gambardella’s work [1] and present a worst-case analysis of tabu search for the MAX-k-SAT problem. In the second part of the paper, we examine experimental performance of determinstic local search algorithms (oblivious and non-oblivious local search, tabu search) in comparison to the better performing stocahstic methods (simulated annealing and MWS) on random formulas and on benchmarks from MAX-SAT competitions. Tabu search consistently outperforms both oblivious and non-oblivious local search but does not match the performance of simulated annealing and MWS. However, tabu search when initialized by non-oblivious local search is reasonably competitive. Furthermore, the better performance of the various methods that escape local optima in comparison to the more basic oblivious and non oblivious local search algorithms (that stop at local optima) comes at a cost, namely a significant increase in complexity (which we measure in terms of variable flips). The performance results observed for the unweighted MAX-k-SAT problem carry over to the weighted version of the problem.

References 1. M. Mastrolilli and L. M. Gambardella. Max-2-sat: How good is tabu search in the worst-case? In AAAI, pages 173–178, 2004.

11:30 Chu-Min LI, Felip Manya, Zhe Quan and Zhu Zhu
Exact MinSAT Solving

MinSAT is the problem of finding a truth assignment that minimizes the number of satisfied clauses in a CNF formula. We present an original approach to exact MinSAT solving, which relies on solving MinSAT using MaxSAT encodings and MaxSAT solvers. Our empirical investigation provides evidence that, in the absence of genuine exact solvers for MinSAT, the generic approach proposed in this paper is competitive.

11:50 Rüdiger Ehlers
Minimising Deterministic Büchi Automata Precisely using SAT Solving

We show how deterministic Büchi automata can be fully minimised by reduction to the SAT problem, yielding the first automated method for this task. Size reduction of such omega-automata is an important step in probabilistic model checking as well as synthesis of finite-state systems. Our experiments demonstrate that state-of-the-art SAT solvers are capable of solving the these instances quickly, making the approach presented valuable in practice.

12:10 Gayathri Namasivayam and Mirosław Truszczynski
Simple but Hard Mixed Horn Formulas

We study simple classes of mixed Horn formulas, in which the structure of the Horn part is drastically constrained. We show that the SAT problem for formulas in these classes remains NP-complete, and demonstrate experimentally that formulas randomly generated from these classes are hard for the present SAT solvers, both complete and local-search ones.

14:00‑14:50 Joint SAT/SMT session
Location: AT LT2
14:00 Miquel Bofill, Josep Suy and Mateu Villaret
A system for solving constraint satisfaction problems with SMT

SAT Modulo Theories (SMT) consists of deciding the satisfiability of a formula with respect to a decidable background theory, such as linear integer arithmetic, bit-vectors, etc, in first-order logic with equality. SMT has its roots in the field of verification. It is known that the SAT technology offers an interesting, efficient and scalable method for constraint solving, as many experimentations have shown. Although there already exist some results pointing out the adequacy of SMT techniques for constraint solving, there are no available tools to extensively explore such adequacy. In this paper we introduce a tool for translating FlatZinc (MiniZinc intermediate code) instances of constraint satisfaction problems to the standard SMT-LIB language. It can be used for deciding satisfiability as well as for optimization. The tool determines the required logic for solving each instance. The obtained results suggest that SMT can be effectively used to solve CSPs.

14:20 J. Christ, J. Hoenicke
(SMT'10) Instantiation-Based Interpolation for Quantified Formulae
15:30‑17:30 Competitions
Location: AT LT2
15:30 Claudia Peschiera, Luca Pulina, Armando Tacchella, Uwe Bubeck, Oliver Kullmann and Ines Lynce
The Seventh QBF Solvers Evaluation (QBFEVAL'10)

For almost a decade now, competitive events in the field of Boolean reasoning have influenced related research agendas and shaped the course of tool developments. Researchers and practitioners look at the results of these events as the preferred way to understand the current state of the art. It is therefore important, in any such event, to reach a comprehensive understanding of the testing methods and the latest results. In this paper we report about QBFEVAL'10, the seventh in a series of events established with the aim of assessng the advancements in reasoning about quantified Boolean formulas (QBFs). To reflect an increasing diversification in the latest research on QBF, in QBFEVAL'10 thirteen solvers were evaluated on five different tracks, for a total of XXX QBF instances. Besides the main prenex/CNF track using QDIMACS instances coming from diverse application domains, we also run specialized tracks on random prenex/CNF QBFs, small-but-hard QBFs, single-alternation ($\forall\exists$) QBFs, and non-prenex non-CNF QBFs. The paper discusses the results obtained and the experimental setup, from the criteria used to select QBF instances down to the evaluation infrastructure. We also discuss the current state-of-the-art in light of past challenges and we envision future research directions that are motivated by the results of QBFEVAL'10.

16:00 Competition
16:30 Competition
17:00 Competition