Uwe Schöning

SAT Conference 2014 Conference Paper

Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses

• Adrian Balint
• Armin Biere
• Andreas Fröhlich
• Uwe Schöning

Abstract Stochastic Local Search (SLS) solvers are considered one of the best solving technique for randomly generated problems and more recently also have shown great promise for several types of hard combinatorial problems. Within this work, we provide a thorough analysis of different implementation variants of SLS solvers on random and on hard combinatorial problems. By analyzing existing SLS implementations, we are able to discover new improvements inspired by CDCL solvers, which can speed up the search of all types of SLS solvers. Further, our analysis reveals that the multilevel break values of variables can be easily computed and used within the decision heuristic. By augmenting the probSAT solver with the new heuristic, we are able to reach new state-of-the-art performance on several types of SAT problems, especially on those with long clauses. We further provide a detailed analysis of the clause selection policy used in focused search SLS solvers.

SAT Conference 2012 Conference Paper

Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break

• Adrian Balint
• Uwe Schöning

Abstract Stochastic local search solvers for SAT made a large progress with the introduction of probability distributions like the ones used by the SAT Competition 2011 winners Sparrow2010 and EagleUp. These solvers though used a relatively complex decision heuristic, where probability distributions played a marginal role. In this paper we analyze a pure and simple probability distribution based solver probSAT, which is probably one of the simplest SLS solvers ever presented. We analyze different functions for the probability distribution for selecting the next flip variable with respect to the performance of the solver. Further we also analyze the role of make and break within the definition of these probability distributions and show that the general definition of the score improvement by flipping a variable, as make minus break is questionable. By empirical evaluations we show that the performance of our new algorithm exceeds that of the SAT Competition winners by orders of magnitude.

TCS Journal 2002 Journal Article

A deterministic (2−2/(k+1))n algorithm for k-SAT based on local search

• Evgeny Dantsin
• Andreas Goerdt
• Edward A Hirsch
• Ravi Kannan
• Jon Kleinberg
• Christos Papadimitriou
• Prabhakar Raghavan
• Uwe Schöning

Local search is widely used for solving the propositional satisfiability problem. Papadimitriou (1991) showed that randomized local search solves 2-SAT in polynomial time. Recently, Schöning (1999) proved that a close algorithm for k-SAT takes time (2−2/k) n up to a polynomial factor. This is the best known worst-case upper bound for randomized 3-SAT algorithms (cf. also recent preprint by Schuler et al.). We describe a deterministic local search algorithm for k-SAT running in time (2−2/(k+1)) n up to a polynomial factor. The key point of our algorithm is the use of covering codes instead of random choice of initial assignments. Compared to other “weakly exponential” algorithms, our algorithm is technically quite simple. We also describe an improved version of local search. For 3-SAT the improved algorithm runs in time 1. 481 n up to a polynomial factor. Our bounds are better than all previous bounds for deterministic k-SAT algorithms.

MFCS Conference 2001 Invited Paper

New Algorithms for k -SAT Based on the Local Search Principle

• Uwe Schöning

Abstract Recently, several algorithms for the NP-complete problem k -SAT have been proposed and rigorously analyzed. These algorithms are based on the heuristic principle of local search. Their deterministic and their probabilistic versions and variations, have been shown to achieve the best complexity bounds that are known for k -SAT (or the special case 3-SAT). We review these algorithms, their underlying principles and their analyses.

FOCS Conference 1999 Conference Paper

A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems

• Uwe Schöning

We present a simple probabilistic algorithm for solving k-SAT and more generally, for solving constraint satisfaction problems (CSP). The algorithm follows a simple local search paradigm (S. Minton et al. , 1992): randomly guess an initial assignment and then, guided by those clauses (constraints) that are not satisfied, by successively choosing a random literal from such a clause and flipping the corresponding bit, try to find a satisfying assignment. If no satisfying assignment is found after O(n) steps, start over again. Our analysis shows that for any satisfiable k-CNF-formula with n variables this process has to be repeated only t times, on the average, to find a satisfying assignment, where t is within a polynomial factor of (2(1-1/k))/sup n/. This is the fastest (and also the simplest) algorithm for 3-SAT known up to date. We consider also the more general case of a CSP with n variables, each variable taking at most d values, and constraints of order l, and analyze the complexity of the corresponding (generalized) algorith m. It turns out that any CSP can be solved with complexity at most (d/spl middot/(1-1/l)+/spl epsiv/)/sup n/.

MFCS Conference 1997 Invited Paper

Resolution Proofs, Exponential Bounds, and Kolmogorov Complexity

• Uwe Schöning

Abstract We prove an exponential lower bound for the length of any resolution proof for the same set of clauses as the one used by Urquhart [13]. Our contribution is a significant simplification in the proof and strengthening of the bound, as compared to [13]. We use on the one hand a simplification similar to the one suggested by Beame and Pitassi in [1] for the case of the pidgeon hole clauses. Additionally, we base our construction on a simpler version of expander graphs than the ones used in [13]. These expander graphs are located in the core of the construction. We show the existence of our expanders by a Kolmogorov complexity argument which has not been used before in this context and might be of independent interest since the applicability of this method is quite general.

TCS Journal 1995 Journal Article

If NP has polynomial-size circuits, then MA = AM

• Vikraman Arvind
• Johannes Köbler
• Uwe Schöning
• Rainer Schuler

