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

Subject
Computer Science
Publisher
Self-publishing
Published
2020
Pages
585
Edition
1
Language
English
PDF Size
6.1 MB
License
Open Publication License

Book Hashtags

Related Books

Libelf by Example
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 Notes for Professionals
The R Notes for Professionals book is compiled from Stack Overflow Documentation, the content is written by the beautiful people at Stack Overflow....
Mergers and Alliances in Higher Education
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...
Programming Persistent Memory
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...
Satellite Earth Observations and Their Impact on Society and Policy
The result of a workshop bringing together an international advisory board of experts in science, satellite technologies, industry innovations, and public policy, this book addresses the current and future roles of satellite Earth observations in solving large-scale environmental problems. The book showcases the results of engaging distinct communi...
Tools and Algorithms for the Construction and Analysis of Systems
The LNCS 11427 and 11428 proceedings set constitutes the proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2019, which took place in Prague, Czech Republic, in April 2019, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019. The tot...