SAT 2016: 19TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
STRUCTSAT 2016 ON MONDAY, JULY 4TH

View: session overviewtalk overviewside by side with other conferences

08:30-09:30 Session 1: Reception desk
Location: Labri Main Entrance
09:30-10:30 Session 3B: Presentations I
Location: Room 4 First floor, building A29
09:30
Using Decomposition-Parameters for QBF: Mind the Prefix!
SPEAKER: Eduard Eiben

ABSTRACT. Similar to the satisfiability (SAT) problem, which can be seen to be the archetypical problem for NP, the quantified Boolean formula problem (QBF) is the archetypical problem for PSPACE. Recently, Atserias and Oliva (2014) showed that, unlike for SAT, many of the well-known decompositional parameters (such as treewidth and pathwidth) do not allow efficient algorithms for QBF. The main reason for this seems to be the lack of awareness of these parameters towards the dependencies between variables of a QBF formula. In this paper we extend the ordinary pathwidth to the QBF-setting by introducing prefix pathwidth, which takes into account the dependencies between variables in a QBF, and show that it leads to an efficient algorithm for QBF. We hope that our approach will help to initiate the study of novel tailor-made decompositional parameters for QBF and thereby help to lift the success of these decompositional parameters from SAT to QBF.

10:00
Pseudo-Industrial Random SAT Generators

ABSTRACT. In this paper, we address the problem of random generation of realistic pseudo-industrial SAT instances. First, we review some existing generators which are based on the notions of scale-free structure and community structure. Then, we propose a new generator based on the notion of \emph{popularity} and \emph{similarity}. This new model generates instances with both scale-free and community structure, solving the drawbacks of the previous generators.

10:30-11:00Coffee Break
11:00-12:30 Session 4C: Presentations II
Location: Room 4 First floor, building A29
11:00
Experiments with CNF Structure and Hardness
SPEAKER: unknown

ABSTRACT. Structural properties of CNF formulas are often suggested as a basis for explaining the large variation in solving hardness or as instance features that could be exploited by solvers. Examples include community structure and tree-width of graphs associated with the formulas. We will describe some findings from an experimental exploration of the relevance of these properties to actual performance of CDCL SAT solvers.

11:30
Structure-based knowledge compilation: the singular case of $\beta$-acyclic formulas

ABSTRACT. We present a compilation algorithm for beta-acyclic formulas into polynomial size decision DNNF. The DNNF constructed by this algorithm are not structured and we present a proof that this cannot be improved by showing that beta-acyclic formulas may have exponential size structured DNNF.

12:00
Minimal unsatisfiability and deficiency: recent developments

ABSTRACT. In my talk I would like to give some insights about recent investigations into the structure of MU, minimally unsatisfiable clause-sets, organised in layers by the deficiency.

12:30-14:00Lunch Break
14:00-15:00 Session 5C: Presentations III
Location: Room 4 First floor, building A29
14:00
CNF Encoding of Cardinality Constraints via Tree-Decomposition
SPEAKER: Yoichi Iwata

ABSTRACT. This is an extended abstract of our ongoing research. We report that the ordering of additions strongly affects the performance of a CNF encoding of cardinality constraints. Then we propose a new encoding that automatically decides a nice ordering by exploiting the underlying graph structure.

14:30
Complexity and Approximability for Parameterized MAXCSPs
SPEAKER: unknown

ABSTRACT. The complexity of various Constraint Satisfaction Problems (CSP) when parameterized by structural measures (such as treewidth or clique-width) is a very well-investigated area. In this paper, we take a fresh look at such questions from the point of view of approximation, considering four standard CSP predicates: AND, OR, PARITY, and MAJORITY. By providing new or tighter hardness results for the satisfiability versions, as well as approximation algorithms for the corresponding maximization problems, we show that already these basic predicates display a diverse set of behaviors, ranging from being FPT to optimize exactly for quite general parameters (PARITY), to being W-hard but well-approximable (OR, MAJORITY) to being W-hard and inapproximable (AND). Our results indicate the interest in posing the question of approximability during the usual investigation of CSP complexity with regards to the landscape of structural parameters.

15:00-15:30Coffee Break
15:30-16:30 Session 6C: Keynote STRUCTSAT

Invited Talk

Location: Room 4 First floor, building A29
15:30
Capturing Structure in SAT and Related Problems

ABSTRACT. Propositional satisfiability (SAT) and related problems (like Model Counting, QBF-SAT, and CSP) are in practise often much easier to solve than suggested by their respective theoretical worst-case complexities. This "friendliness" of the real world is often explained by the presence of some kind of "hidden structure" in practical problem instances. In this talk we will review some mathematical concepts that attempt to capture the structure in problem instances and discuss their virtues and limits. We will focus rather on general questions than on  technical details.

19:30-22:00 Session : Welcome reception
Location: Palais de la bourse