CoPTIC: constraint programming translated into C

Lester, M. M. ORCID: https://orcid.org/0000-0002-2323-1771 (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 doi: 10.1007/978-3-031-30820-8_13

Abstract/Summary

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
URI	https://reading-clone.eprints-hosting.org/id/eprint/110428
Identification Number/DOI	10.1007/978-3-031-30820-8_13
Refereed	Yes
Divisions	Science > School of Mathematical, Physical and Computational Sciences > Department of Computer Science
Uncontrolled Keywords	constraint programming bounded model-checking C programming language
Publisher	Springer, Cham
Download/View statistics	View download statistics for this item