Egly, UweHaller, Leopold2018-01-082018-01-0820102010https://dl.gi.de/handle/20.500.12116/11121We present an extension of the BC tableau, a calculus for determining satisfiability of constrained Boolean circuits. We argue that a satisfiability decision procedure based on the BC tableau can be implemented as a non-clausal DPLL procedure and that therefore, advances to the DPLL framework can be integrated into such a tableau procedure. We present a prototypical implementation of these ideas and evaluate it using a set of benchmark instances. We show that the extensions increase the efficiency of the basic BC tableau considerably and compare the performance of our solver with that of the non-clausal solver NoClause and the CNF-based SAT solver MiniSat.Text/Journal Article1610-1987