
## 2. Background

In this section we give a brief account of the sat and csp **problems and related notions.**
Propositional logic. We assume standard notions of propositional logic: literal, clause, propositional formula, **conjunctive normal form** (cnf), valuation (or assignment), **interpretation**,
model, satisfiable formula, etc. We denote by ⊤ and ⊥ the Boolean constants true and false and the logical connectives by ¬ (negation), ∧ (conjunction), ∨ (disjunction), ⊕ (exclusive disjunction), ⇒ (implication), ⇔ (equivalence). Two formulae A and B **are said to**
be equivalent if A and B have the same truth value in any valuation. Two formulae A and B are said to be weakly equivalent (or equisatisfiable) if whenever A **is satisfiable then** B is satisfiable and vice versa.

Constraint Satisfaction Problem. A constraint satisfaction problem (csp**) is defined as a**
triple (X, D, C), where X is a finite set of variables x1, x2, . . ., xn, D **is a set of domains**
d1, d2, . . ., dn for these variables, and C is a set of constraints c1, c2, . . ., ck**. In a finitedomain** csp, all sets from D are finite. Constraints from C **may define combinations of**
values assigned to variables that are allowed or that are prohibited**. A problem instance** is satisfiable if there is an assignment to variables such that all constraints are satisfied. Such assignment is called a solution**. A constraint optimization problem is a** csp **in which** the goal is to find a solution maximizing (or minimizing) a given objective function **over all**
allowed values of the given variables.

sat **Problem and** sat **Solvers.** sat **is the problem of deciding if a given propositional formula** in cnf is satisfiable, i.e., if there is any assignment to variables **such that all clauses are true.**
Obviously, sat **is a special case of** csp, with all variables ranging over the domain {0, 1} and with constraints given as clauses. sat was the first problem shown to be np**-complete [15],**
and it still holds a central position in the field of computational complexity. Stochastic sat solvers cannot prove the input instance to be unsatisfiable, **but may find a solution (i.e., a**
satisfying variable assignment) for huge satisfiable instances quickly. On the other hand, for a given sat **instance, a complete** sat **solver always finds a satisfying variable assignment** or shows that there is no such assignment. Most of the state-of-the-art complete sat solvers are cdcl **(conflict-driven, clause-learning) based extensions of the Davis-PutnamLogemann-Loveland algorithm (**dpll**) [18, 17, 3]. In recent years, a tremendous advance**
has been made in sat **solving technology [52, 22, 75, 3]. These improvements involve both** high-level and low-level algorithmic techniques. The advances in sat **solving make possible** deciding satisfiability of some industrial sat **problems with tens of thousands of variables** and millions of clauses.

## 3. Problem Specification And Problem Solving

There are two basic components of the presented approach: - **problem specification: a problem is specified by a test (expressed in an imperative form)**
that given values of relevant variables are indeed a solution to the problem.

- **problem solving: all relevant variables of the problem are represented by finite vectors of**
propositional formulae (corresponding to vectors of bits and to binary representation, in case of numerical values); the specification is symbolically executed over such representation and the assertion that given values make a solution is transformed to an instance