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”.
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
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). 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
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.
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"
}
Please see here for the status of the open problems given at the end of the report.
(compared with CSR 13-2006, the hypergraph applications have been taken out, while the fundamental theory has been revised and completed)