Logo des Repositoriums

Künstliche Intelligenz 24(1) - März 2010

https://dl.gi.de/handle/20.500.12116/11092
Auflistung nach:

Auflistung Künstliche Intelligenz 24(1) - März 2010 nach Autor:in "Egly, Uwe"

1 - 1 von 1
  • Zeitschriftenartikel
    A SAT Solver for Circuits Based on the Tableau Method
    (KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Egly, Uwe; Haller, Leopold
    We 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.