Constraint Programming and Combinatorial Optimization

Constraint programming is a declarative computation paradigm defining solutions by variable domains and logical relations. Combinatorial optimization searches the corresponding discrete feasible region for optimal objective values. Propagation, systematic search, global constraints, SAT, SMT, and CP-SAT are analyzed through algorithms and correctness limits.

Unit 1: Mathematical Foundations of Constraint Satisfaction

1.1. Variables, Domains, and Relations

A constraint satisfaction problem comprises variables, domains, and relations restricting joint assignments. A solution is a complete assignment satisfying every constraint. Feasibility and minimization of an objective represent different computational tasks.

1.2. Constraint Graphs and the Search Space

A constraint graph connects variables participating in common constraints; hyperedges represent higher-arity relations. For finite-domain models, a naive search space is the product of all domain cardinalities.

P = (X,D,C);   Sol(P) = {a ∈ ∏[i] Dᵢ : ∀c∈C, c(a)=true}

1.3. Validation of Complete Assignments

Validate the formal model on small instances by enumerating every assignment. State the relation semantics and variable domains rather than relying on constraint names.

1.4. Numerical and Algorithmic Example

Three variables with domains {1,2,3} and AllDifferent admit six feasible assignments out of 27 total assignments, namely 3!. Domain filtering can reduce the search space without changing the valid assignments.

1.5. Mathematical Representation of Constraint Networks

A constraint satisfaction problem contains variables, their finite or otherwise well-defined domains, and relations that must all be satisfied. In its primal graph, variables are connected when appearing together in a constraint; a hypergraph represents n-ary constraints more directly. Satisfaction seeks any valid assignment without an objective. Optimization adds a criterion for ranking valid assignments.

CSP = (X,D,C);   Sol(CSP) = {x ∈ D : ∀c∈C, c(x)}

1.6. Local and Global Information in Satisfaction

Satisfying one binary constraint does not make the full network satisfiable. Relations such as X≠Y, Y≠Z and X=Z may be locally consistent yet become contradictory under restricted domains. Propagation removes domain values without valid support, but does not decide every general CSP by itself. Propagation and branching are therefore distinct algorithmic operations.

1.7. Small Instances for Model Verification

A reference enumerator can evaluate every assignment for small domains. It checks each constraint independently and compares results with a specialized solver. A reversed inequality or inconsistent indexing can produce incorrect outcomes even when propagation itself is implemented correctly. Data generation, model construction and solution checking must therefore be tested separately.

1.8. Computational Example and Calculation

For X,Y∈{1,2} and X≠Y, precisely the assignments (1,2) and (2,1) are feasible. All four possible assignments can be enumerated as a reference oracle.

|Sol(P)|=2;   (X,Y)∈{(1,2),(2,1)}

1.9. Independent Verification and Implementation Constraints

An independent enumerator can reveal incorrect relation direction or variable indexing.

Unit 2: Variables, Domains, and Constraint Modeling

2.1. Decision and Auxiliary Variables

Modeling distinguishes decision variables from derived variables. Redundant variables can enlarge search, but auxiliary variables can sometimes strengthen propagation. A model consists of domains and semantics as well as equations.

2.2. Modeling with Global Constraints

In scheduling, each job has a start time, duration, and resource requirement. Global constraints such as AllDifferent, NoOverlap, and Cumulative can express structure more directly than long families of pairwise constraints. Their support and semantics must be checked for the selected solver.

AllDifferent(x₁,…,xₙ) ⇒ xᵢ ≠ xⱼ   (i ≠ j)

2.3. Model Equivalence and Domain Validation

Model equivalence is evaluated by comparing solution sets on common instances. A shorter formulation does not automatically imply faster solving.

2.4. Numerical and Algorithmic Example

Three jobs of durations 2, 3, and 1 share one machine. With integer start times, NoOverlap prevents conflicting execution intervals. A required precedence such as finishing job one before starting job two must be declared separately.

2.5. Sparse and Dense Constraint Encodings

