Constraint programming (CP)is a paradigm for solving combinatorial problems that draws on a wide range of techniques from artificial intelligence, computer science, and operations research.
Constraint satisfaction problem (CSPs)are mathematical questions defined as the set of objects whose state must satisfy a number of constraints or/ limitations.
Boolean satisfiability problem (SAT)asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE.
Satisfiability modulo theories (SMT)generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings.
SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs.
how many ways the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE
Constraint satisfaction problemare mathematical questions defined as a set of objects whose state must satisfy a number of constraints or limitations.
c2dis a system that compiles CNF into d-DNNF (deterministic, decomposable negation normal form). d-DNNF is a tractable logical form that allows operations such as model counting, clausal entailment, and model enumeration and minimization to be performed in linear time. d-DNNF is also a strict superset of OBDD and is strictly more succinct than OBDD.
new approach to constructing programs, which exploits advances in constraint solving to make programming easier
much of everyday programming involves the use of domain-specific languages (DSLs) that are embedded, in the form of APIs and interpreters, into modern host languages (for example, JavaScript, Scala or Racket)
productivity tools based on constraint solvers (such as verification or synthesis) work best when specialized to a given domain
Rosette is a new kind of host language, designed for easy creation of DSLs that are equipped with solver-based tools.
CSE507: Computer-Aided Reasoning for Software EngineeringCovers theory, implementation, and applications of automated reasoning techniques, such as satisfiability solving, theorem proving, model checking, and abstract interpretation. Topics include concepts from mathematical logic and applications of automated reasoning to the design, construction, and analysis of software.