Generation of Oriented Matroids Using Satisfiability Solvers

摘要

Oriented matroids are a combinatorial abstraction of finite sets of points in IR~n. They have been used to study various problems in discrete and computational geometry (for more material on oriented matroids, see [1,2]). A number of methods to generate oriented matroids have been proposed (for instance in [4,8-10]) as these methods can be used as a building block for the algorithmic treatment of some hard problems: Algorithms to generate oriented matroids have for instance been used to decide whether certain 4-polytopes exist. For these questions it is important to have effective algorithms for the generation of oriented matroids. We propose to use satisfiability solvers to generate oriented matroids. We have adapted this approach to generate oriented matroids that satisfy certain geometric constraints. Even though one can use the generated oriented matroids as a first step to find realizations (see for instance), we will only focus on non-realizability results.