The MUC Extraction Page

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:

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.


Valid XHTML 1.0 Strict Valid CSS!