@Summary Compile formulas to a BDD @Description If a list of formulas is given, the BDD of the conjunction of these formulas is computed.

@Summary Compile formulas to a BDD an return its graphical representation @Description If a list of formulas is given, the BDD of the conjunction of these formulas is computed.

@Summary Compute a Constraint graph of formulas @Description Takes a list of formulas.

@Summary Compute a Constraint graph of formulas as a graphical representation @Description Takes a list of formulas.

@Summary Report whether a formula is a contradiction @Description If a list of formulas is given it is reported of the conjunction of these formulas are a contradiction.

@Summary Compile formulas to DNNF @Description If a list of formulas is given, the DNNF of the conjunction of these formulas is computed.

@Summary Report whether the first formula and the second formula are equivalent @Description Must be called with exactly two formulas.

@Summary Compute clusters of formulas which occurr in the same components of the constraint graph @Description Takes a list of formulas.

@Summary Report whether the first formula implies the second formula @Description Must be called with exactly two formulas.

@Summary Solve a given set of hard and soft formulas with a MAX-SAT solver @Tags Solver @Param algorithm query string false "MAX-SAT Algorithm" Enums(oll, msu3, wmsu3, linear-su, linear-us, wbo, inc-wbo) @Param request body sio.MaxSatInput true "MAX-SAT input" @Success 200 {object} sio.MaxSatResult @Router /solver/maxsat [post].

@Summary Compute a minimal prime implicant of a formula @Description If a list of formulas is given, the prime implicant is computed for the conjunction of these formulas.

@Summary Compute a minimal prime implicant cover of a formula @Description If a list of formulas is given, the prime implicant cover is computed for the conjunction of these formulas.

@Summary Count the satisfying models of a formula @Description If a list of formulas is given, the result refers to the conjunction of these formulas.

@Summary Enumerate the satisfying models of a formula @Description If a list of formulas is given, the result refers to the conjunction of these formulas.

@Summary Compute a minimal unsatisfiable set (MUS) of an unsatisfiable formula @Description If a list of formulas is given, the result refers to the conjunction of these formulas.

@Summary Report whether a formula is an a certain normal form @Description If a list of formulas is given, the predicate is computed for the conjunction of these formulas.

@Summary Count the models of a formula projected to a set of variables @Description If a list of formulas is given, the result refers to the conjunction of these formulas.

@Summary Enumerate the satisfying models of a formula projected to a set of variables @Description If a list of formulas is given, the result refers to the conjunction of these formulas.

@Summary Generate a random formula @Tags Randomizer @Param fsort path string true "Formula sort to generate" Enums(const, var, lit, atom, not, impl, equiv, and, or, cc, amo, exo, pbc, formula) Default(formula) @Param depth query int false "Formula depth" @Param vars query int false "Number of variables" @Param seed query int false "Seed for the randomizer" @Param formulas query int false "Number of formulas to generate" @Success 200 {object} sio.FormulaResult @Router /randomizer/{fsort} [get].

@Summary Compute the satisfiability of a set of formulas with a SAT solver @Description If a list of formulas is given, the satisfiability is computed for the conjunction of these formulas.

@Summary Compute the backbone of a set of formulas @Description If a list of formulas is given, the backbone is computed for the conjunction of these formulas.

@Summary Compute a shortest minimal unsatisfiable set (SMUS) of an unsatisfiable formula @Description If a list of formulas is given, the result refers to the conjunction of these formulas.

@Summary Report whether a formula is a tautology @Description If a list of formulas is given it is reported of the conjunction of these formulas are a tautology.