Fra SMT – A tool for computing the fractional hypertree width of hypergraphs Bounded fractional hypertree width (fhtw) is the most general known structural property that guarantees polynomial-time solvability of the constraint satisfaction problem. Bounded fhtw generalizes other structural properties like bounded induced width and bounded hypertree width. Fra SMT is the first practical algorithm for computing the fhtw and its associated structural decomposition. Fra SMT is based on an efficient encoding of the decomposition problem to SMT (SAT modulo Theory) with Linear Arithmetic as implemented in the SMT solver Z3. The encoding is further

Branch LIS: a tool for computing branch decompositions of graphs and hypergraphs with SAT-based local improvement Various decomposition techniques have proven to be useful for efficient solving of many hard problems, e.g., the #P-complete problem of counting models for a propositional formula, albeit there is an exponential dependency on the width measures that are associated with these decompositions. Therefore, it is of interest to obtain decompositions of small width. There are various exact methods, approximations, and heuristics which allow us to compute the decompositions. The exact methods can be only used for very small problem

Qute: A Dependency Learning QBF Solver Quantified Boolean Formulas, or QBFs, augment propositional formulas with existential and universal quantification over truth values. QBFs can succinctly encode problems arising in areas such as formal verification and synthesis. For instance, if (\phi (X, Y)) specifies a system’s desired input/output behavior (with inputs (X) and outputs (Y)), the QBF (\Phi = \forall X \exists Y \phi (X, Y)) is true if there is a system implementing this specification. In general, the value of a variable (y \in Y) can depend on the values of all variables