Binary relations can be represented through allowed-value tables, logical predicates or arithmetic inequalities. Dense tables grow large for wide domains, while sparse supports or forbidden tuples may be cheaper. Alternative representations must preserve the same solution set. Equivalence between a compiled encoding and the original problem should be tested on small instances.

Allowed(X,Y) = {(a,b) ∈ D(X)×D(Y) : C(a,b)}

2.6. Reification and Conditional Constraints

Reification associates a Boolean variable with the truth of a constraint. A one-way implication and a two-way equivalence have different semantics: b=1 may require C while C being true need not force b=1. Incorrect implication direction can admit unintended assignments in selection and scheduling models. Both truth cases should be tested.

2.7. Reversible Domain Reduction

Domain removals made during search must be reversible when returning to a branch point. Full-state copying is simple but expensive; trailing reversible updates or persistent structures may scale better. If propagation effects leak across branches, a solver can lose valid solutions. Restoration invariants should therefore be part of each branching test.

2.8. Computational Example and Calculation

Let b be Boolean and X integer with implication b=1 ⇒ X≤3. X=2,b=0 satisfies the implication but fails equivalence b⇔(X≤3).

b ⇒ (X≤3)  ≠  b ⇔ (X≤3)

2.9. Independent Verification and Implementation Constraints

Test whether the solver API constructs implication or full reification.

Unit 3: Constraint Propagation and Consistency Algorithms

3.1. Arc Consistency and Supports

Constraint propagation removes unsupported domain values without excluding valid solutions. Arc consistency of a binary constraint requires support in the adjacent domain for every retained value. Arc consistency alone does not guarantee the existence of a full solution.

3.2. The AC-3 Fixed-Point Algorithm

AC-3 enqueues arcs affected by domain reductions until reaching a fixed point. Only relevant neighboring constraints need reconsideration after a reduction. Queue order and cost of checking supports influence running time.

∀a∈D(X), ∃b∈D(Y) : C[X,Y](a,b)

3.3. Soundness and Completeness Limits

Removing a value requires proving the absence of its support in the relevant constraint. An empty domain proves failure; the absence of empty domains does not prove satisfiability.

3.4. Numerical and Algorithmic Example

If X and Y both have domains {1,2} and constraint X<Y, values X=2 and Y=1 lack support. Arc consistency leaves X=1 and Y=2. Solving this instance by propagation does not imply that propagation solves every CSP.

3.4.1. Illustrative Pseudocode

queue = all_directed_constraint_arcs()
while queue:
    (x,y) = queue.pop()
    if revise_domain(x, y):
        if empty(domain[x]): return INFEASIBLE
        enqueue_incoming_arcs_except(y, x)
return REDUCED_DOMAINS

3.5. Arc Consistency and Supports

For a directed arc X→Y, every value a in X's domain must have at least one supporting value b in Y's domain. Unsupported a values are removed, potentially requiring incoming neighboring arcs to be revised. Algorithms such as AC-3 maintain an update queue. More sophisticated support-caching methods reduce repeated checks but require extra memory and bookkeeping.

∀a∈D(X), ∃b∈D(Y) : C(X=a,Y=b)

3.6. Costs of Stronger Consistency Levels

Node, arc and path consistency offer different local guarantees. Stronger consistency may shrink the search tree but increase propagation work per node. Not every consistency level is polynomially cheap for arbitrary CSPs. For structured constraints, global propagators may reason more strongly than binary decompositions. Evaluations should report pruned values and total explored nodes together.

3.7. Fixpoints and Propagation Termination

Over finite domains, monotone propagation that only removes values terminates at a fixpoint or a contradiction. Poor queue scheduling may increase repeated work without changing the mathematical fixpoint. Reaching a fixpoint with nonempty domains does not mean a complete assignment exists. Search with further propagation is generally required.

3.8. Computational Example and Calculation

For X∈{1,2}, Y∈{2} and X<Y, value X=2 has no support and is removed. Domains become X={1},Y={2}, yielding a solution.

D(X)={1};  D(Y)={2}

3.9. Independent Verification and Implementation Constraints

Arc consistency alone does not solve every larger CSP, so search tests remain necessary.

Unit 4: Backtracking and Systematic Search

