Arrow Research search

Author name cluster

Friedrich Slivovsky

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

28 papers
2 author rows

Possible papers

28

AAAI Conference 2026 Conference Paper

Model Counting for Dependency Quantified Boolean Formulas

  • Long-Hin Fung
  • Che Cheng
  • Jie-Hong Roland Jiang
  • Friedrich Slivovsky
  • Tony Tan

Dependency Quantified Boolean Formulas (DQBF) generalize QBF by explicitly specifying which universal variables each existential variable depends on, instead of relying on a linear quantifier order. The satisfiability problem of DQBF is NEXP-complete, and many hard problems can be succinctly encoded as DQBF. Recent work has revealed a strong analogy between DQBF and SAT: k-DQBF (with k existential variables) is a succinct form of k-SAT, and satisfiability is NEXP-complete for 3-DQBF but PSPACE-complete for 2-DQBF, mirroring the complexity gap between 3-SAT (NP-complete) and 2-SAT (NL-complete). Motivated by this analogy, we study the model counting problem for DQBF, denoted #DQBF. Our main theoretical result is that #2-DQBF is #EXP-complete, where #EXP is the exponential-time analogue of #P. This parallels Valiant's classical theorem stating that #2-SAT is #P-complete. As a direct application, we show that first-order model counting (FOMC) remains #EXP-complete even when restricted to a PSPACE-decidable fragment of first-order logic and domain size two. Building on recent successes in reducing 2-DQBF satisfiability to symbolic model checking, we develop a dedicated 2-DQBF model counter. Using a diverse set of crafted instances, we experimentally evaluated it against a baseline that expands 2-DQBF formulas into propositional formulas and applies propositional model counting. While the baseline worked well when each existential variable depends on few variables, our implementation scaled significantly better to larger dependency sets.

PDF Details DOI

SAT Conference 2025 Conference Paper

Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas

  • Che Cheng
  • Long-Hin Fung
  • Jie-Hong Roland Jiang
  • Friedrich Slivovsky
  • Tony Tan

Dependency Quantified Boolean Formulas (DQBF) extend Quantified Boolean Formulas by allowing each existential variable to depend on an explicitly specified subset of the universal variables. The satisfiability problem for DQBF is NEXP-complete in general, with only a few tractable fragments known to date. We investigate the complexity of DQBF with k existential variables (k-DQBF) under structural restrictions on the matrix - specifically, when it is in Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF) - as well as under constraints on the dependency sets. For DNF matrices, we obtain a clear classification: 2-DQBF is PSPACE-complete, while 3-DQBF is NEXP-hard, even with disjoint dependencies. For CNF matrices, the picture is more nuanced: we show that the complexity of k-DQBF ranges from NL-complete for 2-DQBF with disjoint dependencies to NEXP-complete for 6-DQBF with arbitrary dependencies.

Details

SAT Conference 2024 Conference Paper

eSLIM: Circuit Minimization with SAT Based Local Improvement

  • Franz-Xaver Reichl
  • Friedrich Slivovsky
  • Stefan Szeider

eSLIM is a tool for circuit minimization that utilizes Exact Synthesis and the SAT-based local improvement method (SLIM) to locally improve circuits. eSLIM improves upon the earlier prototype CIOPS that uses Quantified Boolean Formulas (QBF) to succinctly encode resynthesis of multi-output subcircuits subject to don't cares. This paper describes two improvements. First, it presents a purely propositional encoding based on a Boolean relation characterizing the input-output behavior of the subcircuit under don't cares. This allows the use of a SAT solver for resynthesis, substantially reducing running times when applied to functions from the IWLS 2023 competition, where eSLIM placed second. Second, it proposes circuit partitioning techniques in which don't cares for a subcircuit are captured only with respect to an enclosing window, rather than the entire circuit. Circuit partitioning trades completeness for efficiency, and successfully enables the application of exact synthesis to some of the largest circuits in the EPFL suite, leading to improvements over the current best implementation for several instances.

Details

