A Portfolio Approach to Solving SMT Problems
Mohammad Abdulaziz (ANU)
LOGIC AND COMPUTATION SEMINARDATE: 2013-04-23
TIME: 14:00:00 - 15:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
We describe an approach to solving Satisfiability Modulo Theory (SMT) problems. SMT has application in formal verification of software and hardware. It is also applied to different decision and optimization problems, such as graph colouring, traveling sales person, networking problems, etc. We developed a novel system for solving such problems. A portfolio approach, it is a meta-algorithm devised to choose between various algorithms that can solve the problem at hand. Our portfolio comprises five contesting solvers from the SMT competition in 2011. The choice of which solver to use is made according to the expected performance (i.e. "hardness") of the problem instance. The focus of my talk is our statistical hardness model, especially the model features, and the machine learning technique which we use for hardness inference.