4.1. Backtracking Trees and Variable Selection

Backtracking chooses a variable assignment, propagates consequences, and backtracks from failures. Minimum remaining values selects the smallest current domain, while degree heuristics favor strongly connected variables. These heuristics reorder search without changing the solution set.

4.2. Conflict Analysis and Nogood Recording

Conflict-directed backjumping and nogood recording avoid repeated exploration of inconsistent partial assignments. Recorded nogoods must exclude only provably impossible assignments. Restarts can revisit the same subtrees unless useful learned information survives.

search(P) = propagate(P) → [branch(X=a) ∨ branch(X≠a)]

4.3. Search Metrics and Reproducibility

Benchmark node counts, propagator invocations, and wall-clock time independently. Compare heuristics under identical instances, random seeds, and hardware conditions.

4.4. Numerical and Algorithmic Example

Given variables with domains of sizes two and twenty, MRV prefers the first. On conflict, search backtracks without repeating the rejected assignment. One slow random-selection run does not establish a universal heuristic ranking.

4.4.1. Illustrative Pseudocode

propagate_current_domains()
if contradiction(): return FAILURE
if complete_assignment(): return SOLUTION
x = choose_variable_mrv()
for value in ordered(domain[x]):
    snapshot = save_reversible_state()
    branch(x == value)
    restore(snapshot)

4.5. Search Trees and Variable Selection

Backtracking organizes assignments in a decision tree; propagation at each node removes inconsistent branches. Minimum remaining values (MRV) chooses a tightly constrained variable first. Degree heuristics may favor variables involved in many other constraints. These heuristics are instance-dependent and do not guarantee a minimum number of search nodes.

T(n) ≈ |D₁|·|D₂|·…·|Dₙ|   (naive enumeration bound)

4.6. Forward Checking and Conflict Analysis

Forward checking removes inconsistent neighboring values after an assignment, while full arc consistency may propagate further. Upon contradiction, a solver can track decisions responsible for the conflict. Conflict-directed backjumping skips irrelevant branch levels, provided the recorded explanations are correct. Invalid explanations can incorrectly prune unseen valid solutions.

4.7. Restarts and Search Memory

Restarts revisit the root with potentially improved branching choices; not all learned information must be discarded. Retaining sound conflict information avoids repeating previously failed regions. Restart cost and conflict counts should be measured. For randomized search, seeds and tie-breaking policies are needed to reproduce outcomes.

4.8. Computational Example and Calculation

Suppose A has two remaining values and B has four. MRV branches on A first; after assigning A, propagation must refresh B’s domain.

|D(A)|=2<4=|D(B)|

4.9. Independent Verification and Implementation Constraints

After backtracking, verify complete restoration of domains to their prior decision level.

Unit 5: Global Constraints and Propagation Algorithms

5.1. Matching-Based AllDifferent

A global constraint encodes a structured relation among many variables. Pairwise inequalities are generally weaker in propagation than matching-based algorithms for AllDifferent. Cumulative constraints bound aggregate resource demand over time.

5.2. Cumulative Resource Constraints

A global propagator must preserve every feasible completion while removing impossible values. Matching-based approaches can exploit Hall-type conditions. In resource constraints, overlap reasoning and energetic reasoning provide distinct strengths of filtering.

∑[j : t∈[sⱼ,sⱼ+dⱼ)] rⱼ ≤ C   ∀t

5.3. Filtering Strength and Algorithm Cost

Propagation strength is balanced against runtime cost. Stronger propagators do not invariably solve faster; inspect both propagation time and the reduction in search-tree size.

5.4. Numerical and Algorithmic Example

AllDifferent over four variables can be encoded using six pairwise inequalities. Yet a matching-based global propagator can detect the impossibility of three variables restricted to two distinct values earlier. Equivalent models need not have equal propagation strength.

5.5. AllDifferent and Bipartite Matching

AllDifferent requires pairwise distinct values. Decomposition into binary inequalities preserves solutions but may propagate less strongly than a global constraint. If the variable-value bipartite graph lacks a matching covering all variables, the constraint is inconsistent. Régin-style filtering uses matching structure to remove domain values absent from every feasible complete matching.

