Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Exploiting Circuit Duality to Speed Up SAT
 
conference paper

Exploiting Circuit Duality to Speed Up SAT

Amaru, Luca
•
Gaillardon, Pierre-Emmanuel
•
Mishchenko, Alan
Show more
2015
Proceedings of the IEEE Computer Society Annual Symposium on VLSI (ISVLSI)
IEEE Computer Society Annual Symposium on VLSI (ISVLSI)

In this paper, we establish a non-trivial duality between tautology and contradiction check to speed up circuit SAT. Tautology check determines if a logic circuit is true in every possible interpretation. Analogously, contradiction check determines if a logic circuit is false in every possible interpretation. A trivial transformation of a (tautology, contradiction) check problem into a (contradiction, tautology) check problem is the inversion of all outputs in a logic circuit. In this work, we show that exact logic inversion is not necessary. We give operator switching rules that selectively exchange tautologies with contradictions, and vice versa. Our approach collapses into logic inversion just for tautology and contradiction extreme points but generates non-complementary logic circuits in the other cases. This property enables computing benefits when an alternative, but equisolvable, instance of a problem is easier to solve than the original one. As a case study, we investigate the impact on SAT. There, our methodology generates a dual SAT instance solvable in parallel with the original one. This concept can be used on top of any other SAT approach and does not impose much overhead, except having to run two solvers instead of one, which is typically not a problem because multi-cores are widespread and computing resources are inexpensive. Experimental results show a 25% speed-up of SAT in a concurrent execution scenario. Also, statistical experiments confirmed that our runtime reduction is not of the random variation type.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

ISLVSI15.pdf

Access type

openaccess

Size

787.38 KB

Format

Adobe PDF

Checksum (MD5)

c0eb6be8ff520d3419d7c2cfa687fa42

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés