| Most problems, from theoretical problems in combinatorics to real-world applications, comprise hidden structural properties not directly captured by the problem definition. A key to the recent progress in automated reasoning and combinatorial optimization has been to automatically uncover and exploit this hidden problem structure, resulting in a dramatic increase in the scale and complexity of the problems within our reach. The most complex tasks, however, still require human abilities and ingenuity.;This dissertation studies how we can leverage human insights about the structure of the problem to effectively complement and dramatically boost stateof- the-art optimization techniques. The proposed framework couples the concept of streamlined combinatorial search, a strong branching mechanism that evaluates and propagates a set of constraints corresponding to suggested properties, with a human computation component, in a complementary, iterative approach. The human computation component is used to identify possible patterns in the problem instance and suggest insightful properties or potential hidden structure of the instance. I demonstrate the effectiveness of the approach with a series of scientific discoveries, in areas such as graph theory, combinatorics, and discrepancy theory as well as materials science, experimental design and conservation biology. |
