When a Constraint Satisfaction Problem (CSP) admits no solution, it can be useful to pinpoint which constraints are actually contradicting one another and make the problem infeasible.

This page proposes a recent heuristic-based approach to compute infeasible minimal subparts of discrete CSPs, also called Minimally Unsatisfiable Cores (MUCs).

This approach, called CB(full-wcore), is based on the heuristic exploitation of the number of times each constraint has been falsified during previous failed search steps. It appears to enhance the performance of the initial technique, which was the most efficient one until now.

Download the binaries

The proposed approach is composed of two main steps. The first aims at approximating a MUC within a CSP. The second step is actually a minimization technique which is able to efficiently extract a MUC from an some approximation previously computed. This minimization approach is an hybridization of the destructive (DS) and dichotomic methods (DC) (more details about those techniques here).

Binaries of CB(full-wcore) (also including the DS,DC minimizations) are available here.

The whole set of used benchmarks is available here. You can also download specific families of problems:

• ``Structured'' random problems, involving some (randomly generated) fragments linked to a main one using binary constraints. More details about this familly here.
  • composed-75-1-40
  • composed-75-1-2
  • composed-25-1-2
  • composed-25-1-25
  • composed-25-1-40
  • composed-75-1-25
  • composed-75-1-80
  • composed-25-1-80
• Radio Link Frequency Assignment Problem (RLFAP) is the task of assigning frequencies to a number of radio links in such a manner as to simultaneously satisfy a large number of constraints and use as few distinct frequencies as possible. Benchmarks provided by the CELAR (the French ``Centre d'Electronique de l'Armement''). More details about this familly here.
  • RLFAP
• Series of 3-SAT unsatisfiable instances have been converted into CSP instances using the dual method as described here.
  • ehi-85
  • ehi-90
• The Queens-Knights problem is the task of putting on a chessboard of size n*n, q queens and k knights such that no two queens can attack each other and all knights form a cycle (when considering knight moves). More details about this familly here.
  • Queen Knight Problem

Please note that both steps use for now the XML-based XCSP 1.0, also used for instance during the Second International Competition of CSP and Max-CSP Solvers. This format has now evolved toward a non compatible version (XCSP 2.1). However, a new version of CB(full-wcore) is being developped taking into account this new format. The released will be available soon, including both binaries and source code.

Extensive Experimental Results

CB(full-wcore) has been empirically evaluated through extensive experiments conducted on Pentium IV with 1GB of memory. The obtained results are available here.

How to read this table ?

First, information related to the tested problem are provided, through its name and the number of constraints it is composed of.

Second, full-wcore is compared to the original wcore. For each problem, the size of the obtained approximation is given (#UC) with the time spent for this computation in seconds.

Finally, we compared our new minimization method CB with the destructive (DS) and the dichotomic one (DC). After each approximation delivered by (full-)wcore, the 3 minimization methods has been used to deliver a MUC. For each experiment, the size (in term of number of constraints) of the obtained MUC is reported (#MUC), with the time in seconds. Moreover, the number of satisfiable (#runS) and unsatisfiable (#runU) calls to the complete solver are reported.

For each experiment, a limit of 3600 seconds of CPU has been respected. Beyond this limit, the note ``time out'' is reported.

Links

• Back to Cédric Piette Home Page
• Lens Computer Science Research Centre (CRIL) where I am working.