Logo des Repositoriums

Auflistung nach Schlagwort "SAT"

1 - 3 von 3
  • Textdokument
    Computing Treewidth with Constraint Programming
    (SKILL 2022, 2022) Voboril, Florentina
    In this paper, we revisit a known SAT encoding for the fundamental combinatorial treewidth problem. Based on this encoding, we rework it within the constraint modeling language MiniZinc. Two MiniZinc encodings for treewidth are created and their performance is compared in an experimental evaluation. A further dimension for comparison is added by choosing between different backbone solvers supported by MiniZinc.
  • Zeitschriftenartikel
    SATPin: Axiom Pinpointing for Lightweight Description Logics Through Incremental SAT
    (KI - Künstliche Intelligenz: Vol. 34, No. 3, 2020) Manthey, Norbert; Peñaloza, Rafael; Rudolph, Sebastian
    One approach to axiom pinpointing (AP) in description logics is its reduction to the enumeration of minimal unsatisfiable subformulas, allowing for the deployment of highly optimized methods from SAT solving. Exploiting the properties of AP, we further optimize incremental SAT solving, resulting in speedups of several orders of magnitude: through persistent incremental solving the solver state is updated lazily when adding clauses or assumptions. This adaptation consistently improves the runtime of the tool by an average factor of 3.8, and a maximum of 38. SATPin , our system, was tested over large biomedical ontologies and performed competitively.
  • Textdokument
    A Survey of Constraint Transformation Methods
    (INFORMATIK 2021, 2021) Löffler, Sven; Becker, Ilja; Kroll, Franz; Hofstedt, Petra
    The solution performance of finite domain (FD) constraint problems can often be improved by either transforming particular constraints or sub-problems into other FD constraints like binary, table or regular membership constraints, or by transformation of the complete FD problem into an equivalent problem but of another domain, e.g. in a SAT problem. Specialized constraint solvers (like binary or SAT solvers) can outperform general constraint solvers for certain problems. However, this comes with high efforts for the transformation and/or other disadvantages such as a restricted set of constraints such specialized solvers can handle or limitations on the variables domains. In this paper we give an overview of CSP and constraint transformations and discuss applicabilibty and advantages and disadvantages of these approaches.