Tascpl: TAS solver for classical propositional logic

Abstract

We briefly overview the most recent improvements we have incorporated to the existent implementations of the TAS methodology, the simplified Δ-tree representation of formulas in negation normal form. This new representation allows for a better description of the reduction strategies, in that considers only those occurrences of literals which are relevant for the satisfiability of the input formula. These reduction strategies are aimed at decreasing the number of required branchings and, therefore, control the size of the search space for the SAT problem.