Do Portfolio Solvers Harm?
This content discusses the impact of portfolio solvers on automated reasoning, focusing on the work of Christoph Weidenbach. It explores topics such as CDCL reasoning, Bernays-Schoenfinkel calculi, and the potential of model portfolio calculus. The research direction towards SM portfolio solving is highlighted for advancements in automated reasoning.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Do Portfolio Solvers Harm? Christoph Weidenbach
CDCL Reasoning Ordering Portfolio Ordered Resolution Not Redundant Christoph Weidenbach ARCADE 2017 2
Bernays-Schoenfinkel (BS) NEXPTIME-Complete Target language for a number of decidable logics: Description Logics, Modal Logics, Monadic Fragment, Ontology Languages QBF, There is no Prime Calculus. Christoph Weidenbach ARCADE 2017 3
BS to SAT CDCL upfront instantiation overhead no redundant inferences long proofs large models Christoph Weidenbach ARCADE 2017 4
BS via InstGen iProver no upfront instantiation overhead redundant inferences long proofs large models Christoph Weidenbach ARCADE 2017 5
BS via NRCL no instantiation no redundant inferences short proofs possibly compact models non-linear computations Christoph Weidenbach ARCADE 2017 6
BS Calculi & End [BaumgartnerFuchsTinelli 2006] [GanzingerKorovin 2003] [PiskacMouraBjorner 2010] [ClaessenSrensson 2003] [BonacinaPlaisted 2016] [PerezVoronkov 2008] [SudaWeidenbachWischnewski 2010] [AlagiWeidenbach 2015] Can we have a Model Portfolio Calculus in the same way CDCL is an Ordering Portfolio Implementation of Ordered Resolution? Research in the Direction of SM Portfolio Solving has more potential for Advances in Automated Reasoning Than Research in SS Portfolio Solving Thanks for your attention. Christoph Weidenbach ARCADE 2017 7
