# Solwery SAT i SMT

EN: **SAT and SMT solvers** · id `satsmt` · aliases: SAT solver, SAT solvers, SMT solver, SMT solvers, solwer SAT, solwer SMT, solwery SAT i SMT

Path: [AI Atlas](https://aiatlasgraph.com/llms.txt) › [Fundamenty i rozumowanie](https://aiatlasgraph.com/t/foundations.md) › [Logika i reprezentacja wiedzy](https://aiatlasgraph.com/t/logic.md) › Solwery SAT i SMT

## Description

- PL: Silniki rozstrzygające spełnialność formuł logiki zdań (SAT) i formuł z teoriami tła, np. arytmetyką czy tablicami (SMT).
- EN: Engines deciding satisfiability of propositional formulas (SAT) and of formulas with background theories such as arithmetic or arrays (SMT).

## In one sentence

- PL: Programy, które błyskawicznie sprawdzają, czy da się spełnić naraz tysiące logicznych warunków, i podają przykład takiego rozwiązania.
- EN: Programs that quickly check whether thousands of logical conditions can all hold at once, and give an example solution.

## Problem it solves

- PL: Wiele zadań, od planowania po sprawdzanie programów, wymaga przeszukania astronomicznej liczby kombinacji, czego nie da się zrobić ręcznie.
- EN: Many tasks, from scheduling to checking programs, require searching an astronomical number of combinations, impossible by hand.

## What it does

- PL: Jak bardzo sprytny rozwiązywacz łamigłówek: próbuje, a po każdej sprzeczności zapisuje lekcję, żeby nie wpadać w ten sam błąd.
- EN: Like a very clever puzzle solver: it tries, and after each contradiction records a lesson so it never repeats the same mistake.

## Everyday example

- PL: Narzędzie programisty wskazuje, przy jakich danych wejściowych program może się wysypać, zanim zrobi to użytkownik.
- EN: A developer tool points out which inputs could make a program crash before a user hits them.

## This concerns you if you…

- PL: chcesz sprawdzić, czy kod lub reguły nie mają luk
- PL: układasz harmonogramy z wieloma ograniczeniami
- PL: łączysz modele językowe z twardym sprawdzaniem logiki
- EN: want to check that code or rules have no gaps
- EN: build schedules with many constraints
- EN: combine language models with rigorous logic checks

## Keywords

CDCL · DPLL · Z3 · cvc5 · MaxSAT · bounded model checking · symbolic execution · neural network verification · SAT competition · MiniSat

## How it works

- PL: Solwery SAT działają na formułach w postaci koniunkcyjnej normalnej; algorytm CDCL przypisuje wartości, propaguje skutki i z każdego konfliktu wyprowadza nową klauzulę, która przycina przeszukiwanie. Solwery SMT łączą taki rdzeń z wyspecjalizowanymi procedurami dla teorii tła. Stosuje się je w weryfikacji oprogramowania, generowaniu testów, planowaniu i weryfikacji sieci neuronowych.
- EN: SAT solvers work on conjunctive normal form; the CDCL algorithm assigns values, propagates consequences and learns a new clause from each conflict to prune search. SMT solvers combine such a core with specialised procedures for background theories. They are used in software verification, test generation, planning and neural-network verification.

## Limits

- PL: Problem SAT jest NP-zupełny, więc niektóre małe formuły bywają nierozwiązywalne w rozsądnym czasie. Problem trzeba najpierw precyzyjnie zakodować, a teorie z kwantyfikatorami lub nieliniową arytmetyką bywają nierozstrzygalne albo bardzo kosztowne.
- EN: SAT is NP-complete, so some small formulas can be intractable in reasonable time. The problem must first be encoded precisely, and theories with quantifiers or nonlinear arithmetic may be undecidable or very costly.

## Key terms

- PL: **CNF**: Formuła zapisana jako iloczyn alternatyw prostych warunków.
- PL: **CDCL**: Przeszukiwanie, które uczy się nowych reguł z napotkanych sprzeczności.
- PL: **teoria tła**: Dodatkowa dziedzina, np. liczby całkowite, rozumiana przez solwer.
- EN: **CNF**: A formula written as an AND of OR-clauses.
- EN: **CDCL**: Search that learns new rules from contradictions it meets.
- EN: **background theory**: An extra domain, e.g. integers, the solver understands.

## Know first

- [Logika zdań i logika pierwszego rzędu (Propositional and first-order logic)](https://aiatlasgraph.com/t/fol.md)
- [Problemy z ograniczeniami (CSP) (Constraint satisfaction problems (CSP))](https://aiatlasgraph.com/t/csp.md)

## Related topics

Untyped, symmetric "see also" links.

- [Automatyczne dowodzenie twierdzeń (Lean) (Automated and formal theorem proving (Lean))](https://aiatlasgraph.com/t/theoremproving.md)

## Sources

- [Russell & Norvig · Artificial Intelligence: A Modern Approach, 4th ed. — table of contents](<https://aima.cs.berkeley.edu/>) `aima4` · by Stuart Russell, Peter Norvig
- [de Moura & Bjørner · Z3: An Efficient SMT Solver](<https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/>) `demoura-bjorner-z3-2008` · by Leonardo de Moura, Nikolaj Bjørner

---

AI Atlas revision 122 (2026-10-30) · HTML: https://aiatlasgraph.com/t/satsmt · index: https://aiatlasgraph.com/llms.txt · everything: https://aiatlasgraph.com/llms-full.txt · updated 2026-10-30