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: 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:

 (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 = {?},