W O L F G A N G   B L O C H I N G E R  :: 

Parallel SAT Solving

The Boolean satisfiability (SAT) problem consists of determining for a Boolean formula F a variable assignment such that F evaluates to TRUE, resp. to prove that for F no satisfying variable assignment exists. SAT was the first problem shown to be NP complete. Besides this central role in theoretical computer science, SAT solving is also increasingly recognized as a universal tool for tackling hard realworld problems. Prominent examples come from electronic design automation, software-verification, scheduling, and ai planning.

The significant progress of SAT solving techniques achieved in the last decade requires to rethink established approaches for constructing parallel SAT solvers. This research addresses several aspects of parallel SAT solving, especially scalability and robustness in the context of state-of-the-art SAT solving methods.

SAT Solving

The original Davis-Putnam-Logemann-Loveland (DPLL) SAT solving algorithm still serves as algorithmic framework of modern complete SAT solvers. However, it has been significantly enhanced by sophisticated heuristics for pruning the search space of variable assignments to be tested. Basically, the DPLL algorithm is a backtrack search algorithm. Partial variable assignments are stepwise extended, by choosing at each step an unbound variable according to a heuristics (branching rule). Backtracking is performed when a conflict (the formula evaluates to FALSE under the current partial assignment) occurs, undoing variable assignments until the conflict is resolved. This process can be represented by a search tree, where the leaves are either solutions or conflicts. At each inner node of the search tree a procedure called unit-propagation is carried out, inferring additional variable assignments which are logical consequences of the current partial assignment. At each conflict leaf of the search tree, a conflict analysis procedure is invoked, which produces additional knowledge about the problem instance in the form of a so called lemma. A lemma is a clause reflecting the minimal variable assignment which is the ultimate reason of the current conflict. When added to the input formula, a lemma prevents the search process from reproducing this conflict in other regions of the search space and thus can prune the total search space to be treated. This process is called dynamic learning. Since the employed schemes for constructing lemmas are all based on resolution, adding a lemma to the input formula does not affect the correctness of the DPLL algorithm. The clauses of the input formula and lemmas constitute the clause database.

Parallel Search

A common technique for the design of a parallel SAT solving method is exploratory decomposition. With exploratory decomposition, the whole search space of variable assignments that must be checked is split into disjoint sub-spaces which can be treated in parallel. While exploratory decomposition delivers disjoint subproblems, their individual size cannot be predicted, since the effectiveness of the applied heuristics for pruning the search space can differ considerably. This establishes a high degree of irregularity which turned out to be especially pronounced for SAT instances encoding real-world problems. Due to the highly irregular structure of the search space, dynamic problem decomposition (and consequently dynamic task mapping) is required. The parallel search process is implemented using the DOTS multithreading programming model.

Scalable Distributed Dynamic Learning

The dynamic learning process of modern SAT solvers relies on accumulated knowledge which is continuously deduced during the solving process. Employing exploratory decomposition techniques on a distributed memory architecture results in a (partially overlapping) partition of the clause database, consisting of several distributed clause databases. All clause databases comprise the problem clauses and also locally deduced lemmas. Since dynamic learning can considerably prune the search space, it is crucial to exchange lemmas among the different clause databases, establishing a distributed dynamic learning process. This process is orthogonal to the parallelization of the backtracking search (by exploratory decomposition) and specifically addresses the deduction part of modern SAT solving methods. Exchanging lemmas synchronously among the clause databases (for example by an SPMD style all-to-all broadcast operation) causes significant processor idling due to the high irregularity of the solving process. Moreover, the total amount of deduced knowledge increases with the number of processors. Thus, a total exchange approach is highly unscalable. Consequently, for realizing an effective distributed learning process an asynchronous and selective communication method must by employed. We propose a corresponding communication scheme that is based on mobile agents. Every clause database employs a mobile agent which visits otherclause databases for gathering pertinent lemmas. When a mobile agent comes back to its home clause database it delivers new lemmas. At the same time, it gets a description of the current state of the solving process in order to be able to decides which lemmas to scoop up next. For example, lemmas which are permanently subsumed in the context of the current sub-problem are useless and thus need not be brought to the local clause database.

Selected Publications:

• W. Blochinger, C. Sinz, and W. Küchlin. Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Computing, 29(7):969-994, 2003.
• W. Blochinger, W. Westje, W. Küchlin, and S. Wedeniwski. ZetaSAT - Boolean satisfiability solving on desktop grids. In Proc. of the IEEE International Symposium on Cluster Computing and the Grid (CCGrid 2005), Cardiff, UK, 2005.
• W. Blochinger. Towards robustness in parallel SAT solving. In Parallel Computing: Current & Future Issues of High-End Computing (Proc. of the International Conference ParCo 2005), Malaga, Spain, Sept. 2006.