Part IV · Ch. 18 — Logic Programming / Solvers
Symbolic · Formal reasoning · Resolution / SAT-SMT. Solves problems declared as logical formulas or constraints — with guaranteed correctness. Card:
../02-types-of-ai/01-symbolic.kmd.
🎨 Figure
F-IV.18.0— From formula to solution. Brief: a set of logical constraints entering a solver that returns SAT (with an assignment) or UNSAT; a stylized backtracking tree.
1. Definition and short history
Solves satisfiability and constraints by complete logical search. Lineage: Prolog (1972), the Fifth Generation project (Japan, 1982), and modern SAT/SMT solvers (Z3) ubiquitous in verification.
2. Foundations
- Mathematical logic / proof theory — satisfiability, resolution.
- Complexity — SAT is the canonical NP-complete problem.
- Combinatorics — search over the space of assignments.
3. Algorithms and architectures
- Resolution / unification — basis of Prolog.
- DPLL / CDCL — core of modern SAT solvers (conflict-driven).
- SMT — SAT + theories (arithmetic, arrays); e.g., Z3.
- ASP / CP — Answer Set Programming, constraint programming.
4. Inputs
- Hardware: CPU; some problems explode (NP).
- Data: the problem formulation (clauses/constraints).
- Data structures: clauses, implication graph, trail.
- Systems: Prolog, MiniSat, Z3, OR-Tools.
5. Specialized lifecycle
| Stage | Specialization |
|---|---|
| 0 Problem | Problem formalizable in logic/constraints |
| 1 Data | Encode the problem (clauses, theories) |
| 2 EDA | Structure/difficulty of the instance |
| 3 Modeling | Choose SATSMTCP; efficient encoding |
| 4 "Training" | There is none — there is formulation; solvers have heuristics |
| 5 Evaluation | Correctness (guaranteed), time to solution |
| 5.5 Acceptance | Validate the encoding against the real problem |
| 6 Production | Solve instances; timeouts/heuristics |
| 7 Monitoring | Hard instances, time |
| 8 Maintenance | Reformulate as the domain changes |
| 9 Governance | Reliability of the proof/verification |
6. Capabilities, modes and modalities
Deductive/verification: hardware/software verification, scheduling, configuration, proof; guaranteed correctness when it terminates.
7. Limits, risks and ethics
NP-hardness (may not scale); requires exact formalization; no learning. Strong point: formal guarantees — hence the central role in neuro-symbolic AI (ch. 32) and in trustworthy AI.
8. State of the art and examples
Z3 (SMT), CDCL SAT solvers, OR-Tools; formal verification, program synthesis; LLM + solver (the LLM formalizes, the solver guarantees) is a trend in trustworthy reasoning.