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:








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:

18 September 2019

Event End Date:

18 September 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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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