Overview

A Constraint Satisfaction Problem (CSP) is a formal computational framework in which a set of variables, each taking values from a given domain, is restricted by a set of constraints that limit the simultaneous values those variables may take.[csp-definition] The paradigm combines a high-level declarative specification with efficient specialized solving algorithms, and is widely used in problem-solving and combinatorial-optimization applications, sometimes drawing on techniques from Operational Research and Numerical Analysis.[csp-paradigm]

Classical constraint solving

A classical CSP solver operates on finite domains (integers or naturals) for the variables and is based on arc-consistency techniques. The solver maintains an internal representation of variable domains in order to handle all kinds of constraints. For example, the domain of an unsigned variable X constrained by X less than a constant C can be represented exactly by an interval [0 … C], whereas for more heavily constrained variables the interval representation is only an approximation of the effective domain.[csp-classical-solver]

Solving constraints in this classical setting consists of two main steps:[csp-solving-process]

1. Domain reduction — reducing the variable domains through local-propagation techniques.
2. Labeling phase — finding values for each constrained variable by iteratively grounding variables (fixing a value) and propagating the effect on other variable domains by re-applying arc-consistency techniques.

The labeling phase can be improved using heuristics for the order in which variables are considered and the order in which values are considered in the variable domains.[csp-solving-process]

STCS: a dedicated bit-aware constraint solver for hardware test generation

The TACAS 2003 evidence reports that the initial approach to solving a microprocessor test-generation problem was to use the existing solver GNU Prolog, but several drawbacks were identified when constraints include operations derived from a hardware description language:[stcs-motivation]

• Typed variables with fixed bit size and casting — casting between typed variables of different bit widths can result in information loss on domain values (e.g., an 8-bit unsigned variable equal to the cast of a 9-bit unsigned sum may have value 0 or 1 due to loss of the 9th bit). GNU Prolog also handles only natural, not signed-integer variables.
• Bit-manipulation constraints — bit extraction (e.g., X = Y[5:3]) and concatenation (e.g., X = (Y : Z)) require specific handling. Treating variables as bit vectors with constraints on individual bits prevents combining bit-level constraints with arithmetic constraints on the same variable, blocking useful domain reductions.
• Array manipulations — encoding arrays as lists of variables in the solver produces an impractically large number of variables when the array represents memory.

To address these limitations, a dedicated constraint solver called STCS was developed. STCS builds on the experience of GNU Prolog and introduces new specific constraints: logical and (X Eq Y and Z), logical shift (X Eq Y slr C), bit concatenation (X Eq Y concat Z), and bit extraction (X Eq Y extract C).[stcs-solver]

Internally, STCS uses two representations of each variable's domain:[stcs-representation]

• A simple interval representation (min, max) for arithmetic constraints.
• A bit representation that maintains the known bits of the bit-vector, for efficient handling of bit-based constraints.

Propagation is decomposed into bit propagation and interval propagation, with coherence maintained by two rules:[stcs-coherence]

• On each interval modification, the bit representation is checked for modification (propagating the most significant bit, 1 for the min value and 0 for the max value, into the bit representation).
• On each bit modification, a new [min, max] interval is computed according to the known bits.

The STCS solver was developed as a general library and is not limited to microprocessor test-generation problems; it can be reused in other domains or applications.[stcs-generality]

CSP in RISC-V test generation (RISCV-CTG)

The RISC-V Compatibility Test Generator (RISCV-CTG) is described as a constrained test generator that produces tests for the official RISC-V Architectural Test Suite and the RISCCOF test framework, all compliant with the official Test Format Spec.[riscv-ctg-overview] The CTG treats each cover-point in a Coverage Group Format (CGF) file as a constraint and uses CSP solvers from the python-constraint package to identify potential solutions.[riscv-ctg-csp]

The internal flow of the CTG proceeds in stages:[riscv-ctg-flow]

