The (un)reasonable (in)effectiveness of theory for Sat solvers

Cite

Related Material

Banff International Research Station (BIRS) for Mathematical Innovation and Discovery

Buss, Sam

Formal Metadata

Title

The (un)reasonable (in)effectiveness of theory for Sat solvers

Title of Series

Theory and Practice of Satisfiability Solving (18w5208)

Number of Parts

Author

Buss, Sam

License

CC Attribution - NonCommercial - NoDerivatives 4.0 International:
You are free to use, copy, distribute and transmit the work or content in unchanged form for any legal and non-commercial purpose as long as the work is attributed to the author in the manner specified by the author or licensor.

Identifiers

10.5446/59376 (DOI)

Publisher

Banff International Research Station (BIRS) for Mathematical Innovation and Discovery

Release Date

2018

Language

English

Content Metadata

Subject Area

Computer Science Mathematics

Genre

Workshop/Interactive Format Lecture

Abstract

There is an increasing interplay between practical implementations of Sat Solvers and theoretical results about proof complexity. In some cases, theory can be useful for understanding or designing Sat solvers, but the connections are not as strong as might be wished for. This talk will discuss these issues, and make some suggestions for further research directions both for theoreticians and for practitioners.