Boolean Satisfiability Problem (SAT)

SAT is the Boolean engine underlying more expressive reasoning paradigms:

• Satisfiability Modulo Theories (SMT): Decides the satisfiability of formulas over theories (e.g., linear arithmetic, arrays). Modern SMT solvers like Z3 use a SAT solver as the central dispatcher to handle the Boolean structure, consulting theory-specific solvers for constraints.
• Constraint Programming (CP): While CP solvers often use dedicated propagation algorithms, many hybrid approaches compile finite-domain constraint problems into SAT (SAT-encoding) to leverage the raw power of modern CDCL solvers for search.

Complex planning problems, where an agent must find a sequence of actions to achieve a goal, are encoded into SAT. This is known as SAT-based planning.

• The problem is bounded to a fixed number of time steps.
• Propositional variables represent facts and actions at each timestep.
• The initial state, goal conditions, and action preconditions/effects are encoded as clauses.
• The SAT solver finds an assignment that corresponds to a valid plan. This approach was famously used in Blackbox, a planner that competed in the International Planning Competition, translating planning problems into SAT for efficient solving.

SAT solvers attack cryptographic primitives by modeling their internal logic and searching for contradictions or keys.

• Algebraic Cryptanalysis: Represents a cipher (like AES or DES) as a large system of Boolean equations. The secret key is a variable; finding an assignment that satisfies the equations for a known plaintext-ciphertext pair recovers the key.
• Finding Collisions: Encodes the condition for a hash function collision (two different inputs producing the same output) as a SAT instance. Successful solves demonstrate cryptographic weaknesses.
• Reverse Engineering: Can be used to infer functionality or constraints from obfuscated or minified code.

Complex configurable systems, like software product families or hardware platforms with thousands of interdependent options, are modeled as Feature Models. These are essentially compact representations of a CSP.

• Each feature is a Boolean variable.
• Constraints define mandatory features, exclusions, and implications (e.g., "Sunroof requires Premium Audio").
• A SAT solver can instantly:
  • Check if a specific customer configuration is valid.
  • Find a valid configuration given a partial set of selected features.
  • Explain why an invalid configuration fails by analyzing the unsatisfiable core.
  • Count the total number of valid product variants, which can be in the billions.

SAT is the Boolean engine inside more advanced Satisfiability Modulo Theories (SMT) solvers like Z3 and CVC5. These solvers decide the satisfiability of formulas over theories like:

• Bit Vectors: For modeling fixed-width computer arithmetic.
• Arrays: For modeling memory reads and writes.
• Uninterpreted Functions: For abstract symbolic reasoning.
• Linear Integer/Real Arithmetic.

The SMT solver leverages a core CDCL SAT solver to handle the Boolean structure of the problem, while dedicated theory solvers check consistency within their domains. This combination powers program verification, compiler optimization, and automated theorem proving.

Z3 is a high-performance, open-source Satisfiability Modulo Theories (SMT) solver developed by Microsoft Research. It is a foundational tool in automated reasoning and a direct, more powerful successor to SAT solvers for many engineering tasks.

Primary use cases include:

• Software verification and bug finding.
• Program synthesis (automatically generating code from specifications).
• Security analysis (e.g., finding vulnerabilities).
• Complex configuration and planning for autonomous systems.

Z3 provides APIs for Python, C++, and other languages, making it accessible for integrating advanced constraint solving and theorem proving directly into agentic cognitive architectures.