We will present our experiences with the development of a non-clausal SAT solver called SBSAT - what worked well and what did not and under what conditions. We avoid data structure issues and concentrate on problem solving ideas.
The salient feature of SBSAT is to solve Boolean expressions developed directly in the domain of a user and avoid the translation to CNF because it is believed the exploitable user-domain specific information is often garbled, rendering it useless to a brancher in that case. A secondary feature is, during pre-processing, to memoize all information that can be used to support the development of powerful brancher heuristics with relatively little overhead. Finally, SBSAT introduces the concept of function-complete lookahead which contrasts with the depth-first lookahead strategies of zChaff-like algorithms and the breadth-first lookahead strategies of Prover by providing complete lookahead knowledge for functional segments of a given input expression.
SBSAT uses BDDs to represent functional segments. We have experimented with and invented a few operations on pairs of functional segments that assist in discovering inferred and non-inferred but safe constraints during preprocessing. We have also experimented with the effect of adding non-inferred and unsafe constraints at the start of search and retracting those constraints at some search depth. We have observed remarkable differences in performance when branching favors independent or dependent variables.
We relate these experience in terms of several families of benchmarks we have considered. These include some invented benchmarks, benchmarks associated with finding Van der Waerden bounds, and benchmarks from bounded model checking, in addition to a smattering of others.