SAT on Tuesday, August 15th

Competitions (09:00‑10:00)
Chair: João Marques-Silva

09:00‑09:20	Carsten Sinz SAT-Race Information on the SAT-Race remains on separate page.
09:20‑09:40	Olivier Roussel Pseudo Boolean Evaluation Information on the Pseudo Boolean Evaluation resides on a separate page.
09:40‑10:00	Armando Tacchella QBF Evaluation Information on the QBF Evaluation resides on a separate page.

Break (10:00‑10:30)

Session 8: QBF (10:30‑12:30)
Chair: Lintao Zhang

10:30‑11:00	Hans Kleine Büning (University of Paderborn) Xishun Zhao (Insitute of Logic and Cognition, Sun Yat-Sen University) Minimal False Quantified Boolean Formulas This paper is concerned with the minimal falsity problem MF for quantified Boolean formulas. A QCNF formula (i.e., with CNF-matrix) is called minimal false, if the formula is false and any proper subformula is true. It is shown that the minimal falsity problem is PSPACE-complete. Then the deficiency of a QCNF formula is defined as the difference between the number of clauses and the number of existentially quantified variables. For quantified Boolean formulas with deficiency one, MF is solvable in polynomial time. For QEHIT formulas (with hitting existential parts), MF can also be solved efficiently.
11:00‑11:30	Horst Samulowitz (University of Toronto) Fahiem Bacchus (University of Toronto) Binary Clause Reasoning in QBF Binary clause reasoning has found some success applications in SAT, and it is natural to investigate its use in various extensions of SAT. In this paper we investigate the use of binary clause reasoning in context of solving Quantified Boolean Formulas (QBF). We develop a DPLL based QBF solver that employs extended binary clause reasoning (hyper-binary resolution) to infer new binary clauses both before and during search. These binary clauses are used to discover additional forced literals, as well as to perform equality reduction (whereby all instances of a literal are replaced by an equivalent literal). Both of these transformations simplify the theory by removing one of its variables. This stronger inference applied during DPLL search can offer significant decreases in the size of the search tree, but it can also be costly to apply. We are able to show empirically that despite the extra costs binary clause reasoning is often able to improve our ability to solve QBF.
11:30‑12:00	Daijue Tang (Princeton University) Sharad Malik (Princeton University) Solving Quantified Boolean Formulas with Circuit Observability Don't Cares Traditionally the propositional part of a Quantified Boolean Formula (QBF) instance has been represented using a conjunctive normal form (CNF). As with propositional satisfiability (SAT), this is motivated by the efficiency of this data structure. However, in many cases, part of or the entire propositional part of a QBF instance can often be represented as a combinational logic circuit. In a logic circuit, the limited observability of the internal signals at the circuit outputs may make their assignments irrelevant for specific assignments of values to the outputs. This circuit observability don’t care (ODC) information has been used to advantage in circuit based SAT solvers. A CNF encoding of the circuit, however, does not capture the signal direction and this limited observability, and thus cannot directly take advantage of this. However, recently it has been shown that this don’t care information can be encoded in the CNF description and taken advantage of in a DPLL based SAT solver by modifying the decision heuristics/Boolean constraint propagation/conflict driven learning to account for these don’t cares. Thus far however the use of these don’t cares in the CNF encoding has not been explored for QBF solvers. In this paper, we examine how this can be done for QBF solvers as well as evaluate its practical benefits of this through experimentation. We implemented the usage of circuit ODCs in various parts of the DPLL-based procedure of the Quaffle QBF solver. We show that DPLL search based QBF solvers can use circuit ODC information to detect satisfying branches earlier during search and make satisfiability directed learning more effective. Our experiments demonstrate that significant performance gain can be obtained by considering circuit ODCs in evaluating the satisfiability of QBFs.
12:00‑12:30	Ashish Sabharwal (Cornell University) Carlos Ansotegui (Artificial Intelligence Research Institute (IIIA-CSIC)) Carla P. Gomes (Cornell University) Justin W. Hart (Cornell University) Bart Selman (Cornell University) QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency Quantified Boolean Formulas (QBFs) present the next big challenge for automated propositional reasoning. Not surprisingly, most of the present day QBF solvers are extensions of successful propositional satisfiability algorithms (SAT solvers). They directly integrate the lessons learned from SAT research, thus avoiding re-inventing the wheel. In particular, they use the standard conjunctive normal form (CNF) augmented with layers of variable quantification for modeling tasks as QBF. We argue that while CNF is well suited to "existential reasoning" as demonstrated by the success of modern SAT solvers, it is far from ideal for "universal reasoning" needed by QBF. The CNF restriction imposes an inherent asymmetry in QBF and artificially creates issues that have led to complex solutions, which, in retrospect, were unnecessary and sub-optimal. We take a step back and propose a new approach to QBF modeling based on a game-theoretic view of problems and on a dual CNF-DNF (disjunctive normal form) representation that treats the existential and universal parts of a problem symmetrically. It has several advantages: (1) it is generic, compact, and simpler, (2) unlike fully non-clausal encodings, it preserves the benefits of pure CNF and leverages the support for DNF already present in many QBF solvers, (3) it doesn't use the so-called indicator variables for conversion into CNF, thus circumventing the associated illegal search space issue, and (4) our QBF solver based on the dual encoding (Duaffle) consistently outperforms the best solvers by two orders of magnitude on a hard class of benchmarks, even without using standard learning techniques.

