|
|
Model building using CSP
Peterová, Alena ; Stanovský, David (advisor) ; Kazda, Alexandr (referee)
In the present work, we study algorithms for building finite models of sets of first-order axioms with the aim of proposing and implementing a new method, based on translation onto constraint satisfaction problem (CSP). In the theoretical part, we describe the standard MACE-style method, based on translating problems onto SAT, and advanced techniques that improve the effectiveness of this method: clause splitting, term definitions and static symmetry reduction. Next, we propose an alternative method, which translates problems onto CSP in a similar way. In addition, we have newly proposed a static symmetry reduction technique for binary functions. Next, we describe an implementation of the alternative method using a CSP-modelling language MiniZinc and a CSP-solver Gecode. Finally, we compare performance of our model finder against state-of-the-art representatives of standard methods, systems Paradox and Mace4.
|
|
|
Methods of proving lower bounds in propositional logic
Peterová, Alena ; Pudlák, Pavel (advisor) ; Krajíček, Jan (referee)
In the present work, we study the propositional proof complexity. First, we prove an exponential lower bound on the complexity of resolution applying directly Razborov's approximation method, which was previously used only for bounds on the size of monotone circuits. Next, we use the approximation method for a new proof of an exponential lower bound on the complexity of random resolution refutations. That should have further applications in separating some theories in bounded arithmetic. In both cases, we use a problem from the graph theory called Broken Mosquito Screens. Finally, we state a conjecture that the approximation method is applicable even for stronger propositional proof systems, for example Cutting Plane Proofs. Powered by TCPDF (www.tcpdf.org)
|
|
|
Model building using CSP
Peterová, Alena ; Stanovský, David (advisor) ; Kazda, Alexandr (referee)
In the present work, we study algorithms for building finite models of sets of first-order axioms with the aim of proposing and implementing a new method, based on translation onto constraint satisfaction problem (CSP). In the theoretical part, we describe the standard MACE-style method, based on translating problems onto SAT, and advanced techniques that improve the effectiveness of this method: clause splitting, term definitions and static symmetry reduction. Next, we propose an alternative method, which translates problems onto CSP in a similar way. In addition, we have newly proposed a static symmetry reduction technique for binary functions. Next, we describe an implementation of the alternative method using a CSP-modelling language MiniZinc and a CSP-solver Gecode. Finally, we compare performance of our model finder against state-of-the-art representatives of standard methods, systems Paradox and Mace4.
|
guest ::
RSS feed.