• Instr Attributes — instruction metadata stored in a YAML attributes file (xlen, ISA extension, operation, format type, legal register operands, legal operand value datasets, and an assembly template).
• Op and Val Combinations — the first two stages of the CTG receive the CGF file and identify solutions for operand and value combinations, carried out independently. If randomization is enabled, random solvers are employed at this stage.
• Instruction Creation — operand and value combination solutions are combined to fill all fields of the instruction under test.
• Signature and Test Register Allocation — each instruction instance is provided a signature register and an additional test register, allocated greedily to minimize register-pointer transfers.
• CorrectVal Generation — for arithmetic instructions (add, sll, sub, etc.), the operation field defined in the attributes YAML is used to compute expected results (a WIP feature).
• Generate Tests — final templates conforming to the Test Format Spec are used to generate assembly files.
• Parallel Runs — because CSP solver runtime can grow quickly with large data sets, the CTG internally allocates a cover-group in the CGF to an individual host process, parallelizing the runs.[riscv-ctg-parallel]

Random solvers

The documentation states that random solvers are essential for boosting speed. With loosely defined constraints in the CGF (e.g., rs1_val >0 and rs2_val>0), the solvers may spend considerable time finding all solutions when datasets are large. Random solvers, by contrast, provide the first solution that satisfies the problem and quit, saving time.[riscv-ctg-random]

A second benefit of using random values for loosely defined constraints is that it increases the chances of covering multiple cover-points (which may be presented later) in the same instruction, thereby reducing the number of instructions required to cover all cover-points in a cover-group of the CGF. The documentation emphasizes that at no point is coverage of the test compromised by the use of random solvers. A noted downside is that the same test cannot be reproduced again, but the typical user intent is to generate tests satisfying the cover-points, which CTG guarantees, so the reproducibility issue can be set aside.[riscv-ctg-random]

Theoretical extensions

Automatic CSP (AutCSP)

Recent work studies constraint languages defined by finite automata, giving rise to automata-based CSPs. The key notion is the Automatic Constraint Satisfaction Problem (AutCSP), in which both constraint languages and instances are specified by finite automata. This captures infinite yet finitely describable sets of relations, enabling concise representations of complex constraints. The work proves that checking whether an operation is a polymorphism of such a language can be done in polynomial time, extends Schaefer's Dichotomy Theorem to the AutCSP over the Boolean domain, and provides algorithms to decide tractability of some classes of AutCSPs over arbitrary finite domains via automatic polymorphisms. Crucially, the polynomial-time algorithms run on AutCSP instances that can be exponentially more succinct than their standard CSP counterparts.[autcsp]

Quantified CSP (QCSP)

A separate line of work studies the Quantified Constraint Satisfaction Problem, which evaluates a sentence with both quantifiers over relations from a constraint language, with conjunction as the only connective. The work shows that for any constraint language on a finite domain, the QCSP is either in Π_2^P or PSpace-complete, and constructs a constraint language on a 6-element domain for which the QCSP is Π_2^P-complete.[qcsp]

Research themes reflected in the evidence

The evidence identifies several technical themes from the CSP literature:

• Random solution generation: Dechter, Kask, Bin, and Emek are cited for work on "Generating random solutions for constraint satisfaction problems."[random-solutions-for-csp]
• Conditional CSP: Geller and Veksler are cited for "Assumption-based pruning in conditional CSP."[conditional-csp-pruning]
• Dynamic CSP: Mittal and Falkenhainer are cited for "Dynamic constraint satisfaction problems."[dynamic-csp]
• Constraint hierarchies: Borning, Freeman-Benson, and Willson are cited for "Constraint hierarchies."[constraint-hierarchies]
• Consistency in relation networks: Mackworth is cited for "Consistency in Networks of Relations."[consistency-networks]
• Stochastic CSP solving: Naveh is cited for a "Stochastic solver for constraint satisfaction problems with learning of high-level characteristics of the problem topography."[stochastic-csp-solver]

See also

• RISCV-CTG (RISC-V Compatibility Test Generator) — a tool that uses CSP solvers for RISC-V test generation
• Random Solver — a technique that implements CSP solving by returning the first satisfying solution
• Parallel Test Generation — a technique that uses CSP by parallelizing cover-group solving across host processes
• Hardware verification
• Random stimuli generation
• Random test program generation
• Conditional CSP
• Dynamic CSP
• Constraint hierarchies
• STCS (dedicated bit-aware constraint solver)
• GNU Prolog (general-purpose constraint solver)
• Automatic Constraint Satisfaction Problem (AutCSP)
• Quantified Constraint Satisfaction Problem (QCSP)