An explicit semidefinite characterization of satisfiability for Tseitin instances on toroidal grid graphs
| Autor: | Miguel F. Anjos |
|---|---|
| Rok vydání: | 2006 |
| Předmět: |
Semidefinite programming
Semidefinite embedding Discrete mathematics Applied Mathematics Dimension (graph theory) Computer Science::Computational Complexity Mathematical proof Satisfiability Combinatorics Artificial Intelligence Computer Science::Logic in Computer Science Discrete optimization Combinatorial optimization Boolean satisfiability problem Mathematics |
| Zdroj: | Annals of Mathematics and Artificial Intelligence. 48:1-14 |
| ISSN: | 1573-7470 1012-2443 |
| DOI: | 10.1007/s10472-006-9041-2 |
| Popis: | This paper is concerned with the application of semidefinite programming to the satisfiability problem, and in particular with using semidefinite liftings to efficiently obtain proofs of unsatisfiability. We focus on the Tseitin satisfiability instances which are known to be hard for many proof systems. For Tseitin instances based on toroidal grid graphs, we present an explicit semidefinite programming problem with dimension linear in the size of the Tseitin instance, and prove that it characterizes the satisfiability of these instances, thus providing an explicit certificate of satisfiability or unsatisfiability. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink