Version von AIGSolve. Eliminierungsbasiertes Verfahren zur Evaluation von QBF. Inklusive Branch für MaxQBF.
Attacking block cipher with SAT solver
- antomantom is a C++ library for solving
- Unweighted MaxSAT,
- Partial MaxSAT, and
- #SAT problems.
- Various activity-based decision heuristics,
- Fast unit propagation via watched literals,...
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 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....
countAntom  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 ....
- SAT-based Attacks on Small Scale AES
SAT-based attacks on different vhdl implementations of small scale AES.
Ideen zu Arithmetikverifikation
git clone https://projects.informatik.uni-freiburg.de/git/sca
- Solver Proxy
SATSolverProxy is a C++ Framework to easily switch between multiple SAT solver.The following solver are currently supported:
- antom 
- CaDiCaL 
- Glucose 3 
- Glucose 4.2.1 
- CryptoMiniSAT 5.6.5 
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