AllDifferent(x₁,…,xₙ)  ⇒  |{x₁,…,xₙ}| = n

5.6. Cumulative Resource Scheduling

The cumulative constraint prevents overlapping tasks from exceeding resource capacity. Time-table propagation uses compulsory resource-usage intervals to eliminate impossible start times. Energetic reasoning compares workload inside a window with capacity multiplied by window length. Zero-duration tasks, preemption and alternative machines require carefully specified semantics.

5.7. Reusable Implementations of Global Constraints

A global propagator must report domain changes and support reversibility, not merely compute a result. Wake-up conditions, incremental caches, trailing and explanation generation belong to the solver architecture. Hard-coding each global constraint inside an application can increase maintenance and verification cost. Independent propagator tests must detect both missed pruning and unsound pruning.

5.8. Computational Example and Calculation

With domains {1}, {1,2} and {2,3}, AllDifferent has a unique full matching selecting 1,2,3 in order. Global propagation can remove 1 from the second and 2 from the third domain.

(x₁,x₂,x₃)=(1,2,3)

5.9. Independent Verification and Implementation Constraints

Force two variables to one value to verify detection of infeasible matchings.

Unit 6: Symmetry Breaking and Computational Complexity

6.1. Value and Variable Symmetries

A CSP symmetry transforms variables or values while preserving feasibility. Enumerating many equivalent solutions wastes search. Symmetry-breaking constraints must preserve at least one representative from every equivalence class.

6.2. Lexicographic Symmetry Breaking

Identical servers in assignment models may be permuted. Lexicographic rules on server-use patterns may prune equivalent branches. When server costs differ, these permutations generally cease to be symmetries.

σ∈Aut(P) ⇒ [a∈Sol(P) ⇔ σ(a)∈Sol(P)]

6.3. Equivalence Classes and Solution Preservation

Check proposed symmetries by explicit transformations of small instances. An incorrectly assumed symmetry can remove optimal solutions.

6.4. Numerical and Algorithmic Example

With two identical servers, swapping their labels in an assignment produces an equivalent solution. If server A has a distinct cost, the symmetry disappears. Verify symmetry assumptions before adding ordering constraints.

6.5. Solution Symmetries and Group Actions

A variable or value permutation that preserves every constraint and objective is a symmetry of the model. Searching equivalent solutions individually can create enormous redundancy. Symmetry-breaking constraints must retain at least one representative from each orbit. An incorrect lexicographic ordering restriction may eliminate all globally optimal representatives. Symmetry must be established through model invariance rather than superficial solution similarity.

σ ∈ Aut(P)  ⇒  [x∈Sol(P) ⇔ σ(x)∈Sol(P)]

6.6. Static and Dynamic Symmetry Breaking

Static symmetry breaking adds constraints before search; dynamic methods recognize symmetric branches during traversal. Too many static constraints can increase propagation overhead. Dynamic techniques depend on branching history and group representations. Both approaches should be tested on small instances by enumerating solution orbits and verifying that at least one representative of each remains.

6.7. Complexity Under Structural Restrictions

Hardness of general CSP does not mean that every structured constraint graph is difficult. Tree-structured networks may admit polynomial-time elimination or dynamic programming. Intermediate tables can grow exponentially with treewidth. Evaluation should therefore include domain sizes, constraint tightness and graph structure alongside variable counts.

6.8. Computational Example and Calculation

With identical resources, swapping the labels of the resources leaves an assignment outcome unchanged. A carefully chosen ordering constraint can reduce such symmetric duplications.

resource₁ ≤lex resource₂

6.9. Independent Verification and Implementation Constraints

If resources have different speeds, the assumed symmetry fails and the ordering restriction may be unsound.

Unit 7: Soft Constraints and Constrained Optimization

7.1. Hard and Soft Constraints

Hard constraints define mandatory feasibility while soft constraints express preferences or violation penalties. When not all constraints can be met, allowed violations must be specified explicitly. Weighted penalties combine priorities into one score but large weights can cause numerical issues.

7.2. Weighted and Lexicographic Objectives

