Encodings and representations play an important role both in theory and practice. From the point of view of computational complexity, the theory of efficient reductions is precisely the claim that any problem from a complexity class can be encoded as an instance of its canonical complete problem. On the other hand, it is not hard to imagine that from the point of view of solving real-word instances by a computer, certain encodings would seem more desirable than others. Even in theory, if we care to understand the power of classes of algorithms from certain families, then the way the input is encoded could play an important role. The range of examples to which this claim applies goes from algorithms based on proof-search for resolution and related proof systems, through algorithms based on linear, integer and non-linear programming, to logic-based procedures that are required to preserve the level of abstraction in the input. The purpose of this workshop is to bring together experts in logic, complexity and algorithms, both theoreticians and practitioners, who deal with questions such as symmetry-handling and breaking in the input, the succinctness in expressive power of Boolean formulas, decision diagrams and other low-level models of computation, the expressive power of logical languages, and the reasoning power of proof methods.
All events take place in the Calvin Lab auditorium.
Further details about this workshop will be posted in due course. Enquiries may be sent to the organizers workshop-sat3 [at] lists.simons.berkeley.edu (at this address).