Solving hard industrial combinatorial problems with SAT

摘要: The topic of this thesis is the development SAT-based techniques and tools for solving industrial combinatorial problems. First, it describes architecture state-of-the-art SAT SMT Solvers based on classical DPLL procedure. These systems can be used as black boxes However, sometimes we increase their efficiency with slight modifications basic algorithm. Therefore, study adjusting to specific problems first goal thesis. Namely, only deal propositional logic. For general problems, two different approaches are possible: - Reducing complex constraints into clauses. Enriching Solver language. approach corresponds encoding constraint SAT. second one using propagators, basis Solvers. Regarding approach, in document improve most important constraints: cardinality pseudo-Boolean constraints. After that, present a new mixed called lazy decomposition, which combines advantages encodings propagators. other part uses these theoretical improvements We give method efficiently scheduling some professional sport leagues results promising show that valid chaotical behavior CDCL-based due VSIDS heuristics makes difficult obtain similar solution This may inconvenient real-world since user expects solutions when problem specification. In order overcome limitation, have studied solved close problem, i.e., quickly finding considered.