BattleAx3 - A prover for circuits based on tableau methods

Abstract

BattleAx solves satisfiability problems where the formula is given as a circuit. It is based on a specific variant of tableaux.

Installation

Download the required version of the 32 bit Linux executable (./battleax... -? prints usage)

Decision heuristics
  • BattleAx with BERKMIN heuristics
  • BattleAx with VSIDS heuristics (This solver was used for the KI submission)
    • Restarting schemes
  • geometric
  • geometric + phase saving
  • Luby based
  • Luby based + phase saving
  • nested scheme
  • nested scheme + phase saving
    • Full lookahead
  • BattleAx with lookahead decision heuristic
  • BattleAx with lookahead decision heuristic and justification filtering
    • Restricted lookahead
  • BattleAx with lookahead on the first four VSIDS heap literals
  • BattleAx with lookahead on the first 32 VSIDS heap literals
  • BattleAx with VSIDS decision heuristic on the first four VSIDS heap literals

    • Additional resources

  • Description of the input format and conversion tools (from Helsinki University of Technology)
  • Master thesis of Leopold Haller: Extending a Tableau-based SAT Procedure with Techniques from CNF-based SAT

    • The master thesis describes the theoretical foundations of an extension/refinement of KE tableaux, the implementation of the solver and extensive testing/comparisons with different implementations of BattleAx and the CNF-based solver minisat.

    Feedback

    e-mail to Leopold Haller: "leopoldhaller" + "@" + "gmail.com" or Uwe Egly: "uwe" + "@" + "kr.tuwien.ac.at"

    Last updated on: 10.09.2009 by Uwe Egly