Download PDFOpen PDF in browser

Solving XCSP3 Constraint Problems Using Tools from Software Verification

EasyChair Preprint 8679

3 pagesDate: August 12, 2022

Abstract

Since 2012, the Software Verification Competition (SV-COMP) has evaluated the performance of a wide range of software verification tools, using a wide range of techniques and representations. These include SAT/SMT solving, abstract interpretation, Constrained Horn Clause solving and finite state automata.

The XCSP3 constraint format serves as an intermediate language for constraint problems. When trying to solve a particular problem, one often wishes to trial a range of techniques to see which one is initially most promising. Unfortunately, there might not always be an implementation of the desired technique for one's formulation.

We propose to address this problem by encoding XCSP3 problems as C program software verification problems. This grants the ability to trial all techniques implemented in SV-COMP entries. We should not expect the encoding to be efficient, but it may be sufficient to identify the most promising techniques.

Keyphrases: XCSP3, automatic reformulation, software verification

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:8679,
  author    = {Martin Mariusz Lester},
  title     = {Solving XCSP3 Constraint Problems Using Tools from Software Verification},
  howpublished = {EasyChair Preprint 8679},
  year      = {EasyChair, 2022}}
Download PDFOpen PDF in browser