Efficient Encodings from CSP into SAT, and from MaxCSP into MaxSAT.
Saved in:
| Title: | Efficient Encodings from CSP into SAT, and from MaxCSP into MaxSAT. |
|---|---|
| Authors: | ARGELICH, JOSEP1, CABISCOL, ALBA1, LYNCE, INÊS2, MANYÀ, FELIP3 felip@iiia.csic.es |
| Source: | Journal of Multiple-Valued Logic & Soft Computing. 2012, Vol. 19 Issue 1-3, p3-23. 21p. 3 Charts. |
| Subjects: | CSP (Computer program language), Computer simulation, Empirical research, Performance evaluation, Machine learning |
| Abstract: | We first survey existing encondings from CSP into SAT, and define two new encodings: the minimal support encoding and the interval-based support encoding. Then, we study how the existing and new encodings from CSP into SAT can be extended for encoding MaxCSP into Partial MaxSAT. Finally, we report on the empirical investigation. The obtained results provide empirical evidence of the good performance profile of the new encodings on SAT solvers such as MiniSat and PrecoSAT that incorporate conflict-clause learning, as well as when they are used to encode MaxCSP into Partial MaxSAT and are solved with MaxSAT solvers such as MSUnCore, SAT4J-Maxsat and WMaxSatz. [ABSTRACT FROM AUTHOR] |
| Copyright of Journal of Multiple-Valued Logic & Soft Computing is the property of Old City Publishing, Inc. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 109040226 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Efficient Encodings from CSP into SAT, and from MaxCSP into MaxSAT. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22ARGELICH%2C+JOSEP%22">ARGELICH, JOSEP</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22CABISCOL%2C+ALBA%22">CABISCOL, ALBA</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22LYNCE%2C+INÊS%22">LYNCE, INÊS</searchLink><relatesTo>2</relatesTo><br /><searchLink fieldCode="AR" term="%22MANYÀ%2C+FELIP%22">MANYÀ, FELIP</searchLink><relatesTo>3</relatesTo><i> felip@iiia.csic.es</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Multiple-Valued+Logic+%26+Soft+Computing%22">Journal of Multiple-Valued Logic & Soft Computing</searchLink>. 2012, Vol. 19 Issue 1-3, p3-23. 21p. 3 Charts. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22CSP+%28Computer+program+language%29%22">CSP (Computer program language)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+simulation%22">Computer simulation</searchLink><br /><searchLink fieldCode="DE" term="%22Empirical+research%22">Empirical research</searchLink><br /><searchLink fieldCode="DE" term="%22Performance+evaluation%22">Performance evaluation</searchLink><br /><searchLink fieldCode="DE" term="%22Machine+learning%22">Machine learning</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: We first survey existing encondings from CSP into SAT, and define two new encodings: the minimal support encoding and the interval-based support encoding. Then, we study how the existing and new encodings from CSP into SAT can be extended for encoding MaxCSP into Partial MaxSAT. Finally, we report on the empirical investigation. The obtained results provide empirical evidence of the good performance profile of the new encodings on SAT solvers such as MiniSat and PrecoSAT that incorporate conflict-clause learning, as well as when they are used to encode MaxCSP into Partial MaxSAT and are solved with MaxSAT solvers such as MSUnCore, SAT4J-Maxsat and WMaxSatz. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Journal of Multiple-Valued Logic & Soft Computing is the property of Old City Publishing, Inc. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=109040226 |
| RecordInfo | BibRecord: BibEntity: Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 21 StartPage: 3 Subjects: – SubjectFull: CSP (Computer program language) Type: general – SubjectFull: Computer simulation Type: general – SubjectFull: Empirical research Type: general – SubjectFull: Performance evaluation Type: general – SubjectFull: Machine learning Type: general Titles: – TitleFull: Efficient Encodings from CSP into SAT, and from MaxCSP into MaxSAT. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: ARGELICH, JOSEP – PersonEntity: Name: NameFull: CABISCOL, ALBA – PersonEntity: Name: NameFull: LYNCE, INÊS – PersonEntity: Name: NameFull: MANYÀ, FELIP IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 06 Text: 2012 Type: published Y: 2012 Identifiers: – Type: issn-print Value: 15423980 Numbering: – Type: volume Value: 19 – Type: issue Value: 1-3 Titles: – TitleFull: Journal of Multiple-Valued Logic & Soft Computing Type: main |
| ResultId | 1 |