AAAI Conference 2024 Conference Paper

Hardness of Random Reordered Encodings of Parity for Resolution and CDCL

  • Leroy Chew
  • Alexis de Colnet
  • Friedrich Slivovsky
  • Stefan Szeider

Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showing that they require exponential resolution refutations with high probability when the variable order is chosen at random. We obtain this result by proving that these formulas, which are known to be Tseitin formulas, have Tseitin graphs of linear treewidth with high probability. Since such Tseitin formulas require exponential resolution refutations, our result follows. We generalize this argument to a new class of formulas that capture a basic form of parity reasoning involving a sum of two random parity constraints with random orders. Even when the variable order for the sum is chosen favorably, these formulas remain hard for resolution. In contrast, we prove that they have short DRAT refutations. We show experimentally that the running time of CDCL SAT solvers on both classes of formulas grows exponentially with their treewidth.

PDF Details DOI

SAT Conference 2024 Conference Paper

Strategy Extraction by Interpolation

  • Friedrich Slivovsky

In applications, QBF solvers are often required to generate strategies. This typically involves a process known as strategy extraction, where a Boolean circuit encoding a strategy is computed from a proof. It has previously been observed that Craig interpolation in propositional logic can be seen as a special case of QBF strategy extraction. In this paper we explore this connection further and show that, conversely, any strategy for a false QBF corresponds to a sequence of interpolants in its complete (Herbrand) expansion. Inspired by this correspondence, we present a new strategy extraction algorithm for the expansion-based proof system Exp+Res. Its asymptotic running time matches the best known bound of O(mn) for a proof with m lines and n universally quantified variables. We report on experiments comparing this algorithm with a strategy extraction algorithm based on combining partial strategies, as well as with round-based strategy extraction.

Details

AAAI Conference 2023 Conference Paper

Circuit Minimization with QBF-Based Exact Synthesis

  • Franz-Xaver Reichl
  • Friedrich Slivovsky
  • Stefan Szeider

This paper presents a rewriting method for Boolean circuits that minimizes small subcircuits with exact synthesis. Individual synthesis tasks are encoded as Quantified Boolean Formulas (QBFs) that capture the full flexibility for implementing multi-output subcircuits. This is in contrast to SAT-based resynthesis, where "don't cares" are computed for an individual gate, and replacements are confined to the circuitry used exclusively by that gate. An implementation of our method achieved substantial size reductions compared to state-of-the-art methods across a wide range of benchmark circuits.

PDF Details DOI

SAT Conference 2022 Conference Paper

Pedant: A Certifying DQBF Solver

  • Franz-Xaver Reichl
  • Friedrich Slivovsky

Pedant is a solver for Dependency Quantified Boolean Formulas (DQBF) that combines propositional definition extraction with Counterexample-Guided Inductive Synthesis (CEGIS) to compute a model of a given formula. Pedant 2 improves upon an earlier version in several ways. We extend the notion of dependencies by allowing existential variables to depend on other existential variables. This leads to more and smaller definitions, as well as more concise repairs for counterexamples. Additionally, we reduce counterexamples by determining minimal separators in a conflict graph, and use decision tree learning to obtain default functions for undetermined variables. An experimental evaluation on standard benchmarks showed a significant increase in the number of solved instances compared to the previous version of our solver.

Details

SAT Conference 2022 Conference Paper

Quantified CDCL with Universal Resolution

  • Friedrich Slivovsky

Quantified Conflict-Driven Clause Learning (QCDCL) solvers for QBF generate Q-resolution proofs. Pivot variables in Q-resolution must be existentially quantified. Allowing resolution on universally quantified variables leads to a more powerful proof system called QU-resolution, but so far, QBF solvers have used QU-resolution only in very limited ways. We present a new version of QCDCL that generates proofs in QU-resolution by leveraging propositional unit propagation. We detail how conflict analysis must be adapted to handle universal variables assigned by propagation, and show that the procedure is still sound and terminating. We further describe how dependency learning can be incorporated in the algorithm to increase the flexibility of decision heuristics. Experiments with crafted instances and benchmarks from recent QBF evaluations demonstrate the viability of the resulting version of QCDCL.

