MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Barth, Peterdblp
Editor(s):
Benhamou, F.
Colmerauer, A.
Smolka, Gert		dblp
dblp
dblp
BibTeX cite key*:
Barth93c
Title, Booktitle
Title*:
A Complete Symbolic 0-1 Constraint Solver
Booktitle*:
3rd Workshop on Constraint Logic Programming (WCLP '93)
Event, URLs
Conference URL::
Downloading URL:
Event Address*:
Marseille, France
Language:
English
Event Date*
(no longer used):
1993
Organization:
Event Start Date:
29 April 2024
Event End Date:
29 April 2024
Publisher
Name*:
Faculty of Luminy
URL:
Address*:
Marseille, France
Type:
Vol, No, Year, pp.
Series:
Volume:
Number:
Month:
March
Pages:
?
Year*:
1993
VG Wort Pages:
ISBN/ISSN:
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We present a complete symbolic 0-1 constraint solver for a system of linear 0-1 inequalities. We give first a method ${\cal T}$ which transforms arbitrary linear 0-1 inequalities into a set $S$ of {\em extended clauses\/} of the form $L1 + \ldots + L_n \geq d$, where the $L_i$ are literals. With the deductive system called {\em generalized resolution\/} (Hooker, 1992) we can then then solve such a set of extended clauses. The solved form is a set of {\em prime\/} extended clauses $\pi(S)$ which has the following key property. If $S$ dominates an extended clause $C$ then there is a single extended clause $D \in \pi(S)$ such that $D$ dominates $C$. Therefore $S$ is insatisfiable iff $0 \geq 1 \in \pi(S)$. So the solved form provides us with an easy test for satisfiability and logical entailment which is useful in the context of constraint logic programming. The basic deduction rules of {\em generalized resolution\/} are a generalization of {\em resolution\/} and {\em diagonal sum\/}. We show how to use the transformation method ${\cal T}$ for implementing these basic deduction rules. For that we use the fact that the rules generate a subset of all possible Gomory rank-1 cuts. We then find a correspondance between these cuts and the result of ${\cal T}$ applied to the linear combination of the involved extended clauses.
Download
Access Level:

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:
CCL bibliography



BibTeX Entry:
@INPROCEEDINGS{Barth93c,
AUTHOR = {Barth, Peter},
 EDITOR = {Benhamou, F. and Colmerauer, A. and Smolka, Gert},
 TITLE = {A Complete Symbolic 0-1 Constraint Solver},
 BOOKTITLE = {3rd Workshop on Constraint Logic Programming (WCLP '93)},
 PUBLISHER = {Faculty of Luminy},
 YEAR = {1993},
 PAGES = {?},
 ADDRESS = {Marseille, France},
 MONTH = {March},
}

Entry last modified by Christine Kiesel, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Brahm		Created
01/14/1995 06:50:35 PM
Revisions
10.
9.
8.
7.
6.		Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE		Edit Dates
03.09.2001 17:08:02
03.09.2001 17:07:53
01/03/95 11:53:02
14/02/95 10:45:37
25/01/95 20:25:28