Lukas Kroc

SAT Conference 2010 Conference Paper

An Empirical Study of Optimal Noise and Runtime Distributions in Local Search

• Lukas Kroc
• Ashish Sabharwal
• Bart Selman

Abstract This paper presents a detailed empirical study of local search for Boolean satisfiability (SAT), highlighting several interesting properties, some of which were previously unknown or had only anecdotal evidence. Specifically, we study hard random 3-CNF formulas and provide surprisingly simple analytical fits for the optimal (static) noise level and the runtime at optimal noise, as a function of the clause-to-variable ratio. We also demonstrate, for the first time for local search, a power-law decay in the tail of the runtime distribution in the low noise regime. Finally, we discuss a Markov Chain model capturing this intriguing feature.

IJCAI Conference 2009 Conference Paper

• Lukas Kroc
• Ashish Sabharwal
• Carla P. Gomes
• Bart Selman

Systematic search and local search paradigms for combinatorial problems are generally believed to have complementary strengths. Nevertheless, attempts to combine the power of the two paradigms have had limited success, due in part to the expensive information communication overhead involved. We propose a hybrid strategy based on shared memory, ideally suited for multi-core processor architectures. This method enables continuous information exchange between two solvers without slowing down either of the two. Such a hybrid search strategy is surprisingly effective, leading to substantially better quality solutions to many challenging Maximum Satisfiability (MaxSAT) instances than what the current best exact or heuristic methods yield, and it often achieves this within seconds. This hybrid approach is naturally best suited to MaxSAT instances for which proving unsatisfiability is already hard; otherwise the method falls back to pure local search.

SAT Conference 2009 Conference Paper

Relaxed DPLL Search for MaxSAT

• Lukas Kroc
• Ashish Sabharwal
• Bart Selman

Abstract We propose a new incomplete algorithm for the Maximum Satisfiability (MaxSAT) problem on unweighted Boolean formulas, focused specifically on instances for which proving unsatisfiability is already computationally difficult. For such instances, our approach is often able to identify a small number of what we call “bottleneck” constraints, in time comparable to the time it takes to prove unsatisfiability. These bottleneck constraints can have useful semantic content. Our algorithm uses a relaxation of the standard backtrack search for satisfiability testing (SAT) as a guiding heuristic, followed by a low-noise local search when needed. This allows us to heuristically exploit the power of unit propagation and clause learning. On a test suite consisting of all unsatisfiable industrial instances from SAT Race 2008, our solver, RelaxedMinisat, is the only (MaxSAT) solver capable of identifying a single bottleneck constraint in all but one instance.

NeurIPS Conference 2008 Conference Paper

Counting Solution Clusters in Graph Coloring Problems Using Belief Propagation

• Lukas Kroc
• Ashish Sabharwal
• Bart Selman

We show that an important and computationally challenging solution space feature of the graph coloring problem (COL), namely the number of clusters of solutions, can be accurately estimated by a technique very similar to one for counting the number of solutions. This cluster counting approach can be naturally written in terms of a new factor graph derived from the factor graph representing the COL instance. Using a variant of the Belief Propagation inference framework, we can efficiently approximate cluster counts in random COL problems over a large range of graph densities. We illustrate the algorithm on instances with up to 100, 000 vertices. Moreover, we supply a methodology for computing the number of clus- ters exactly using advanced techniques from the knowledge compilation literature. This methodology scales up to several hundred variables.

AAAI Conference 2008 Short Paper

Loop Calculus for Satisfiability

• Lukas Kroc

Loop Calculus, introduced by Chertkov and Chernyak, is a new technique to incrementally improve approximations computed by Loopy Belief Propagation (LBP), with the ability to eventually make them exact. In this extended abstract, we give a brief overview of this technique, and show its relevance to the AI community. We consider the problem of Boolean Satisfiability (SAT) and use LBP with Loop Calculus corrections to perform probabilistic inference about the problem. In this preliminary work, we focus on identifying the main issues encountered when applying Loop Calculus, and include initial empirical results in the SAT domain.

UAI Conference 2007 Conference Paper

Survey Propagation Revisited

• Lukas Kroc
• Ashish Sabharwal
• Bart Selman

Survey propagation (SP) is an exciting new technique that has been remarkably successful at solving very large hard combinatorial problems, such as determining the satisfiability of Boolean formulas. In a promising attempt at understanding the success of SP, it was recently shown that SP can be viewed as a form of belief propagation, computing marginal probabilities over certain objects called covers of a formula. This explanation was, however, shortly dismissed by experiments suggesting that non-trivial covers simply do not exist for large formulas. In this paper, we show that these experiments were misleading: not only do covers exist for large hard random formulas, SP is surprisingly accurate at computing marginals over these covers despite the existence of many cycles in the formulas. This re-opens a potentially simpler line of reasoning for understanding SP, in contrast to some alternative lines of explanation that have been proposed assuming covers do not exist.