Lexicographic optimization optimizes a primary criterion before secondary criteria while preserving the primary optimum. Pareto methods retain nondominated alternatives instead of collapsing objectives into one score. These are distinct decision rules.

min[x∈ℱ] ∑[k=1..m] wₖ·violationₖ(x)

7.3. Penalty Scaling and Pareto Solutions

Perform weight-sensitivity analysis and never silently permit hard-constraint violations through penalty terms. Report objective scaling choices separately.

7.4. Numerical and Algorithmic Example

Suppose a preferred deadline incurs penalty two per delay unit. This soft requirement cannot override a hard capacity constraint. When objectives have strict priority, use lexicographic optimization rather than arbitrary blended weights.

7.5. Soft Constraints and Violation Costs

Hard constraints define admissibility, whereas soft constraints permit violations at a specified cost. Violation may be represented by a Boolean indicator, absolute deviation or piecewise penalty. Weights must reflect genuine priorities and units; arbitrary magnitudes can mask trade-offs. Replacing a nonnegotiable hard constraint with a large penalty does not guarantee that it will never be violated.

min ∑ₖ wₖ · violationₖ(x)

7.6. Weighted MaxSAT and Lexicographic Objectives

MaxSAT maximizes satisfied Boolean clauses, and weighted versions attach different penalties to soft clauses. When objectives have strict priorities, lexicographic optimization can be safer than arbitrarily large weights. The first objective is optimized and fixed before solving for the next. Objective values and numerical tolerances must be retained separately.

7.7. Explaining Soft-Constraint Solutions

A solver should report which soft constraints are violated and the penalty contribution of each, not just an aggregate penalty. For scheduling, the magnitude of lateness, affected tasks and relevant hard capacity constraints must be independently verified. Such explanations help integrate solver output with decision support without replacing mathematical correctness checks.

7.8. Computational Example and Calculation

Suppose soft constraints have violation costs 3 and 5, and hard constraints force exactly one to be violated. The minimum-penalty choice violates the one costing 3.

min penalty ∈ {3,5} = 3

7.9. Independent Verification and Implementation Constraints

Validate the hard constraints causing the conflict and whether alternative assignments are feasible.

Unit 8: Combinatorial Optimization Algorithms

8.1. Exact and Approximate Solutions

Combinatorial optimization searches finite but potentially enormous discrete feasible sets. For NP-hard problems, there is no known general polynomial-time exact algorithm unless major complexity assumptions change. Exact optimization, approximation guarantees, and empirical heuristic success are distinct.

8.2. Local Search and Neighborhood Operators

Local search moves among neighboring solutions; tabu memory or restarts can change the region explored. An approximation algorithm provides a proved worst-case ratio for a specified problem class. Good average-case heuristics alone do not establish such a guarantee.

f(x[alg]) / f(x*) ≥ 1/α;   α ≥ 1;   f(x*) > 0

8.3. Quality Guarantees and Empirical Gaps

Compare heuristic results with exact optima for small instances and calculate relative gaps. For large instances, use valid bounds or independently established reference values.

8.4. Numerical and Algorithmic Example

For traveling-salesperson tours, 2-opt local search improves a tour by exchanging edges, but its local optimum need not be global. Exhaustive enumeration or an exact solver supplies reference values on small instances.

8.5. Exact Algorithms and Approximation Guarantees

Exact combinatorial algorithms may certify optimality or provide rigorous bounds. Approximation algorithms instead guarantee a solution ratio under explicit assumptions. Ratio directions differ between maximization and minimization, and zero or negative objective values require care. Strong empirical heuristic performance is not equivalent to a proven approximation guarantee.

min problem: cost(alg) ≤ α·cost(opt),  α≥1

8.6. Relaxation and Rounding

Continuous relaxations of integer decisions may give tractable subproblems. Independently rounding each fractional variable can violate capacity or assignment constraints, so feasibility after rounding requires proof. Randomized rounding also needs bounds on constraint-violation probability. Derandomization and repair may add cost and must be included in any guarantee.

8.7. Structure of Specialized Problem Families