Details

JAIR Journal 2022 Journal Article

Sum-of-Products with Default Values: Algorithms and Complexity Results

  • Robert Ganian
  • Eun Jung Kim
  • Friedrich Slivovsky
  • Stefan Szeider

Weighted Counting for Constraint Satisfaction with Default Values (#CSPD) is a powerful special case of the sum-of-products problem that admits succinct encodings of #CSP, #SAT, and inference in probabilistic graphical models. We investigate #CSPD under the fundamental parameter of incidence treewidth (i.e., the treewidth of the incidence graph of the constraint hypergraph). We show that if the incidence treewidth is bounded, #CSPD can be solved in polynomial time. More specifically, we show that the problem is fixed-parameter tractable for the combined parameter incidence treewidth, domain size, and support size (the maximum number of non-default tuples in a constraint). This generalizes known results on the fixed-parameter tractability of #CSPD under the combined parameter primal treewidth and domain size. We further prove that the problem is not fixed-parameter tractable if any of the three components is dropped from the parameterization.

PDF Details DOI

SAT Conference 2021 Conference Paper

Certified DQBF Solving by Definition Extraction

  • Franz-Xaver Reichl
  • Friedrich Slivovsky
  • Stefan Szeider

Abstract We propose a new decision procedure for dependency quantified Boolean formulas (DQBFs) that uses interpolation-based definition extraction to compute Skolem functions in a counter-example guided inductive synthesis (CEGIS) loop. In each iteration, a family of candidate Skolem functions is tested for correctness using a SAT solver, which either determines that a model has been found, or returns an assignment of the universal variables as a counterexample. Fixing a counterexample generally involves changing candidates of multiple existential variables with incomparable dependency sets. Our procedure introduces auxiliary variables—which we call arbiter variables —that each represent the value of an existential variable for a particular assignment of its dependency set. Possible repairs are expressed as clauses on these variables, and a SAT solver is invoked to find an assignment that deals with all previously seen counterexamples. Arbiter variables define the values of Skolem functions for assignments where they were previously undefined, and may lead to the detection of further Skolem functions by definition extraction. A key feature of the proposed procedure is that it is certifying by design: for true DQBF, models can be returned at minimal overhead. Towards certification of false formulas, we prove that clauses can be derived in an expansion-based proof system for DQBF. In an experimental evaluation on standard benchmark sets, a prototype implementation was able to match (and in some cases, surpass) the performance of state-of-the-art-solvers. Moreover, models could be extracted and validated for all true instances that were solved.

Details

SAT Conference 2021 Conference Paper

Davis and Putnam Meet Henkin: Solving DQBF with Resolution

  • Joshua Blinkhorn
  • Tomás Peitl
  • Friedrich Slivovsky

Abstract Davis-Putnam resolution is one of the fundamental theoretical decision procedures for both propositional logic and quantified Boolean formulas. Dependency quantified Boolean formulas ( DQBF ) are a generalisation of QBF in which dependencies of variables are listed explicitly rather than being implicit in the order of quantifiers. Since DQBFs can succinctly encode synthesis problems that ask for Boolean functions matching a given specification, efficient DQBF solvers have a wide range of potential applications. We present a new decision procedure for DQBF in the style of Davis-Putnam resolution. Based on the merge resolution proof system, it directly constructs partial strategy functions for derived clauses. The procedure requires DQBF in a normal form called H-Form. We prove that the problem of evaluating DQBF in H-Form is NEXP-complete. In fact, we show that any DQBF can be converted into H-Form in linear time.

Details

SAT Conference 2021 Conference Paper

Proof Complexity of Symbolic QBF Reasoning

  • Stefan Mengel
  • Friedrich Slivovsky

Abstract We introduce and investigate symbolic proof systems for Quantified Boolean Formulas (QBF) operating on Ordered Binary Decision Diagrams (OBDDs). These systems capture QBF solvers that perform symbolic quantifier elimination, and as such admit short proofs of formulas of bounded path-width and quantifier complexity. As a consequence, we obtain exponential separations from standard clausal proof systems, specifically (long-distance) QU-Resolution and IR-Calc. We further develop a lower bound technique for symbolic QBF proof systems based on strategy extraction that lifts known lower bounds from communication complexity. This allows us to derive strong lower bounds against symbolic QBF proof systems that are independent of the variable ordering of the underlying OBDDs, and that hold even if the proof system is allowed access to an NP-oracle.

Details

SAT Conference 2020 Conference Paper

A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth

  • Friedrich Slivovsky
  • Stefan Szeider

Abstract The propositional model counting problem (#SAT) is known to be fixed-parameter-tractable (FPT) when parameterized by the width k of a given tree decomposition of the incidence graph. The running time of the fastest known FPT algorithm contains the exponential factor of \(4^k\). We improve this factor to \(2^k\) by utilizing fast algorithms for computing the zeta transform and covering product of functions representing partial model counts, thereby achieving the same running time as FPT algorithms that are parameterized by the less general treewidth of the primal graph. Our new algorithm is asymptotically optimal unless the Strong Exponential Time Hypothesis (SETH) fails.

Details

KR Conference 2020 Conference Paper

Fixed-Parameter Tractability of Dependency QBF with Structural Parameters

  • Robert Ganian
  • Tomáš Peitl
  • Friedrich Slivovsky
  • Stefan Szeider

We study dependency quantified Boolean formulas (DQBF), an extension of QBF in which dependencies of existential variables are listed explicitly rather than being implicit in the order of quantifiers. DQBF evaluation is a canonical NEXPTIME-complete problem, a complexity class containing many prominent problems that arise in Knowledge Representation and Reasoning. One approach for solving such hard problems is to identify and exploit structural properties captured by numerical parameters such that bounding these parameters gives rise to an efficient algorithm. This idea is captured by the notion of fixed-parameter tractability (FPT). We initiate the study of DQBF through the lens of fixed-parameter tractability and show that the evaluation problem becomes FPT under two natural parameterizations: the treewidth of the primal graph of the DQBF instance combined with a restriction on the interactions between the dependency sets, and also the treedepth of the primal graph augmented by edges representing dependency sets.

PDF Details DOI

SAT Conference 2020 Conference Paper

Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness

  • Matthias Schlaipfer
  • Friedrich Slivovsky
  • Georg Weissenbacher
  • Florian Zuleger

Abstract In applications, QBF solvers are expected to not only decide whether a given formula is true or false but also return a solution in the form of a strategy. Determining whether strategies can be efficiently extracted from proof traces generated by QBF solvers is a fundamental research task. Most resolution-based proof systems are known to implicitly support polynomial-time strategy extraction through a simulation of the evaluation game associated with an input formula, but this approach introduces large constant factors and results in unwieldy circuit representations. In this work, we present an explicit polynomial-time strategy extraction algorithm for the \(\forall \hbox {-}\mathsf{Exp}\hbox {+}\mathsf{Res}\) proof system. This system is used by expansion-based solvers that implement counterexample-guided abstraction refinement (CEGAR), currently one of the most effective QBF solving paradigms. Our argument relies on a Curry-Howard style correspondence between strategies and \(\forall \hbox {-}\mathsf{Exp}\hbox {+}\mathsf{Res}\) derivations, where each strategy realizes an invariant obtained from an annotated clause derived in the proof system.

Details

SAT Conference 2020 Conference Paper

Short Q-Resolution Proofs with Homomorphisms

  • Ankit Shukla 0003
  • Friedrich Slivovsky
  • Stefan Szeider

Abstract We introduce new proof systems for quantified Boolean formulas (QBFs) by enhancing Q-resolution systems with rules which exploit local and global symmetries. The rules are based on homomorphisms that admit non-injective mappings between literals. This results in systems that are stronger than Q-resolution with (injective) symmetry rules. We further strengthen the systems by utilizing a dependency system D in a way that surpasses Q( D )-resolution in relative strength.

Details

SAT Conference 2019 Conference Paper

Combining Resolution-Path Dependencies with Dependency Learning

  • Tomás Peitl
  • Friedrich Slivovsky
  • Stefan Szeider

Abstract We present the first practical implementation of the reflexive resolution-path dependency scheme in a QBF solver. Unlike in DepQBF, which uses the less general standard dependency scheme, we do not compute the dependency relation upfront, but instead query relevant dependencies on demand during dependency conflicts, when the solver is about to learn a missing dependency. Thus, our approach is fundamentally tied to dependency learning, and shows that the two techniques for dependency analysis can be fruitfully combined. As a byproduct, we propose a quasilinear-time algorithm to compute all resolution-path dependencies of a given variable. Experimental results on the QBF library confirm the viability of our technique and identify families of formulas where the speedup is particularly promising.

Details

JAIR Journal 2019 Journal Article

Dependency Learning for QBF

  • Tomáš Peitl
  • Friedrich Slivovsky
  • Stefan Szeider

Quantified Boolean Formulas (QBFs) can be used to succinctly encode problems from domains such as formal verification, planning, and synthesis. One of the main approaches to QBF solving is Quantified Conflict Driven Clause Learning (QCDCL). By default, QCDCL assigns variables in the order of their appearance in the quantifier prefix so as to account for dependencies among variables. Dependency schemes can be used to relax this restriction and exploit independence among variables in certain cases, but only at the cost of nontrivial interferences with the proof system underlying QCDCL. We introduce dependency learning, a new technique for exploiting variable independence within QCDCL that allows solvers to learn variable dependencies on the fly. The resulting version of QCDCL enjoys improved propagation and increased flexibility in choosing variables for branching while retaining ordinary (long-distance) Q-resolution as its underlying proof system. We show that dependency learning can achieve exponential speedups over ordinary QCDCL. Experiments on standard benchmark sets demonstrate the effectiveness of this technique.

PDF Details DOI

SAT Conference 2019 Conference Paper

Proof Complexity of Fragments of Long-Distance Q-Resolution

  • Tomás Peitl
  • Friedrich Slivovsky
  • Stefan Szeider

Abstract Q-resolution is perhaps the most well-studied proof system for Quantified Boolean Formulas (QBFs). Its proof complexity is by now well understood, and several general proof size lower bound techniques have been developed. The situation is quite different for long-distance Q-resolution (LDQ-resolution). While lower bounds on LDQ-resolution proof size have been established for specific families of formulas, we lack semantically grounded lower bound techniques for LDQ-resolution. In this work, we study restrictions of LDQ-resolution. We show that a specific lower bound technique based on bounded-depth strategy extraction does not work even for reductionless Q-resolution by presenting short proofs of the QParity formulas. Reductionless Q-resolution is a variant of LDQ-resolution that admits merging but no universal reduction. We also prove a lower bound on the proof size of the completion principle formulas in reductionless Q-resolution. This shows that two natural fragments of LDQ-resolution are incomparable: Q-resolution, which allows universal reductions but no merging, and reductionless Q-resolution, which allows merging but no universal reductions. Finally, we develop semantically grounded lower bound techniques for fragments of LDQ-resolution, specifically tree-like LDQ-resolution and regular reductionless Q-resolution.

Details

SAT Conference 2018 Conference Paper

Polynomial-Time Validation of QCDCL Certificates

  • Tomás Peitl
  • Friedrich Slivovsky
  • Stefan Szeider

Abstract Quantified Boolean Formulas (QBFs) offer compact encodings of problems arising in areas such as verification and synthesis. These applications require that QBF solvers not only decide whether an input formula is true or false but also output a witnessing certificate, i. e. a representation of the winning strategy. State-of-the-art QBF solvers based on Quantified Conflict-Driven Constraint Learning (QCDCL) can emit Q-resolution proofs, from which in turn such certificates can be extracted. The correctness of a certificate generated in this way is validated by substituting it into the matrix of the input QBF and using a SAT solver to check that the resulting propositional formula (the validation formula ) is unsatisfiable. This final check is often the most time-consuming part of the entire certification workflow. We propose a new validation method that does not require a SAT call and provably runs in polynomial time. It uses the Q-resolution proof from which the given certificate was extracted to directly generate a (propositional) proof of the validation formula in the RUP format, which can be verified by a proof checker such as DRAT-trim. Experiments with a prototype implementation show a robust, albeit modest, increase in the number of successfully validated certificates compared to validation with a SAT solver.

Details

SAT Conference 2017 Conference Paper

Dependency Learning for QBF

  • Tomás Peitl
  • Friedrich Slivovsky
  • Stefan Szeider

Abstract Quantified Boolean Formulas (QBFs) can be used to succinctly encode problems from domains such as formal verification, planning, and synthesis. One of the main approaches to QBF solving is Quantified Conflict Driven Clause Learning (QCDCL). By default, QCDCL assigns variables in the order of their appearance in the quantifier prefix so as to account for dependencies among variables. Dependency schemes can be used to relax this restriction and exploit independence among variables in certain cases, but only at the cost of nontrivial interferences with the proof system underlying QCDCL. We propose a new technique for exploiting variable independence within QCDCL that allows solvers to learn variable dependencies on the fly. The resulting version of QCDCL enjoys improved propagation and increased flexibility in choosing variables for branching while retaining ordinary (long-distance) Q-resolution as its underlying proof system. In experiments on standard benchmark sets, an implementation of this algorithm shows performance comparable to state-of-the-art QBF solvers.

Details

IJCAI Conference 2016 Conference Paper

Knowledge Compilation Meets Communication Complexity

  • Simone Bova
  • Florent Capelli
  • Stefan Mengel
  • Friedrich Slivovsky

Choosing a language for knowledge representation and reasoning involves a trade-off between two competing desiderata: succinctness (the encoding should be small) and tractability (the language should support efficient reasoning algorithms). The area of knowledge compilation is devoted to the systematic study of representation languages along these two dimensions - in particular, it aims to determine the relative succinctness of languages. Showing that one language is more succinct than another typically involves proving a nontrivial lower bound on the encoding size of a carefully chosen function, and the corresponding arguments increase in difficulty with the succinctness of the target language. In this paper, we introduce a general technique for obtaining lower bounds on Decomposable Negation Normal Form (DNNFs), one of the most widely studied and succinct representation languages, by relating the size of DNNFs to multi-partition communication complexity. This allows us to directly translate lower bounds from the communication complexity literature into lower bounds on the size of DNNF representations. We use this approach to prove exponential separations of DNNFs from deterministic DNNFs and of CNF formulas from DNNFs.

PDF Details

SAT Conference 2016 Conference Paper

Long Distance Q-Resolution with Dependency Schemes

  • Tomás Peitl
  • Friedrich Slivovsky
  • Stefan Szeider

Abstract Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers, which use these systems to generate proofs. In this paper, we define a new proof system that combines two such proof systems: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system is sound for the reflexive resolution-path dependency scheme—in fact, we prove that it admits strategy extraction in polynomial time. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q-resolution with universal reduction according to the standard dependency scheme. We report on experiments with a configuration of DepQBF that generates proofs in this system.

Details

TCS Journal 2016 Journal Article

Soundness of Q-resolution with dependency schemes

  • Friedrich Slivovsky
  • Stefan Szeider

Q-resolution and Q-term resolution are proof systems for quantified Boolean formulas (QBFs). We introduce generalizations of these proof systems named Q ( D ) -resolution and Q ( D ) -term resolution. Q ( D ) -resolution and Q ( D ) -term resolution are parameterized by a dependency scheme D and use more powerful ∀-reduction and ∃-reduction rules, respectively. We show soundness of these systems for particular dependency schemes: we prove (1) soundness of Q ( D ) -resolution parameterized by the reflexive resolution-path dependency scheme, and (2) soundness of Q ( D ) -term resolution parameterized by the resolution-path dependency scheme. These results entail soundness of the proof systems used for certificate generation in the state-of-the-art solver DepQBF.

Details DOI

SAT Conference 2015 Conference Paper

On Compiling CNFs into Structured Deterministic DNNFs

  • Simone Bova
  • Florent Capelli
  • Stefan Mengel
  • Friedrich Slivovsky

Abstract We show that the traces of recently introduced dynamic programming algorithms for #SAT can be used to construct structured deterministic DNNF (decomposable negation normal form) representations of propositional formulas in CNF (conjunctive normal form). This allows us prove new upper bounds on the complexity of compiling CNF formulas into structured deterministic DNNFs in terms of parameters such as the treewidth and the clique-width of the incidence graph.

Details

SAT Conference 2014 Conference Paper

Variable Dependencies and Q-Resolution

  • Friedrich Slivovsky
  • Stefan Szeider

Abstract We propose Q ( D )-resolution, a proof system for Quantified Boolean Formulas. Q ( D )-resolution is a generalization of Q-resolution parameterized by a dependency scheme D. This system is motivated by the generalization of the QDPLL algorithm using dependency schemes implemented in the solver DepQBF. We prove soundness of Q ( D )-resolution for a dependency scheme D that is strictly more general than the standard dependency scheme; the latter is currently used by DepQBF. This result is obtained by proving correctness of an algorithm that transforms Q ( D )-resolution refutations into Q-resolution refutations and could be of independent practical interest. We also give an alternative characterization of resolution- path dependencies in terms of directed walks in a formula’s implication graph which admits an algorithmically more advantageous treatment.

Details

MFCS Conference 2013 Conference Paper

Meta-kernelization with Structural Parameters

  • Robert Ganian
  • Friedrich Slivovsky
  • Stefan Szeider

Abstract Meta-kernelization theorems are general results that provide polynomial kernels for large classes of parameterized problems. The known meta-kernelization theorems, in particular the results of Bodlaender et al. (FOCS’09) and of Fomin et al. (FOCS’10), apply to optimization problems parameterized by solution size. We present meta-kernelization theorems that use structural parameters of the input and not the solution size. Let \(\mathcal{C}\) be a graph class. We define the \(\mathcal{C}\) - cover number of a graph to be the smallest number of modules the vertex set can be partitioned into such that each module induces a subgraph that belongs to the class \(\mathcal{C}\). We show that each graph problem that can be expressed in Monadic Second Order (MSO) logic has a polynomial kernel with a linear number of vertices when parameterized by the \(\mathcal{C}\) - cover number for any fixed class \(\mathcal{C}\) of bounded rank-width (or equivalently, of bounded clique-width, or bounded Boolean-width). Many graph problems such as c -Coloring, c -Domatic Number and c -Clique Cover are covered by this meta-kernelization result. Our second result applies to MSO expressible optimization problems, such as Minimum Vertex Cover, Minimum Dominating Set, and Maximum Clique. We show that these problems admit a polynomial annotated kernel with a linear number of vertices.

Details

SAT Conference 2012 Conference Paper

Computing Resolution-Path Dependencies in Linear Time,

  • Friedrich Slivovsky
  • Stefan Szeider

Abstract The alternation of existential and universal quantifiers in a quantified boolean formula (QBF) generates dependencies among variables that must be respected when evaluating the formula. Dependency schemes provide a general framework for representing such dependencies. Since it is generally intractable to determine dependencies exactly, a set of potential dependencies is computed instead, which may include false positives. Among the schemes proposed so far, resolution path dependencies introduce the fewest spurious dependencies. In this work, we describe an algorithm that detects resolution-path dependencies in linear time, resolving a problem posed by Van Gelder (CP 2011).

Details
v2026.09.13