ABSTRACT. We show unconditional parameterized lower bounds in the area of knowledge compilation, more specifically on the size of circuits in decomposable negation normal form (DNNF) that encode CNF-formulas restricted by several graph width measures. In particular we show that

- there are CNF formulas of size $n$ and modular incidence-treewidth $k$ whose smallest DNNF-encoding has size $n^{\Omega(k)}$, and

- there are CNF formulas of size $n$ and incidence-neighborhood diversity $k$ whose smallest DNNF-encoding has size $n^{\Omega(\sqrt{k})}$.

These results complement recent upper bounds for compilation into DNNF and strengthen---quantitatively and qualitatively---known conditional lower bounds for cliquewidth. Moreover, they show that, unlike for many graph problems, the parameters considered here behave significantly differently from treewidth.

ABSTRACT. The solution graph of a Boolean formula on n variables is the subgraph of the hypercube H_n induced by the satisfying assignments of the formula. The structure of solution graphs has been the object of much research in recent years since it is important for the performance of SAT-solving procedures based on local search. Several authors have studied connectivity problems in such graphs focusing on how the structure of the original formula might affect the complexity of the connectivity problems in the solution graph Gopalan2009,Schwerdtfeger2013.

In this paper we study the complexity of the isomorphism problem of solution graphs of Boolean formulas. We investigate how this complexity depends on the formula type, considering for this the classes of formulas introduced in Gopalan2009,Schwerdtfeger2013.

We show that for general formulas the solution graph isomorphism problem can be solved in exponential time while in the cases of 2CNF formulas as well as for CPSS formulas, the problem is in the counting complexity class C_=P, a subclass of PSPACE. We also prove a strong property on the structure of solution graphs of Horn formulas showing that they are just unions of partial cubes.

In addition we give a PSPACE lower bound for the problem on general Boolean functions. We use a recent result on the complexity of testing the number of perfect matchings Curticapean2015 to prove that for 2CNF as well as for CPSS formulas the solution graph isomorphism problem is hard for C_=P under polynomial time many one reductions, thus matching the given upper bound.

ABSTRACT. In this paper, we introduce a notion of backdoors to Reiter's propositional default logic. We consider the problems of backdoor detection as well as backdoor evaluation for various kinds of target classes (cnf, horn, krom, monotone, identity). We show that backdoor detection when parameterised by the size of the backdoor is fixed-parameter tractable for the considered target classes. We investigate backdoor evaluation when parameterised by the size of a given backdoor for various combinations of target classes and show fixed-parameter tractability, para-DeltaP2 membership, or para-NP membership, respectively.

ABSTRACT. Two Boolean functions are NPN equivalent if one can be obtained from the other by negating inputs, permuting inputs, or negating the output. NPN equivalence is an equivalence relation and the number of equivalence classes is significantly smaller than the number of all Boolean functions. This property has been exploited successfully to increase efficiency in various logic synthesis algorithms. Since computing the NPN representative of a Boolean function is not scalable, heuristics have been proposed that do not guarantee to find the representative for all functions. So far, these heuristics have been implemented using the function's truth table representation, and therefore do not scale for functions exceeding 16 variables.

In this paper, we present a symbolic heuristic NPN classification using And-Inverter Graphs and Boolean satisfiability techniques. This allows us to heuristically compute NPN representatives for functions with much larger number of variables; our experiments contain benchmarks with up to 194 variables. A key technique of the symbolic implementation is SAT-based procedure LEXSAT, which finds the lexicographically smallest satisfiable assignment. To our knowledge, LEXSAT has not been used in logic synthesis algorithms.

ABSTRACT. Managing inconsistency in databases is a long-standing challenge. The framework of database repairs provides a principled approach towards coping with inconsistency in databases. Intuitively, a repair of an inconsistent database is a consistent database that differs from the given inconsistent database in a minimal way. Repair checking and consistent query answering are two fundamental algorithmic problems arising in this context. The first of these two problems asks whether, given two databases, one is a repair of the other. The second asks whether, a query is true on every repair of a given inconsistent database.

The aim of this talk is to give an overview of a body of results in this area with emphasis on the computational complexity of repair checking and consistent query answering, including the quest for dichotomy theorems. In addition to presenting open problems, the last part of the talk will include a discussion of the potential use of solvers in developing practical systems for consistent query answering.

ABSTRACT. Over the years the constrained-based method has been successfully applied to a wide range of problems in program analysis, from invariant generation to termination and non-termination proving. Quite often the semantics of the program under study as well as the properties to be generated belong to difference logic, i.e., the fragment of linear arithmetic where atoms are inequalities of the form u - v <= k. However, so far constrained-based techniques have not exploited this fact: in general, Farkas' Lemma is used to produce the constraints over template unknowns, which leads to non-linear SMT problems. Based on classical results of graph theory, in this paper we propose new encodings for generating these constraints when program semantics and templates belong to difference logic. Thanks to this approach, instead of a heavyweight non-linear arithmetic solver, a much cheaper SMT solver for difference logic or linear integer arithmetic can be employed for solving the resulting constraints. We present encouraging experimental results that show the high impact of the proposed techniques on the performance of the VeryMax verification system.

ABSTRACT. The theory of bit-vectors in SMT solvers is very important for many applications due to its ability to faithfully model the behavior of machine instructions. A crucial step in solving bit-vector formulas is the translation from high-level bit-vector terms down to low-level boolean formulas that can be efficiently mapped to CNF clauses and fed into a SAT solver. In this paper, we demonstrate how a combination of program synthesis and machine learning technology can be used to automatically generate code to perform this translation in a way that is tailored to particular problem domains. Using this technique, the paper shows that we can improve upon the basic encoding strategy used by CVC4 (a state of the art SMT solver) and automatically generate variants of the solver tailored to different families of problems represented in the bit-vector benchmark suite from the SMT-COMP 2015 competition.

ABSTRACT. We propose a novel approach to solve quantified boolean formulas with one quantifier alternation (2QBF). The algorithm incrementally adds new constraints to the formula until only one Skolem function remains - or until the absence of a Skolem function is detected. Backtracking is required if the absence of Skolem functions depends on the newly introduced constraints. We present the algorithm in analogy to search based algorithms for SAT and explain how propagation, decisions, and conflict analysis are lifted from values to Skolem functions. We also discuss how the algorithm produces certificates and we experimentally evaluate the algorithm.

ABSTRACT. In a recent work, we introduced an abstraction based algorithm for solving quantified Boolean formulas (QBF) in prenex negation normal form (PNNF) where quantifiers are only allowed in the formula's prefix and negation appears only in front of variables. In this paper, we present a modified algorithm that lifts the restriction on prenex quantifiers. Instead of a linear quantifier prefix, the algorithm handles tree-shaped quantifier hierarchies where different branches can be solved independently. In our implementation, we exploit this property by solving independent branches in parallel. We report on an evaluation of our implementation on a recent case study regarding the synthesis of finite-state controllers from $\omega$-regular specifications.

ABSTRACT. 2QBF is a subset of the general quantified Boolean formulae, limited to only two quantification layers (either $\exists\forall$ or $\forall\exists$). Despite the limitation 2QBF is $\Sigma^p_2$-complete and provides a framework for some industrial applications. CEGAR-based 2QBF solving approach, among others, was shown as dominant. In this work we overview several implementations of the CEGAR based 2QBF solvers, introduce both algorithmic and implementation improvements, and provide experimental comparison both on competition and application benchmarks.