Problems such as minimum spanning tree, shortest path, matching and maximum flow have polynomial algorithms under their standard definitions, whereas general traveling-salesperson and set-cover problems are NP-hard. Similar graph representations do not imply equal complexity. Solver selection depends on objectives, restrictions, weight signs and graph structure. A specialized algorithm is justified only when the model genuinely belongs to its supported problem family.

8.8. Computational Example and Calculation

For universe {a,b,c} and candidate sets {a,b} and {b,c}, both sets must be chosen to cover all elements, giving an optimum of 2.

minimum set cover size = 2

8.9. Independent Verification and Implementation Constraints

Compare exhaustive enumeration, integer modeling and greedy choice on the identical instance.

Unit 9: Boolean Satisfiability and SAT Solvers

9.1. CNF and Literals

SAT asks whether a Boolean formula admits a satisfying assignment. In CNF, the formula is a conjunction of clauses, each a disjunction of literals. General SAT is NP-complete, while restricted cases such as Horn-SAT and 2-SAT have polynomial-time algorithms.

9.2. CDCL and Unit Propagation

CDCL solvers combine unit propagation, decision assignments, conflict analysis, and learned clauses. Two-watched-literal mechanisms reduce propagation overhead. A learned clause is sound only if logically implied by the original formula.

F = ⋀[j=1..m] (⋁[ℓ∈Cⱼ] ℓ)

9.3. Validation of SAT/UNSAT Results

SAT assignments can be checked by evaluating the formula; UNSAT claims require a suitable proof trace or independent procedure. A timeout is not an UNSAT result.

9.4. Numerical and Algorithmic Example

The CNF (a∨b)∧(¬a∨c) is satisfied by a=0, b=1, c=0. A SAT assignment is independently checked by evaluating all clauses. An UNSAT result cannot be certified by merely observing one failed search branch.

9.5. CNF and Tseitin Transformation

SAT solvers typically process propositional formulas in conjunctive normal form. Naive distribution can cause exponential expansion; Tseitin transformation introduces auxiliary variables to construct a linearly sized equisatisfiable CNF. The meaning of auxiliary variables must be retained for decoding assignments back to original variables. Logical equivalence and mere equisatisfiability are different verification claims.

F = C₁ ∧ C₂ ∧ … ∧ Cₘ;   Cⱼ = ℓ₁ ∨ … ∨ ℓₖ

9.6. CDCL, Learned Clauses and Backjumping

Conflict-driven clause learning analyzes contradictions through Boolean propagation and decision levels. A learned clause blocks recurrence of a conflicting decision combination. First-UIP learning is common, but every learned clause must be logically implied by the original formula and valid deductions. Unbounded clause databases consume memory, motivating reduction policies.

9.7. Two-Watched Literals and Unit Propagation

Two-watched literals support efficient unit propagation without scanning every literal of every clause after each assignment. When a watched literal becomes false, an alternative is sought; otherwise a unit implication or conflict is detected. Incorrect sign or decision-level bookkeeping can produce false UNSAT reports. Small random formulas should be cross-checked against exhaustive enumeration.

9.8. Computational Example and Calculation

For (a∨b)∧(¬a∨c), assignment a=1,b=0,c=1 satisfies both clauses; a=1,c=0 violates the second clause.

F=(a∨b)∧(¬a∨c);   F(1,0,1)=true

9.9. Independent Verification and Implementation Constraints

Check the original propositional formula after decoding a SAT assignment.

Unit 10: SMT and CP-SAT Solver Architectures

10.1. Boolean Logic and Theory Solvers

SMT combines Boolean structure with theories such as linear arithmetic, bit-vectors, or arrays. Its solver coordinates propositional decisions with theory consistency checking. CP-SAT uses a different architecture for integer and Boolean constraint optimization with propagation and search.

10.2. Modeling Languages and Integer Scaling

SMT-LIB is an interchange language for formulas, whereas MiniZinc models can compile to different backend solvers. OR-Tools CP-SAT uses integer-valued variables and coefficients, so real-valued inputs require justified scaling. These tools do not accept identical model classes.

