Satisfiability Problems - shivamvats/notes GitHub Wiki

Constraint Satisfaction Problem (CSP)

CSPs are defined as problems involving a set of objects whose states must satisfy a number of constraints or limitations. SAT and SMT problems are specific forms of CSP.

Boolean Satisfiability (SAT)

Also called the Propositional Satisfiability Problem. Given a propositional-logic formula or a boolean expression, decide whether the formula is satisfiable or not, i.e. whether some assignment of true/false to the logic variables exists that will make the formula true.

  • Fluent: An aspect of the problem that changes with time. It is a synonym of state variable. Eg: Facing-East-0, Facing-East-1, Facing-East-t etc.

Satisfiability Modulo Theories (SMT)

The SMT problem is a decision-making problem for logical formulas with respect to some background theory expressed in first-order logic with equality.

⚠️ **GitHub.com Fallback** ⚠️