It is shown that the assumption of NP having polynomial-size circuits implies (apart from a collapse of the polynomial-time hierarchy as shown by Karp and Lipton) that the classes AM and MA of Babai's Arthur-Merlin hierarchy coincide. This means that also a certain inner collapse of the remaining classes of the polynomial-time hierarchy occurs.

TCS Journal 1992 Journal Article

Logarithmic advice classes

• JoséL. Balcázar
• Uwe Schöning

Karp and Lipton (1980) introduced the notion of nonuniform complexity classes where a certain amount of additional information, the advice, is given for free. The advice only depends on the length of the input. Karp and Lipton initiated the study of classes with either logarithmic or polynomial advice; however, later Yap (1983), Schöning (1984), Balcázar (1987) and Ko and Schöning (1985) concentrated on the study of classes of the form C /poly, where C is P, NP, or PSPACE, and poly denotes a polynomial-size advice. This paper considers classes of the form C /log. As a main result it is shown that in the context of an NP/log computation, log-bounded advice is equivalent to a sparse oracle in NP. In contrast, it has been shown that a poly-bounded advice to an arbitrary sparse oracle set. Furthermore, a general theorem is presented that generalizes Karp and Lipton's “round-robin tournament” method.

CSL Conference 1988 Conference Paper

Complexity Cores and Hard-To-Prove Formulas

• Uwe Schöning

Abstract Extending the theory of complexity cores, it is proved, assuming NP ≠ co-NP, that there exist collections of tautologies of exponential density which have only non-polynomially long proofs under every sound proof system.

MFCS Conference 1988 Invited Paper

Robust Orale Machines

• Uwe Schöning

Abstract The notion of a robust oracle machine and an oracle set "helping" a robust oracle machine has been introduced for better understanding the nondeterministic "witness searching" process in NP problems. It is shown that straightforward modifications of the original notion are closely related with other concepts in structural complexity theory, such as "self-reducibility", "lowness", and "interactive proof systems".

TCS Journal 1985 Journal Article

On bounded query machines

• Jose L. Balcázar
• Ronald V. Book
• Uwe Schöning

Simple proofs are given for each of the following results: (a) P = Pspace if and only if, for every set A, P(A) = Pquery(A) (Selman et al. , 1983): (b) NP = Pspace if and only if, for every set A, NP(A) = NPquery(S) (Book, 1981); (c) PH = Pspace if and only if, for every set A, PH(A) = PQH(A) (Book and Wrathall, 1981); (c) PH = Pspace if and only if, for every set set S, PH(S) = PQH(S) = Pspace(S) (Balcázar et al. , 1986; Long and Selman, 1986).

TCS Journal 1985 Journal Article

Robust algorithms: A different approach to oracles

• Uwe Schöning

A new notion of an oracle machine being ‘helped’ by an oracle set is introduced. It is required that the oracle machine is ‘robust’, i. e. , it always computes the same set independent of the oracle. The main result states that the class of sets that can be computed by deterministic polynomial time algorithms being helped by some oracle set is exactly NP ∩ co-NP. Some connections to probabilistic classes are also investigated.

TCS Journal 1984 Journal Article

Minimal pairs for P

• Uwe Schöning

We prove a general minimal pair theorem which yields as corollaries many results about minimal pairs for P obtained previously by various authors. Furthermore, it yields the new counterintuitive result that there exist ‘arbitrarily complex’ minimal pairs. We also investigate the question of whether minimal pairs in NP are ‘low’.

TCS Journal 1984 Journal Article

On small generators

• Uwe Schöning

Yap (1983) shows that each set having small generators is in the class NP/poly which was introduced by Karp and Lipton (1980). We show here that the converse is also true, i. e. , each set in NP/poly has small generators. This settles a question left open by Yap (1983). Further, an argument by Meyer stated in Berman and Hartmanis (1977) is generalized to show that a set has small generators if and only if for some sparse set S, A ϵ NP(S).

FOCS Conference 1984 Conference Paper

Sparse Oracles and Uniform Complexity Classes

• José L. Balcázar
• Ronald V. Book
• Timothy J. Long
• Uwe Schöning
• Alan L. Selman

We show that several questions about the polynomial-time hierarchy can be answered by answering their counterparts for the polynomial-time hierarchy relativized to an arbitrary sparse oracle set. For each of these questions, the answer will be the same for the hierarchy relativized to S/sub 1/ as it will be for the hierarchy relativized to S/sub 2/ for any choice of S/sub 1/ and S/sub 2/ that are sparse sets, including the choice of S/sub 1/ being empty and S/sub 2/ being nonempty but sparse.

MFCS Conference 1984 Conference Paper

Sparse Oracles, Lowness, and Highness

• José L. Balcázar
• Ronald V. Book
• Uwe Schöning

MFCS Conference 1984 Conference Paper

The Structure of Polynomial Complexity Cores (Extended Abstract)

• Pekka Orponen
• Uwe Schöning

TCS Journal 1982 Journal Article

A uniform approach to obtain diagonal sets in complexity classes

• Uwe Schöning

A uniform method for constructing sets which diagonalize over certain complexity classes while preserving other complexity properties is given. We obtain some known results as well as some new ones as corollaries of our main theorem. The new results concern the complexity classes P, NP, co-NP, PSPACE, APT (almost polynomial time), R (random polynomial time), and the polynomial hierarchy.