SMT: SAT + theory consistency checks;   CP-SAT ≠ SMT

10.3. Solver Classes and Comparison Metrics

Where solvers support equivalent models, validate outputs against the original constraints. An unknown or timeout outcome from one solver does not establish that another is incorrect.

10.4. Numerical and Algorithmic Example

SMT can represent (x−y=3)∧(x≥0)∧(y≥0) in integer arithmetic. CP-SAT can use bounded integer variables. Translating real-valued constraints into integer-scaled arithmetic without precision analysis may change the feasible set.

10.5. DPLL(T) and Theory Solver Cooperation

SMT combines Boolean structure with consistency checks over selected theories such as linear arithmetic, bit vectors and arrays. In DPLL(T), a SAT engine proposes Boolean assignments and theory solvers test their semantic consistency. Theory conflicts can be fed back as explaining clauses. Decidability and complexity depend on the chosen theory; arbitrary program behavior is not generally decidable.

SMT = Boolean search + theory consistency;   SAT ≠ SMT

10.6. CP-SAT and Integer Constraint Encoding

CP-SAT combines SAT-style learning and search with integer variables, scheduling constraints and optimization. It is not synonymous with a general SMT solver; available domains and arithmetic depend on the solver. Real-valued variables may need careful integer scaling rather than direct exact representation. Scaling factors, overflow bounds and integer arithmetic checks are integral to model correctness.

10.7. Validation at Solver API Boundaries

Solver API integration must respect indices, signed integer ranges and model-object lifetimes. UNKNOWN or timeout cannot be presented as proven UNSAT. Returned assignments should be checked against the original constraints. Differential testing across solvers can reveal encoding defects, although disagreement alone does not identify the faulty implementation.

10.8. Computational Example and Calculation

For arithmetic constraints x−y=3, x≥0,y≥0, assignment x=3,y=0 is valid. Satisfiability of the Boolean abstraction alone does not ensure consistency of the arithmetic theory.

(x,y)=(3,0)  ⇒  x−y=3

10.9. Independent Verification and Implementation Constraints

Theory conflicts require explanation clauses justified by the current arithmetic assumptions.

Unit 11: Scheduling, Assignment, and Routing Optimization

11.1. Precedence and Time Variables

Scheduling combines precedence relations, start times, and resource capacities. Processing time differs from waiting time. NoOverlap captures exclusive resource use whereas Cumulative limits concurrent consumption of a finite capacity.

11.2. Resource Constraints and Routing Models

Binary variables assign jobs to resources. Routing problems require subtour-elimination constraints in addition to capacity and visit requirements. Visiting every node does not automatically establish one connected tour.

sⱼ ≥ sᵢ + dᵢ   (i ≺ j);   ∑[i] rᵢ(t) ≤ C

11.3. Connectivity and Schedule Validation

Check precedence in schedules, connectivity and capacity in routes, and exactly-one constraints in assignments. Benchmark methods on equivalent problems and hardware.

11.4. Numerical and Algorithmic Example

With job durations 2, 3, and 4, precedence A≺C requires C to start after A completes. A conflict-free schedule can still violate precedence, so check both resource and ordering constraints.

11.5. Precedence Graphs and Critical Paths

Scheduling precedence forms a directed graph with tasks as vertices and mandatory finish-to-start relations as edges. Cycles with positive-duration precedence make the model infeasible. The critical path provides a lower bound when resource limits are ignored. With finite resource capacities, precedence bounds alone do not determine optimal makespan; resource conflicts require additional constraints.

startⱼ ≥ startᵢ + durationᵢ  (i ≺ j)

11.6. Alternative Resources and Nonpreemptive Tasks

Tasks executable on multiple machines may have machine-dependent durations and costs. Nonpreemptive activities cannot be split, unlike explicitly preemptive models. Time-indexed formulations can become large, while interval variables and specialized propagators may be more efficient. Resource calendars, maintenance windows and unavailable periods belong in feasibility checking.

11.7. Routing Constraints and Subtour Elimination

