Accessibility navigation

CoPTIC: constraint programming translated into C

Lester, M. M. ORCID: (2023) CoPTIC: constraint programming translated into C. In: Sankaranarayanan, S. and Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. Lecture Notes in Computer Science (13994). Springer, Cham. ISBN 9783031308192

Text (Open Access) - Published Version
· Available under License Creative Commons Attribution.
· Please see our End User Agreement before downloading.

[img] Text - Accepted Version
· Restricted to Repository staff only


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

To link to this item DOI: 10.1007/978-3-031-30820-8_13


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:Book or Report Section
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
Publisher:Springer, Cham


Downloads per month over past year

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

Page navigation