Perceptron Learning of SAT

Abstract : Boolean satisfiability (SAT) as a canonical NP-complete decision problem is one of the most important problems in computer science. In practice, real-world SAT sentences are drawn from a distribution that may result in efficient algorithms for their solution. Such SAT instances are likely to have shared characteristics and substructures. This work approaches the exploration of a family of SAT solvers as a learning problem. In particular, we relate polynomial time solvability of a SAT subset to a notion of margin between sentences mapped by a feature function into a Hilbert space. Provided this mapping is based on polynomial time computable statistics of a sentence, we show that the existence of a margin between these data points implies the existence of a polynomial time solver for that SAT subset based on the Davis-Putnam-Logemann-Loveland algorithm. Furthermore, we show that a simple perceptron-style learning rule will find an optimal SAT solver with a bounded number of training updates. We derive a linear time computable set of features and show analytically that margins exist for important polynomial special cases of SAT. Empirical results show an order of magnitude improvement over a state-of-the-art SAT solver on a hardware verification task.
Type de document :
Communication dans un congrès
Neural Information Processing Systems, Dec 2012, Lake Tahoe, United States. pp.2780-2788, 2012
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger
Contributeur : Matthew Blaschko <>
Soumis le : jeudi 4 octobre 2012 - 11:34:20
Dernière modification le : jeudi 7 février 2019 - 17:29:14
Document(s) archivé(s) le : vendredi 16 décembre 2016 - 18:58:34


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-00738219, version 1



Alex Flint, Matthew Blaschko. Perceptron Learning of SAT. Neural Information Processing Systems, Dec 2012, Lake Tahoe, United States. pp.2780-2788, 2012. 〈hal-00738219〉



Consultations de la notice


Téléchargements de fichiers