Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop
Show entries of:
this year
(2019) |
last year
(2018) |
two years ago
(2017) |
Notes URL
Action:
login to update
Options:
Goto entry point
Author, Editor
Author(s):
Barth, Peter
dblp
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
URL of the conference:
URL for downloading the paper:
Event Address*:
Marseille, France
Language:
English
Event Date*
(no longer used):
1993
Organization:
Event Start Date:
13 November 2019
Event End Date:
13 November 2019
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
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