For investigations into the structure of MU (minimally unsatisfiable clause-sets or conjunctive normal forms), singular DP-reduction is a fundamental tool, applying DP-reduction F -> DP_v(F) in case variable v occurs in one polarity only once. We consider sDP(F), the set of all results of applying singular DP-reduction to F in MU as long as possible, obtaining non-singular F' in MU with the same deficiency, i.e., delta(F') = delta(F). Our main results are: 1. For all F', F" in sDP(F) we have n(F') = n(F"). 2. If F is saturated (F in SMU), then we have |sDP(F)| = 1. 3. If F is "eventually saturated", that is, sDP(F) <= SMU, then for F', F" in sDP(F) we have F' isomorphic F" (establishing "confluence modulo isomorphism"). The results are obtained by a detailed analysis of singular DP-reduction for F in MU. As an application we obtain that singular DP-reduction for F in MU(2) (i.e., delta(F) = 2) is confluent modulo isomorphism (using the fundamental characterisation of MU(2) by Kleine Buening). The background for these considerations is the general project of the classification of MU in terms of the deficiency.
e7dd9b8ab038b4471a67a5dd48e29199 9c2c8d8a1f4ba122f2e39752fb7ca1a8 We present a new SAT approach, called cube-and-conquer, targeted at reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard SAT-competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because cube-and-conquer is natural to parallelise, it is a competitive alternative for solving SAT problems in parallel. This approach was originally developed for solving hard van-der-Waerden problems, and for these (hard, unsatisfiable) problems the approach is not only very well parallelisable, but outperforms all other (parallel or not) SAT-solvers in terms of total run-time by at least a factor of two.
Considers the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Building 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 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.
First we study the properties of the direct translation (or “encoding”) of generalised clause-sets into boolean clause-sets. 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”.
@InProceedings{Kullmann2009OKlibrary,
author = "Oliver Kullmann",
title = "The \texttt{OKlibrary}: Introducing a "Holistic" Research Platform for (Generalised) {SAT} Solving",
journal = "Studies in Logic",
year = 2009,
volume = 2,
number = 1,
pages = "20-53"
}
The OKlibrary is introduced, an open-source library supporting research and development in the area of (generalised) SAT-solving, and available at http://www.ok-sat-library.org. We discuss history, motivation and architecture of the library, and outline its current extent. The differences to existing platforms are explained: We understand the approach of the OKlibrary as “holistic”, so that the OKlibrary includes for example not only program code, but also research plans and methods for processing and evaluation of experiments (as well as experimental results themselves). This leads to the understanding of the OKlibrary as an “IRE”, an “integrated research environment” (however not building a single monolithic block, but based on the Unix/Linux tradition of a “tool chest”). “Generalised satisfiability problems” are understood as a generalisation of SAT towards CSP, and we discuss the basic ideas. To conclude we state 10 research problems which we regard as fundamental for advancing core SAT solving.
6a557631cc862ae37234b61fa1c5859a).
08ac2e185acf8e88efb543f06e490820).
bcb90d78125aa8ccfaf040c32bc6e3b2
2797db71bd07bce630b177b3292a7731
376881cf129946dfa04e770732bdbda7
Capturing propositional logic, constraint satisfaction problems and systems of polynomial equations, we introduce the notion of "systems with finite instantiation by partial assignments", fipa-systems for short, which are independent of special representations of problem instances, but which are based on an axiomatic approach with instantiation (or substitution) by partial assignments as the fundamental notion. Fipa-systems seem to constitute the most general framework allowing for a theory of resolution with non-trivial upper and lower bounds. For every fipa-system we generalise relativised hierarchies originating from generalised Horn formulas, and obtain hierarchies of problem instances with recognition and satisfiability decision in polynomial time and linear space, quasi-automatising relativised and generalised tree resolution and utilising a general "quasi-tight" lower bound for tree resolution. And generalising width-restricted resolution, for every fipa-system a (stronger) family of hierarchies of unsatisfiable instances with polynomial time recognition is introduced, weakly automatising relativised and generalised full resolution and utilising a general lower bound for full resolution. Key words: satisfiability problem (SAT), systems with instantiation, propositional logic, constraint satisfaction problems, polynomial time hierarchies, generalised resolution, lower bounds for resolution, upper bounds for SAT algorithms, automatisation of proof systems, generalised input resolution, generalised width restricted resolution, induced width of constraint satisfaction problems
99d4f3760e87da6e5288240e37eaec2c
Motivated by improved SAT algorithms (see below ), a natural parameterized generalization GER of Extended Resolution (ER) is introduced. GER allows, as ER, the introduction of new clauses, namely blocked clauses. ER can polynomially simulate GER, but GER allows special cases for which exponential lower bounds can be proven. An example is the addition of blocked clauses without new variables and of bounded width (length):
8d06f2fe856f2f2f344b3d52c5f516f8
We prove the worst-case upper bound 1.5045^n for the time complexity of 3-SAT decision in the number n of variables, introducing new methods for the analysis as well as new algorithmic techniques. We add new 3- and 3-clauses, called "blocked clauses", generalising the extension rule of "Extended Resolution". Our methods for estimating the size of trees lead to a refined measure of formula complexity of 3-clause-sets and can be applied also to arbitrary trees.
@InProceedings{Kullmann19963SAT,
author = "Oliver Kullmann",
title = "Worst-case Analysis, {3-SAT} Decision and Lower Bounds: Approaches for Improved {SAT} Algorithms",
pages = "261-313",
crossref = "Dimacs1996SAT"
}
@Proceedings{Dimacs1996SAT,
title = "Satisfiability Problem: Theory and Applications (DIMACS Workshop March 11-13, 1996)",
year = 1997,
editor = "Dingzhu Du and Jun Gu and Panos M. Pardalos",
volume = 35,
series = "DIMACS Series in Discrete Mathematics and Theoretical Computer Science",
publisher = "American Mathematical Society",
note = "ISBN 0-8218-0479-0"
}
e1570afa635bfd67d2c51a853bdac763
New methods for worst-case analysis and (3-)SAT decision are presented. The focus is on the central ideas leading to the improved bound 1.5045^n for 3-SAT decision (n is the number of variables). The implications for SAT decisions in general are discussed and elucidated by a number of hypothesis'. In addition an exponential lower bound for a general class of SAT-algorithms is given, and the only possibilities to remain below this bound are pointed out.
We consider the question of the existence of variables with few occurrences in boolean conjunctive normal forms (clause-sets). Let mvd(F) for a clause-set F denote the minimal variable-degree. Our main result is an upper bound mvd(F ) ≤ nM(sigma(F)) ≤ sigma(F) + 1 + lg(sigma(F)) for lean clause-sets F in dependency on the surplus sigma(F). Lean clause-sets, defined as having no non-trivial autarkies, generalise minimally unsatisfiable clause-sets. For the surplus we have sigma(F) ≤ delta(F) = c(F)−n(F), using the deficiency delta(F) of clause-sets, the difference between the number of clauses and the number of variables. nM(k) is the k-th “non-Mersenne” number, skipping in the sequence of natural numbers all numbers of the form 2^n − 1. As an application of the upper bound we obtain that clause-sets F violating mvd(F) ≤ nM(sigma(F)) must have a non-trivial autarky. It is open whether such an autarky can be found in polynomial time.
d47c9f44aeb637055c5dfdc82f91b567). Problems from exact Ramsey theory are used as test problems for SAT solving. Based on Green-Tao's theorem , the Green-Tao numbers are introduced. Directions of the parameter space are investigated, where these numbers only grow linearly. Using standard SAT solvers the basic Green-Tao numbers are computed. For handling the non-boolean cases, the generic translation scheme is introduced, offering an infinite variety of translations ("encodings") of hypergraph colouring problems to boolean SAT.
c619a62a69ff3b0fd4061630c653f9e7). We study complement-invariant clause-sets F (closed under elementwise complementation of clauses). The reduced deficiency of a clause-set F is defined as delta_r(F) := 1/2 (delta(F) - n(F)), where delta(F) = c(F) - n(F) is the deficiency. The maximal reduced deficiency is delta_r^*(F), the maximum of delta_r(F') over all sub-clause-sets F'. If F is complement-invariant and linearly lean, then we have delta_r^*(F) = delta_r(F). We show polynomial time SAT decision for complement-invariant clause-sets F with delta_r^*(F) = 0, exploiting the (non-trivial) decision algorithm for sign-non-singular matrices given by [Roberton, Seymour, Thomas, 1999]. Minimally unsatisfiable complement-invariant clause-sets fulfil delta_r(F) >= 0, and we immediately get polynomial time decidability of minimally unsatisfiable complement-invariant clause-sets F with delta_r(F) = 0, but we can give also more direct algorithms and characterisations.
8bac4420089d1f811b21d4140986d660). cb1f401d892c65008f2b44089c5a9316
f8c2b8eb758b7fb55236f4b4bec4e8bf
b8cb7ff810c8fa9c26ced030858d8c67
We consider the deficiency delta(F) = c(F) - n(F) and the maximal deficiency delta^*(F), the maximum of delta(F') for all sub-clause-sets F' of F. Here c(F) is the number of clauses, 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 delta^*(F) <= k, where k is considered to be 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). Of basic importance here is the transversal matroid of the bipartite clause-variable graph of the clause-set. Regarding resolution, a fundamental tool is singular DP-reduction. Also an elegant characterisation of MU(1) and SMU(1) is given (minimally unsatisfiable and saturated minimally unsatisfiable clause-sets of deficiency 1).
ebaf0a33de6ee3fd8e1ecad6bbcac911 "Search trees", "branching trees", "backtracking trees" or "enumeration trees" are at the heart of many (complete) approaches towards hard combinatorial problems, constraint problems, and SAT problems. Given many choices for branching, the fundamental question is how to guide the choices so that the resulting trees are (relatively) small. In this chapter the first systematic treatment is given, and a general theory of heuristics guiding the construction of "branching trees" is developed.
502b45ddb5d9bc63c697bf66287a4389 Minimal unsatisfiability describes the reduced kernel of unsatisfiable formulas. The investigation of this property is very helpful in understanding the reasons for unsatisfiability as well as the behaviour of SAT-solvers and proof calculi. The study of minimal unsatisfiability is the study of the structure of problem instances without redundancies. The study of autarkies considers the redundancies themselves, in various guises related to partial assignments which satisfy some part of the problem instance while leaving the rest "untouched". Autarky theory creates many bridges to combinatorics, algebra and logic, and the second part of this chapter provides a solid foundation of the basic ideas and results of autarky theory
f960ac813a6a46d55f73dc5c41d206e9 SAT solving has become an important tool to solve search problems for example from the verification domain, combinatorics, or for cryptanalysis. An obvious problem is the translation into CNF (conjunctive normal form): how to get a good translation? We try to initiate a theory of "good SAT representations", as a kind of "knowledge representation for SAT solvers". Currently, we concentrate on translations of general building blocks, which could be for example some types of constraints (for example cardinality constraints) or components like the S-box in cryptographic ciphers. The first theory-tool available is the notion of "hardness" hd(F), which measures in a certain sense how hard it is for a SAT solver to retrieve information from the representation F of a boolean function f. The talk presents this notion of "hardness", how it fits into the landscape of "representations", and how to generalise this approach.
aaee93b1297a5ed136cee58c59fdccb2 Two areas, where SAT solving and proof complexity should be able to fertilise each other:
fcda95641f82c6f6e868e4926a9f69a5 Presenting an approach towards good representations of boolean functions, based on an algorithmic measurement of the "hardness" of a clause-set F according to the hardness of deriving all consequences from F by tree-resolution.
d6da245a123e7a434958e84f2b58c80a Two topics in the area of SAT-translations are treated in this talk: Translating a non-boolean CNF (with non-boolean variables) into a boolean CNF, via the generic translation. And translating boolean functions (as black boxes) into CNFs, employing the notion of hardness.
Based on the theory of hardness hd(F) for clause-sets F (introduced here and further developed here), we develop a systematic approach towards classes interesting for the area of knowledge compilation for the clausal entailment problem, as well as towards providing "soft" ("good") target classes for SAT translation. The class of unit-refutation complete clause-sets was introduced in 1994, and is denoted here by UC_1. It turns out to be exactly the class of clause-sets of hardness at most 1. Thus we obtain a natural generalisation UC_k of classes of clause-sets which are "unit-refutation complete of level k". Utilising the strong connections to (tree-)resolution complexity and (nested) input resolution, we develop fundamental methods for determination of hardness (the level k in UC_k). UC_1 also turns out to be precisely the class SLUR (Single Lookahead Unit Resolution) introduced in 1995. A natural hierarchy SLUR_k based on SLUR is derived, and we show SLUR_k = UC_k, offering an alternative interpretation of UC_k. Finally we consider the problem of "irredundant" clause-sets in UC_k. For 2-CNF we show that strong minimisations are possible in polynomial time, while already for (very special) Horn clause-sets minimisation is NP-complete. We conclude with a discussion of open problems and future directions.
We present results and conjectures on the van der Waerden numbers w(2;3,t). We have computed the new number w(2;3,19) = 349, and we provide lower bounds for 20 <= t <= 39, where for t <= 30 we conjecture these lower bounds to be exact. We also investigate regularities in the good partitions (certificates) to better understand the lower bounds. We introduce palindromic van der Waerden numbers w^pd(k; t_0,...,t_{k-1}), defined as ordinary van der Waerden numbers w(k; t_0,...,t_{k-1}) however only allowing palindromic solutions (good partitions), defined as reading the same from both ends. All computations are based on SAT solving, and we discuss the various relations between SAT solving and Ramsey theory.
6e5be672e3bffbc9bc7ae31f5183df2d
@Unpublished{KullmannLuckhardt1997Taut,
author = "Oliver Kullmann and Horst Luckhardt",
title = "Deciding propositional tautologies: Algorithms and their complexity",
note = "Preprint, 82 pages; the ps-file can be obtained at \url{http://cs.swan.ac.uk/~csoliver/Artikel/tg.ps}",
year = 1997,
month = "January"
}
d84226a7dfe6baf5d1d8ba8dd97721d4
@Unpublished{KullmannLuckhardt1999Taut,
author = "Oliver Kullmann and Horst Luckhardt",
title = "Algorithms for {SAT}/{TAUT} decision based on various measures",
note = "Preprint, 71 pages; the ps-file can be obtained from \url{http://cs.swan.ac.uk/~csoliver/Artikel/TAUT.ps}",
year = 1999,
month = "February"
}
62cbcb850852110a94a0eec908895167 6a18f0e914421236e177258a9d0576a5 Please see here for the status of the open problems given at the end of the report.