In this case b is called a support of a on c. This definition has been extended to non-binary constraints, giving generalized arc consistency (GAC). For simplicity, in the following we use the term AC to refer to both the binary and the nonbinary cases. 40 Y. Argyropoulos and K. Stergiou A common way to solve CSPs is using a backtracking-based search method. The most widely used such algorithm is MAC (Maintaining Arc Consistency) . At each step MAC makes an assignment of a value to a selected variable x and then applies AC.
The positive or negative appearance of a Boolean variable. As in CSPs, a common way to solve SAT problems is using backtracking search, and namely variations of the DPLL algorithm . At each step DPLL assigns a variable to one of its two possible values and applies a restricted form of resolution called Unit Propagation (UP). UP automatically sets to true the only literal appearing in a unary clause. As a result, any clause containing this literal is removed from the problem (as it is definitely true) while the size of any clause containing the opposite of this literal is reduced by one (as the literal is definitely false).