Arist Kojevnikov,System Engineer at the Intel Mobile Communications GmbH Email: first name at domain |

- Verification
- Circuit Complexity
- Semialgebraic proof systems
- Algorithms for the Boolean satisfiability problem (SAT)
- Exact algorithms

- Optimal Circuit Problem to SAT converter
- Circuit descriptions of multipliers in ISCAS format
- BASolver, a SAT solver based on boolean-algebraic approach
- UnitWalk, a SAT solver using unit clause elimination and random walk
- Semialgebraic Prover, a first-order theorem prover based on semialgebraic proof systems
- Automated proofs of upper bounds for NP-hard problems

This homepage is physically located in Laboratory of Mathematical Logic of Steklov Institute of Mathematics at St.Petersburg.