SAT/SMT by Example
by Dennis Yurichev
DescriptionTable of ContentsDetailsHashtagsReport an issue 
Book Description
SAT/SMT solvers can be viewed as solvers of huge systems of equations. The difference is that SMT solvers takes systems in arbitrary format, while SAT solvers are limited to boolean equations in CNF 1 form. A lot of real world problems can be represented as problems of solving system of equations.This open book is licensed under a Open Publication License (OPL). You can download SAT/SMT by Example ebook for free in PDF format (6.1 MB).
Table of Contents
Chapter 1
Introduction
Chapter 2
Basics
Chapter 3
Equations
Chapter 4
Proofs
Chapter 5
Verification
Chapter 6
Regular expressions
Chapter 7
Gray code
Chapter 8
Recreational mathematics and puzzles
Chapter 9
Graph coloring
Chapter 10
Knapsack problems
Chapter 11
Social Golfer Problem
Chapter 12
Latin squares
Chapter 13
Cyclic redundancy check
Chapter 14
MaxSAT/MaxSMT
Chapter 15
Synthesis
Chapter 16
Toy decompiler
Chapter 17
Symbolic execution
Chapter 18
KLEE
Chapter 19
(Amateur) cryptography
Chapter 20
First-Order Logic
Chapter 21
Cellular automata
Chapter 22
Everything else
Chapter 23
Toy-level solvers
Chapter 24
Glossary (SAT)
Chapter 25
Further reading
Chapter 26
Some applications
Chapter 27
Acronyms used
Book Details
Title
SAT/SMT by Example
Subject
Computer Science
Publisher
Self-publishing
Published
2020
Pages
585
Edition
1
Language
English
PDF Size
6.1 MB
License
Open Publication License
Related Books
This tutorial introduces libelf, a library for reading and writing object code in the Extensible Linking Format (ELF) file format.
- Getting started with libelf: obtaining a handle to an ELF object, establishing a working ELF version, and handling errors reported by libelf.
- How ELF data structures are laid out in-memory and on disk, the notions...
R is a programming language and free software environment for statistical computing and graphics. It is an unofficial and free R ebook created for educational purposes. All the content is extracted from Stack Overflow Documentation, which is written by many hardworking individuals at Stack Overflow....
The R Notes for Professionals book is compiled from Stack Overflow Documentation, the content is written by the beautiful people at Stack Overflow....
Julia is a high-level, dynamic programming language. Its features are well suited for numerical analysis and computational science.
Julia works with other languages (C, Python, R, Rust, C++, SQL, JavaScript, ...)
The Purpose of this open book is to introduce programmers to the Julia programming by example. This is a simplified exposition of the l...
Higher education in Europe and beyond faces a series of major challenges. The economic crisis has accelerated expectations of an increased role in addressing economic and societal challenges while, at the same time, putting pressure on available finances. Broader trends such as shifting student demographics and expectations, globalisation and mobil...
Beginning and experienced programmers will use this comprehensive guide to persistent memory programming. You will understand how persistent memory brings together several new software/hardware requirements, and offers great promise for better performance and faster application startup times - a huge leap forward in byte-addressable capacity compar...