Accessibility navigation

CoPTIC: constraint programming translated into C

Lester, M. ORCID: (2022) CoPTIC: constraint programming translated into C. In: TACAS 2023: 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 24-27 Apr 2023, Paris, France. (In Press)

[img] Text - Accepted Version
· Restricted to Repository staff only
· The Copyright of this document has not been checked yet. This may affect its availability.


It is advisable to refer to the publisher's version if you intend to cite from this work. See Guidance on citing.


Constraint programming systems allow a diverse range of problems to be modelled and solved. Most systems require the user to learn a new constraint programming language, which presents a barrier to novice and casual users. To address this problem, we present the CoPTIC constraint programming system, which allows the user to write a model in the well-known programming language C, augmented with a simple API to support using a guess-and-check paradigm. The resulting model is at most as complex as an ordinary C program that uses naive brute force to solve the same problem. CoPTIC uses the bounded model checker CBMC to translate the model into a SAT instance, which is solved using the SAT solver CaDiCaL. We show that, while this is less efficient than a direct translation from a dedicated constraint language into SAT, performance remains adequate for casual users. CoPTIC supports constraint satisfaction and optimisation problems, as well as enumeration of multiple solutions. After a solution has been found, CoPTIC allows the model to be run with the solution; this makes it easy to debug a model, or to print the solution in any desired format.

Item Type:Conference or Workshop Item (Paper)
Divisions:Science > School of Mathematical, Physical and Computational Sciences > Department of Computer Science
ID Code:110428
Uncontrolled Keywords:constraint programming bounded model-checking C programming language

University Staff: Request a correction | Centaur Editors: Update this record

Page navigation