Speaker: Jan Horáček
Abstract: The Boolean satisfiability problem (SAT) and polynomial system solving over a finite field are two fundamental problems of propositional logic and computational commutative algebra, respectively. Solvers that allow us to describe the set of zeros of a given ideal generated by Boolean polynomials are referred to as algebraic solvers, whereas SAT solvers search for a satisfying assignment of a CNF formula. In several ways how to encode the same problem into conjunctive normal form (CNF) and the Boolean polynomials (ANF) are discussed. Thus one can solve the problem with an algebraic or a SAT solver individually. There exist conversion methods that transform a Boolean system to a CNF formula (and vice versa) such that the rational zeros of the system correspond to the satisfying assignments of the logical formula. Thus we may run both solvers in parallel and let them interchange the \new information", or one solver can dynamically help the another one with a certain sub problem, etc. In this talk we describe an automatic framework which combines the power of the Boolean Border Basis Algorithm and the SAT solver antom in detail and we explain the design of the actual communication process between the two solvers. We report some preliminary results about speed-ups of the overall solving time we could achieve.
Biography: Jan Horáček is a research fellow and a lecturer in the Department of Symbolic Computation and the Department of Computer Engineering at University Passau in Germany since 2015. He received a master's degree in Mathematics in 2014 from Charles University in Prague. His research interests includes developing algebraic solvers and applying them in cryptanalysis, mainly in algebraic fault attacks.
All are welcome to attend!