• Deutsch
Login

  • Home
  • Search
  • Browse
  • Publish
  • FAQ
  • CCS-Classification
  • I. Computing Methodologies
  • I.2 ARTIFICIAL INTELLIGENCE

I.2.3 Deduction and Theorem Proving (F.4.1)

  • Answer/reason extraction subscribe to RSS feed
  • Deduction (e.g., natural, rule-based) subscribe to RSS feed
  • Inference engines (NEW) subscribe to RSS feed
  • Logic programming subscribe to RSS feed
  • Mathematical induction subscribe to RSS feed
  • Metatheory** subscribe to RSS feed
  • Nonmonotonic reasoning and belief revision subscribe to RSS feed
  • Resolution subscribe to RSS feed

Refine

Author

  • Achterberg, Tobias (1)
  • Berthold, Timo (1)
  • Feydy, Thibaut (1)
  • Stuckey, Peter (1)

Year of publication

  • 2010 (1)
  • 2005 (1)

Document Type

  • ZIB-Report (2)

Language

  • English (2)

Has Fulltext

  • yes (2)

Is part of the Bibliography

  • no (2)

Keywords

  • Constraintprogrammierung (1)
  • Ganzzahlige Programmierung (1)
  • Konfliktanalyse (1)
  • Primalheuristik (1)
  • SAT (1)
  • branch and cut (1)
  • conflict analysis (1)
  • conflict learning (1)
  • constraint programming (1)
  • integer programming (1)
+ more

Institute

  • Mathematical Optimization (1)
  • ZIB Allgemein (1)

2 search hits

  • 1 to 2
  • BibTeX
  • CSV
  • RIS
  • XML
  • 10
  • 20
  • 50
  • 100

Sort by

  • Year
  • Year
  • Title
  • Title
  • Author
  • Author
Rapid Learning for Binary Programs (2010)
Berthold, Timo ; Feydy, Thibaut ; Stuckey, Peter
Learning during search allows solvers for discrete optimization problems to remember parts of the search that they have already performed and avoid revisiting redundant parts. Learning approaches pioneered by the SAT and CP communities have been successfully incorporated into the SCIP constraint integer programming platform. In this paper we show that performing a heuristic constraint programming search during root node processing of a binary program can rapidly learn useful nogoods, bound changes, primal solutions, and branching statistics that improve the remaining IP search.
Conflict Analysis in Mixed Integer Programming (2005)
Achterberg, Tobias
Conflict analysis for infeasible subproblems is one of the key ingredients in modern SAT solvers to cope with large real-world instances. In contrast, it is common practice for today's mixed integer programming solvers to just discard infeasible subproblems and the information they reveal. In this paper we try to remedy this situation by generalizing the SAT infeasibility analysis to mixed integer programming. We present heuristics for branch-and-cut solvers to generate valid inequalities from the current infeasible subproblem and the associated branching information. SAT techniques can then be used to strengthen the resulting cuts. We performed computational experiments which show the potential of our method: On feasible MIP instances, the number of required branching nodes was reduced by 50\% in the geometric mean. However, the total solving time increased by 15\%. on infeasible MIPs arising in the context of chip verification, the number of nodes was reduced by 90\%, thereby reducing the solving time by 60\%.
  • 1 to 2

OPUS4 Logo

  • Contact
  • Impressum und Datenschutz
  • Sitelinks