Summary Continuous evolution and improvement of GPGPUs has significantly broadened areas of application. The massively parallel platform they offer, paired with the high efficiency of performing certain operations, opens many questions on the development of suitable techniques and algorithms. In this work, we present a novel algorithm and create a massively parallel, GPGPU‐based solver for enumerating solutions of the N‐Queens problem. We discuss two implementations of our algorithm for GPGPUs and provide insights on the optimizations we applied. We also evaluate the performance of our approach and compare our work to existing literature, showing a clear reduction in computational time.

Abstract We introduce the global conflict graph of DQCNFs (dependency quantified conjunctive normal forms), recording clashes between clauses on such universal variables on which all existential variables depend (called “global variables”). The biclique covers of this graph correspond to the eligible clause-slices of the DQCNF which consider only the global variables. We show that all such slices yield satisfiability-equivalent variations. This opens the possibility to realise this slice using as few global variables as possible. We give basic theoretical results and first supporting experimental data.

Autarkies for SAT are partial assignments for boolean CNF, which either satisfy a clause or leave it untouched. We introduce the natural generalisation of autarkies for DQCNF (dependency-quantified boolean CNF), by generalising constant boolean functions 0, 1, as used in SAT, to arbitrary boolean functions assigned to existential variables, as allowed by the dependency-specification. We regard here DQCNF as a proper generalisation of QCNF (QBF with CNF), and all results naturally apply also to QCNF. We provide the most basic theory, considering confluence of autarky reduction (removing the clauses satisfied by some autarky), and the Autarky Decomposition Theorem, the unique decomposition of a DQCNF into the lean kernel (free from any autarky) and the clauses satisfiable by some autarky. Finding autarkies is NEXPTIME-hard (or PSPACE-hard, when restricting to QCNF), and so autarky systems are introduced, which allow for more feasible restricted notions of autarkies, while maintaining the basic properties. The two most basic autarky systems restrict either the number of existential variables assigned, or the number of universal variables used in the boolean functions assigned.

A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem [Heule et al., 2016], delivering the largest proof yet, of 200 terabytes in size. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, based on integrating the “old” and “new” methods of SAT solving.

We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals are the wellknown “signed literals”, corresponding to unary constraints in CSP. However we argue that only the restricted form of “negative monosigned literals” and the resulting generalised clause-sets, corresponding to “sets of no-goods” in the AI literature, maintain the essential properties of boolean conjunctive normal forms. In this first part of a mini-series of two articles, we build up a solid foundation for (generalised) clause-sets, including the notion of autarky systems, the interplay between autarkies and resolution, and basic notions of (DP-)reductions. As a basic combinatorial parameter of generalised clause-sets we introduce the (generalised) notion of deficiency, which in the boolean case is the difference between the number of clauses and the number of variables. Autarky theory plays a fundamental role here, and we concentrate especially on matching autarkies (based on matching theory). A natural task is to determine the structure of (matching) lean clause-sets, which do not admit non-trivial (matching) autarkies. A central result is the computation of the lean kernel (the largest lean subset) of a (generalised) clause-set in polynomial time for bounded maximal deficiency.

Concluding this mini-series of 2 articles on the foundations of generalised clause-sets, we study the combinatorial properties of non-boolean conjunctive normal forms (clause-sets), allowing arbitrary (but finite) sets of values for variables, while literals express that some variable shall not get some (given) value. First we study the properties of the direct translation (or “encoding”) of generalised clause-sets into boolean clause-sets. Many combinatorial properties are preserved, and as a result we can lift fixed-parameter tractability of satisfiability in the maximal deficiency from the boolean case to the general case. Then we turn to irredundant clause-sets, which generalise minimally unsatisfiable clause-sets, and we prove basic properties. The simplest irredundant clause-sets are hitting clause-sets, and we provide characterisations and generalisations. Unsatisfiable irredundant clause-sets are the minimally unsatisfiable clause-sets, and we provide basic tools. These tools allow us to characterise the minimally unsatisfiable clause-sets of minimal deficiency. Finally we provide a new translation of generalised boolean clause-sets into boolean clause-sets, the nested translation, which preserves the conflict structure. As an application, we can generalise results for boolean clause-sets regarding the hermitian rank/defect, especially the characterisation of unsatisfiable hitting clause-sets where between every two clauses we have exactly one conflict. We conclude with a list of open problems, and a discussion of the “generic translation scheme”.

We consider the deficiency /spl delta/(F):=c(F)-n(F) and the maximal deficiency /spl delta/*(F):=max/sub F'/spl sube/F//sup /spl delta//(F) of a clause-set F (a conjunctive normal form), where c(F) is the number of clauses in F and n(F) is the number of variables. Combining ideas from matching and matroid theory with techniques from the area of resolution refutations, we prove that for clause-sets F with /spl delta/*(F)/spl les/k, where k is considered as a constant, the SAT problem, the minimally unsatisfiability problem and the MAXSAT problem are decidable in polynomial time (previously, only poly-time decidability of the minimally unsatisfiability problem was known, and that only for k=1).