Skip to main navigation Skip to search Skip to main content

Novel integration of Dimetheus and WalkSAT solvers for κ-SAT filter construction

  • Stony Brook University

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations

Abstract

This paper describes a novel approach used to integrate two leading satisfiability (SAT) solvers, Dimetheus and WalkSAT, into a system to provide users with solver selection and solution customization capabilities. The two solvers are efficient for two different cases, have different execution procedures and generate a single solution from a single line of command. This integration provides the most efficient way to find multiple random solutions of any set membership problem from a common single line of command. To build an effective k-SAT filter, multiple random solutions are essential. The integration also provides a unified solution output format rather than two different output formats of two solvers. The theoretical approach and a practical C program were developed and tested during the work in an on-going project to build world's first practical k-SAT filter for deep packet inspection in network intrusion detection systems at Stony Brook University.

Original languageEnglish
Title of host publication2017 IEEE Long Island Systems, Applications and Technology Conference, LISAT 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781538638873
DOIs
StatePublished - Aug 3 2017
Event2017 IEEE Long Island Systems, Applications and Technology Conference, LISAT 2017 - Farmingdale, United States
Duration: May 5 2017 → …

Publication series

Name2017 IEEE Long Island Systems, Applications and Technology Conference, LISAT 2017

Conference

Conference2017 IEEE Long Island Systems, Applications and Technology Conference, LISAT 2017
Country/TerritoryUnited States
CityFarmingdale
Period05/5/17 → …

Keywords

  • Dimetheus
  • k-SAT filtes
  • SAT solver
  • Satisfiability filters
  • WalkSAT

Fingerprint

Dive into the research topics of 'Novel integration of Dimetheus and WalkSAT solvers for κ-SAT filter construction'. Together they form a unique fingerprint.

Cite this