Описание тега clpb

CLP(B), Constraint Logic Programming over Boolean variables, extends Prolog with specialized reasoning for propositional logic. Like SAT solvers, CLP(B) solvers allow to test for satisfiability, tautologies and other properties of SAT formulas.

Many Prolog systems ship with dedicated libraries or predicates for CLP(B). For example, SICStus Prolog and SWI ship with library(clpb), and GNU Prolog provides many predicates to express relations between Boolean formulas.

Generally, CLP(B) systems are more algebraically oriented than SAT solvers. Among the supported operations that go beyond typical SAT solvers are: variable quantification, unification, and symbolic residual goals.

Implementation methods for CLP(B) systems include BDD-based and approximation-based approaches. BDD-based systems are complete and provide some algebraic virtues like existential and universal quantification of variables which can be efficiently implemented with BDDs. Approximation-based approaches use other formalisms like CLP(FD) constraints or indexicals to express CLP(B) constraints. They are easy to implement and very efficient on many benchmarks, though typically incomplete and require explicit enumeration to test satisfiability.