Solving XCSP3 Constraint Problems Using Tools from Software Verification

EasyChair Preprint 8679

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

@booklet{EasyChair:8679,
  author    = {Martin Mariusz Lester},
  title     = {Solving XCSP3 Constraint Problems Using Tools from Software Verification},
  howpublished = {EasyChair Preprint 8679},
  year      = {EasyChair, 2022}}