Project

General

Profile

Projects

Filters

Apply Clear

  • AIGSolve

    Version von AIGSolve. Eliminierungsbasiertes Verfahren zur Evaluation von QBF. Inklusive Branch für MaxQBF.

  • AutoFault

    Attacking block cipher with SAT solver

  • 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,...
  • AVACS

    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

  • Brain Links - Brain Tools
  • 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]....
  • Arithmetikverifikation

    Ideen zu Arithmetikverifikation

  • Planning
  • SCA

    Repository access:
    git clone https://projects.informatik.uni-freiburg.de/git/sca

  • SAT2018PreProAC
  • PUF_GUI
  • Scale4Edge
  • SHIVA
  • SMILE
  • Solver Proxy

    SATSolverProxy is a C++ Framework to easily switch between multiple SAT solver.

    The following solver are currently supported:
    • antom [1]
    • CaDiCaL [2]
    • Glucose 3 [3]
    • Glucose 4.2.1 [3]
    • CryptoMiniSAT 5.6.5 [4]

    SATSolverProxy has served as the backend solver in several projects:...

  • 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