Degree constraints alone may admit multiple disconnected cycles in traveling-salesperson and vehicle-routing formulations. Connectivity needs subtour elimination, flow-based formulations or valid cuts. Capacity and time windows depend on route order. Tests must verify full visitation, connected routes, timing and load capacity, not just total distance.

11.8. Computational Example and Calculation

Task A takes 2 units, B takes 3 and B may start only after A finishes. Without further restrictions the earliest makespan is 5.

startᴮ ≥ startᴬ+2;  finishᴮ ≥ 5

11.9. Independent Verification and Implementation Constraints

A resource calendar can increase actual makespan while leaving the precedence lower bound valid.

Unit 12: Solver Implementation, Correctness, and Performance

12.1. Solver Lifecycle and Reversible State

Solver implementations separate parsing, normalization, propagation, search, and result checking. Reversible data structures must restore domain changes correctly at every backtrack. A faulty undo operation can produce incorrect answers, not merely a slowdown.

12.2. Metamorphic Tests and Independent Validation

Correctness tests combine exhaustive small cases, random instances, metamorphic transformations, and cross-solver checks. Renaming a symmetric variable should preserve satisfiability. UNSAT claims require a proof or independent verifier when strong assurance is needed.

valid(x) = ⋀[c∈C] c(x);   gap = |z[inc]−z[bound]| / max(1, |z[inc]|)

12.3. Performance and Optimality Metrics

Performance reports include node count, propagation time, peak memory, best bound, and time limits. One runtime from one seed and instance distribution cannot support broad performance claims.

12.4. Numerical and Algorithmic Example

Renaming symmetric variables must preserve the SAT/UNSAT status. If a metamorphic test yields a different result, inspect parsing, model construction, and reversible state handling. Preserve original models and solver outputs.

12.4.1. Illustrative Pseudocode

parse_and_normalize(model)
candidate = search_with_propagation(model)
if candidate: assert check_all_constraints(model, candidate)
if solver_claims_unsat: verify_proof_or_independent_solver()
record_nodes_time_memory_limits()

12.5. Separating UNSAT and OPTIMAL Certificates

Checking all constraints is often enough to verify a feasible assignment, but proving unsatisfiability requires stronger evidence than unsuccessful search. SAT witnesses are straightforward to check, whereas UNSAT may be supported by a proof trace and independent proof checker. Optimization additionally requires a bound excluding better feasible candidates. Result statuses must be classified explicitly.

verified OPTIMAL ⇒ feasible candidate ∧ valid bound ∧ closed gap

12.6. Property-Based and Differential Tests

Solver tests should cover randomized satisfiable models, constructed contradictions, empty domains, singleton domains and boundary cases. Adding a constraint cannot enlarge the solution set, providing a useful metamorphic property. Distinct encodings of one model should preserve satisfiability. False UNSAT outcomes are especially serious because they incorrectly exclude every valid solution.

12.7. Comprehensive Benchmark Design and Limits

Benchmarks should include search nodes, conflicts, propagations, memory, wall-clock time and timeout rates. Sampling only easy or solver-friendly instances biases comparisons. Hardware, thread count, random seeds and default-parameter versions must be controlled. Reporting UNKNOWN is scientifically valid provided it is not confused with either SAT or UNSAT.

12.8. Computational Example and Calculation

A CSP with a required variable having an empty domain is immediately infeasible. By contrast, UNKNOWN or a time-limited search does not certify unsatisfiability.

D(X)=∅  ⇒  Sol(P)=∅

12.9. Independent Verification and Implementation Constraints

Verification reports must distinguish explicit contradiction certificates from inconclusive search failures.

References

• Google OR-Tools. CP-SAT Solver Documentation. https://developers.google.com/optimization/cp/cp_solver
• Korte, Bernhard; Vygen, Jens. Combinatorial Optimization: Theory and Algorithms. 6th ed. Springer, 2018.
• Microsoft Research. The Z3 Guide. https://microsoft.github.io/z3guide/
• MiniZinc. MiniZinc Handbook. https://docs.minizinc.org/en/stable/
• Rossi, Francesca; van Beek, Peter; Walsh, Toby (eds.). Handbook of Constraint Programming. Elsevier, 2006. ISBN 9780444527264.