English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Towards Conflict-driven Learning for Virtual Substitution

Korovin, K., Košta, M., & Sturm, T. (2014). Towards Conflict-driven Learning for Virtual Substitution. In V. P. Gerdt, W. Koepf, W. M. Seiler, & E. V. Vorozhtsov (Eds.), Computer Algebra in Scientific Computing (pp. 256-270). Berlin: Springer. doi:10.1007/978-3-319-10515-4_19.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Korovin, Konstantin1, Author           
Košta, Marek2, Author           
Sturm, Thomas2, Author           
Affiliations:
1External Organizations, ou_persistent22              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 Abstract: We consider satisfiability modulo theory-solving for linear real arithmetic. Inspired by related work for the Fourier–Motzkin method, we combine virtual substitution with learning strategies. For the first time, we present virtual substitution—including our learning strategies—as a formal calculus. We prove soundness and completeness for that calculus. Some standard linear programming benchmarks computed with an experimental implementation of our calculus show that the integration of learning techniques into virtual substitution gives rise to considerable speedups. Our implementation is open-source and freely available.

Details

show
hide
Language(s): eng - English
 Dates: 20142014
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: DOI: 10.1007/978-3-319-10515-4_19
BibTex Citekey: KorovinCASC2014
 Degree: -

Event

show
hide
Title: International Workshops on Computer Algebra in Scientific Computing
Place of Event: Warsaw, Poland
Start-/End Date: 2014-09-08 - 2014-09-12

Legal Case

show

Project information

show

Source 1

show
hide
Title: Computer Algebra in Scientific Computing
  Subtitle : 16th International Workshop, CASC 2014 ; Warsaw, Poland, September 8-12, 2014 ; Proceedings
  Abbreviation : CASC 2014
Source Genre: Proceedings
 Creator(s):
Gerdt, Vladimir P.1, Editor
Koepf, Wolfram1, Editor
Seiler, Werner M.1, Editor
Vorozhtsov, Evgenii V.1, Editor
Affiliations:
1 External Organizations, ou_persistent22            
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 256 - 270 Identifier: ISBN: 978-3-319-10514-7

Source 2

show
hide
Title: Lecture Notes in Computer Science
  Abbreviation : LNCS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 8660 Sequence Number: - Start / End Page: - Identifier: -