Lunch break (12:30‑14:00)

Session 9: Counting and Concurrency (14:00‑15:30)
Chair: Ashish Sabharwal

14:00‑14:30	Naomi Nishimura (University of Waterloo) Prabhakar Ragde (University of Waterloo) Stefan Szeider (Durham University) Solving #SAT using Vertex Covers We propose an exact algorithm for counting the models of propositional formulas in conjunctive normal form (CNF). Our algorithm is based on the detection of strong backdoor sets of bounded size; each instantiation of the variables of a strong backdoor set puts the given formula into a class of formulas for which models can be counted in polynomial time. For the backdoor set detection we utilize an efficient vertex cover algorithm applied to a certain "obstruction graph" that we associate with the given formula. This approach gives rise to a new hardness index for formulas, the clustering-width. Our algorithm runs in uniform polynomial time on formulas with bounded clustering-width. It is known that the number of models of formulas with bounded clique-width, bounded treewidth, or bounded branchwidth can be computed in polynomial time; these graph parameters are applied to formulas via certain (hyper)graphs associated with formulas. We show that clustering-width and the other mentioned parameters are incomparable: there are formulas with bounded clustering-width and arbitrarily large clique-width, treewidth, and branchwidth. Conversely, there are formulas with arbitrarily large clustering-width and bounded clique-width, treewidth, and branchwidth.
14:30‑15:00	António Morgado (IST-INESC-ID, Technical University of Lisbon) Paulo Matos (IST-INESC-ID, Technical University of Lisbon) Vasco Manquinho (IST / INESC-ID, Technical University of Lisbon) Joao Marques-Silva (University of Southampton) Counting Models in Integer Domains This paper addresses the problem of counting models in integer linear programming (ILP) using Boolean Satisfiability (SAT) techniques, and proposes two approaches to solve this problem. The first approach consists of encoding ILP instances into pseudo-Boolean (PB) instances. Moreover, the paper introduces a model counter for PB constraints, which can be used for counting models in PB as well as in ILP. A second alternative approach consists of encoding instances of ILP into instances of SAT. A two-step procedure is proposed, consisting of first mapping the ILP instance into PB constraints and then encoding the PB constraints into SAT. One key observation is that not all existing PB to SAT encodings can be used for counting models. The paper provides conditions for PB to SAT encodings that can be safely used for model counting, and proves that some of the existing encodings are safe for model counting while others are not. Finally, the paper provides results, comparing the PB and SAT approaches, as well as existing alternative solutions.
15:00‑15:15	Marc Thurley (Humboldt Universität zu Berlin) sharpSAT - counting models with advanced component caching and implicit BCP We introduce sharpSAT, a new #SAT solver that is based on the well known DPLL algorithm and techniques from SAT and #SAT solvers. Most importantly, we introduce an entirely new approach of coding components, which reduces the cache size by at least one order of magnitude, and a new cache management scheme. Furthermore, we apply a well known look ahead based on BCP in a manner that is well suited for #SAT solving. We show that these techniques are highly beneficial, especially on large structured instances, such that our solver performs significantly better than other #SAT solvers.
15:15‑15:30	Antti Eero Johannes Hyvärinen (Helsinki University of Technology) Tommi Junttila (Helsinki University of Technology) Ilkka Niemelä (Helsinki University of Technology) A Distribution Method for Solving SAT in Grids The emerging large-scale computational grid infrastructure is providing an interesting platform for massive distributed computations. In this paper a novel distribution method called scattering is introduced for solving SAT problem instances in grid environments. The key advantages of scattering are that it can be used in conjunction with any sequential SAT solver (including industrial black box solvers), the distribution heuristic is strictly separated from the heuristic used in sequential solving, and it requires no communication between processes solving subproblems but still allows coordination of such processes. An implementation of the method has been developed for NorduGrid, a large widely distributed production-level grid running in Scandinavia.

Break (15:30‑16:00)

Poster Session (16:00‑18:00)