ABSTRACT. 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.

ABSTRACT. We introduce Bule, a modeling language for problems from the complexity class PSPACE via quantified Boolean formulas (QBF), that is, propositional formulas in which the variables might be existentially or universally quantified. The language features a natural minimal models semantics and a subsequent grounding based generation of a quantified Boolean formula in conjunctive normal form. This makes Bule easy and intuitive to learn and an ideal language to get started with modeling of PSPACE problems in terms of QBF. We implemented a tool of the same name that provides an interface to aribtrary QBF solvers, so that the modeled problems can also be solved. We analyze the complexity theoretic properties of our modeling language, provide a library for common modeling patterns, and showcase its use on several examples.

ABSTRACT. We present an extension of the OptiLog Python framework. We fully redesign the solvers module to support dynamic loading of incremental SAT solvers with support for external libraries. We introduce new modules for modelling problems into Non-CNF format with support for Pseudo Boolean constraints, for evaluating and parsing the results of applications, and we add support for constrained execution of blackbox programs and SAT-heritage integration. All these enhancements allow OptiLog to become a swiss knife for SAT-based applications in academic and industrial environments.

ABSTRACT. The Merge Resolution proof system (MRes) for QBFs, proposed by Beyersdorff et al. in 2019, explicitly builds partial strategies inside refutations. The original motivation for this approach was to overcome the limitations encountered in long-distance Q-Resolution proof system (LDQRes), where the syntactic side-conditions, while prohibiting all unsound resolutions, also end up prohibiting some sound resolutions. However, while the advantage of MRes over many other resolution-based QBF proof systems was already demonstrated, a comparison with LDQRes itself had remained open. In this paper, we settle this question. We show that MRes has an exponential advantage over not only LDQRes, but even over LQUplusRes and IRM, the most powerful among currently known resolution-based QBF proof systems. Combining this with results from Beyersdorff et al. 2020, we conclude that MRes is incomparable with LQURes and LQUplusRes.

Our proof method reveals two additional and curious features about MRes: (i) MRes is not closed under restrictions, and is hence not a natural proof system, and (ii) weakening axiom clauses with existential variables provably yields an exponential advantage over MRes without weakening. We further show that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over MRes without weakening. These results suggest that MRes is better used with weakening, though whether MRes with weakening is closed under restrictions remains open. We note that even with weakening, MRes continues to be simulated by QBFeFrege (the simulation of ordinary MRes was shown recently by Chew and Slivovsky).

ABSTRACT. The following awards will be presented

SAT Best Paper Awards: 10 minutes

Test of Time Award: 35 minutes

MaxSAT Competition:  20 minutes

The ceremony will be broadcast live at: https://tinyurl.com/sat22awards

ABSTRACT. The results of the following competitions will be announced:

QBF Competition: 20 minutes

MC Competition: 20 mintues

SAT Competition: 30 minutes

The ceremony will be broadcast live at: https://tinyurl.com/sat22awards