• antom
    antom is a C++ library for solving
    • SAT,
    • Unweighted MaxSAT,
    • Partial MaxSAT, and
    • #SAT problems.
    It incorporates many features of modern SAT/MaxSAT/#SAT solving:
    • Various activity-based decision heuristics,
    • Fast unit propagation via watched literals,...

    Welcome to the project site of the Transregional Collaborative Research Center 14 AVACS

    • isat

      iSAT has been developed to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions. The core of iSAT is based on a tight integration of recent DPLL-style SAT solving techniques (like lazy clause evaluation, conflict-driven learning, non-chronological backtracking, and restarts) with interval-based arithmetic constraint solving....

    • isat3

      iSAT3 is a satisfiability checker for Boolean combinations of arithmetic constraints over real- and integer-valued variables. Those constraints may contain linear and non-linear arithmetic as well as transcendental functions. iSAT3 is the third implementation of the iSAT algorithm. All three implementations (with HySAT and iSAT being the first two) share the same major core principles of tightly integrating ICP into the CDCL framework. But while the core solvers of HySAT and iSAT operate on simple bounds, the core of iSAT3 uses literals and additionally utilizes an ASG for more advanced formula preprocessing. iSAT3 understands the same input file format as HySAT and iSAT. So you may use the iSAT example benchmarks as well....

    • sisat

      SiSAT is an extension of the iSAT constraint solver to existential, universal and randomized quantification of finite-domain variables.

      Downloads: SiSAT Linux binaries, SiSAT Manual, SiSAT Examples

  • countAntom

    countAntom [1] is a multi-threaded #SAT solver based on the antom SAT solver.

    The source code and a statically linked binary are available under the files tab.

    Furthermore we provide the following #SAT specific benchmark collection:
    • Fault Injection: Encode the probability of a successful fault injection into a security circuit by clock manipulation [2]....
  • InventoryControl


    Ihr Team wurde von einem namhaften Kaffee-Unternehmen beauftragt, die Logistikkette beginnend mit der Anlieferung der diversen gerösteten Kaffebohnen, deren Unterteilung in die drei Produktgruppen "milder, "normaler" und "starker" Kaffee bis hin zur Auslieferung der eingegangenen Kundenbestellungen auf ein effizientes, vollautomatisches System umzustellen....

  • IEMS SMF 2016

    Redmine-Projekt zum IEMS-Kurs PMSE

  • Solving Dependency Quantified Boolean Formulas

    Solvers for Boolean satisfiability problems (SAT) are nowadays applied in numerous domains of Computer Science and Electronic Design Automation with great success: To mention only a few, they are most relevant in (formal) verification and test of hard- and software, e. g., for bounded model checking (BMC) and automatic test pattern generation (ATPG), but also have been successfully used in the area of artificial intelligence, e. g., for planning. In spite of the problem being NP-complete, modern solvers can handle formulas with hundred thousands of variables and millions of clauses. Therefore SAT solvers have gained high industrial relevance; most major chip manufacturers apply SAT-based techniques to find bugs in their hardware designs....

Also available in: Atom