Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Matthew Blaschko Connect in order to contact the contributor
Submitted on : Thursday, October 4, 2012 - 11:34:20 AM
Last modification on : Friday, January 21, 2022 - 3:01:25 AM
Long-term archiving on: : Friday, December 16, 2016 - 6:58:34 PM


Files produced by the author(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. ⟨hal-00738219⟩



Record views


Files downloads