Combining graph theory and linear algebra, we study SAT problems of low “linear algebra complexity”, considering formulas with bounded hermitian rank. We show polynomial time SAT decision of the class of formulas with hermitian rank at most one, applying methods from hypergraph transversal theory. Applications to heuristics for SAT algorithms and to the structure of minimally unsatisfiable clause-sets are discussed.
Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank / Galesi, Nicola; Kullmann, O.. - STAMPA. - 3542:(2004), pp. 89-104. (Intervento presentato al convegno The International Conferences on Theory and Applications of Satisfiability Testing (SAT) tenutosi a Vancouver (BC), Canada) [10.1007/11527695_25].
Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank
GALESI, NICOLA;
2004
Abstract
Combining graph theory and linear algebra, we study SAT problems of low “linear algebra complexity”, considering formulas with bounded hermitian rank. We show polynomial time SAT decision of the class of formulas with hermitian rank at most one, applying methods from hypergraph transversal theory. Applications to heuristics for SAT algorithms and to the structure of minimally unsatisfiable clause-sets are discussed.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
