ABSTRACT. SAT filters are a novel and compact data structure that can be used to quickly query a word for membership in a fixed set. They have the potential to store more information in a fixed storage limit than a Bloom filter. Constructing a SAT filter requires sampling diverse solutions to randomly constructed constraint satisfaction instances, but there is flexibility in the choice of constraint satisfaction problem. Presented here is a case study of SAT filter construction with a focus on constraint satisfaction problems based on MAX-CUT clauses (Not-all-equal 3-SAT, 2-in-4-SAT, etc.) and frustrated cycles in the Ising model. Solutions are sampled using a D-Wave quantum annealer, and results are measured against classical approaches. The SAT variants studied are of interest in the context of SAT filters, independent of the solvers used.

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 even the clique-width of the incidence graph.

ABSTRACT. In incremental SAT solving, information gained from previous similar instances has so far been limited to learned clauses that are still relevant, and heuristic information such as activity weights and scores. In most settings in which incremental satisfiability is applied, many of the instances along the sequence of formulas being solved are unsatisfiable. We show that in such cases, with a linear-time analysis of the proof, many constants can be assumed for the next instance. The added constants simplify the next instance and consequently accelerate the search.

ABSTRACT. The problem of propositional formula minimization can be traced to the mid of the last century, to the seminal work of Quine and McCluskey, with a large body of work ensuing from this seminal work. Given a set of implicants (or implicates) of a formula, the goal for minimization is to find a smallest set of prime implicants (or implicates) equivalent to the original formula. This paper considers the more general problem of computing a smallest prime representation of a non-clausal propositional formula, which we refer to as formula simplification. Moreover, the paper proposes a novel, entirely SAT-based, approach for the formula simplification problem. The original problem addressed by the Quine-McCluskey procedure can thus be viewed as a special case of the problem addressed in this paper. Experimental results, obtained on well-known representative problem instances, demonstrate that a SAT-based approach for formula simplification is a viable alternative to existing implementations of the Quine-McCluskey procedure.

ABSTRACT. Searching for minimal explanations of infeasibility in constraint sets is a problem known for many years. Recent developments closed a gap between approaches that enumerate all minimal unsatisfiable subsets (MUSes) of an unsatisfiable formula in the Boolean domain and approaches that extract only one single MUS. These new algorithms are described as partial MUS enumerators. They offer a viable option when complete enumeration is not possible within a certain time limit. This paper develops a novel method to identify clauses that are identical regarding their presence or absence in MUSes. With this concept we improve the performance of some of the state-of-the-art partial MUS enumerators using its already established framework. In our approach we focus mainly on determining minimal correction sets much faster to improve the MUS finding subsequently. An extensive practical analysis shows the increased performance of our extensions.

ABSTRACT. The enumeration of minimal unsatisfiable subsets (MUSes) finds a growing number of practical applications, that includes a wide range of diagnosis problems. As a concrete example, the problem of axiom pinpointing in the EL family of description logics (DLs) can be modeled as the enumeration of the group-MUSes of Horn formulae. In turn, axiom pinpointing for the EL family of DLs finds important applications, such as debugging medical ontologies, of which SNOMED CT is the best known example. The main contribution of this paper is to develop an efficient group-MUS enumerator for Horn formulae, HgMUS, that finds immediate application in axiom pinpointing for the EL family of DLs. In the process of developing HgMUS, the paper also identifies performance bottlenecks of existing solutions. The new algorithm is shown to outperform all alternative approaches when the problem domain targeted by group-MUS enumeration of Horn formulae is axiom pinpointing for the EL family of DLs, with a representative suite of examples taken from different medical ontologies.

ABSTRACT. In this paper we present several improvements to extraction of minimal unsatisfiable subformulas (MUSes) of Boolean formulas. As our first contribution we amplify the role of preprocessing for computing group MUSes and describe rotation on preprocessed formulas. We find very convenient to adopt the framework of labeled CNF formulas and we present our algorithms in this more general framework. We use the assumption-based approach for computing MUSes due to its simplicity and the ability to use any SAT-solver as the back-end. However, this comes with a price: it is well-known that the assumption-based approach performs significantly worse than the resolution-based approach. This leads to our second contribution, we show how to bridge the gap between the two approaches using ``chunking''. An extensive experimental evaluation shows that our method significantly outperforms state-of-the-art solutions in the context of group MUS extraction.

ABSTRACT. Knowledge compilation and approximation finds a wide range of practical applications. One relevant task in this area is to compute the Horn least upper bound (Horn LUB) of a propositional theory F. The Horn LUB is the strongest Horn theory entailed by F. This paper studies this problem and proposes two new algorithms that rely on making successive calls to a SAT solver. The algorithms are analyzed theoretically and evaluated empirically. The results show that the proposed methods are complementary and enable computing Horn LUBs for instances with a non-negligible number of variables.

ABSTRACT. Quantified Boolean satisfiability (QSAT) is natural formulation of many decision problems and yet awaits further breakthroughs to reach the maturity enabling industrial applications. Recent advancements on quantified Boolean formula (QBF) proof systems sharpen our understanding of their proof complexities and shed light on solver improvement. Particularly QBF solving based on formula expansion has been theoretically and practically demonstrated to be more powerful than non-expansion based solving. However recursive expansion suffers from exponential formula explosion and has to be carefully managed. In this paper, we propose a QBF solver using levelized SAT solving in the flavor of formula expansion. New learning techniques are devised to control formula growth. Experimental results on application benchmarks show that our prototype implementation is comparable with state-of-the-art solvers and outperforms other solvers in certain instances.

ABSTRACT. For SAT and QBF formulas many techniques are applied in order to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solution algorithm. It is well known that these preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper we generalize different preprocessing techniques for SAT and QBF problems to dependency quantified Boolean formulas (DQBF) and describe how they need to be adapted to work with a DQBF solver core. We demonstrate their effectiveness both for CNF- and non-CNF-based DQBF algorithms.