SCSat: A soft constraint guided SAT solver

Hiroshi Fujita, Miyuki Koshimura, Ryuzo Hasegawa

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

SCSat is a SAT solver aimed at quickly finding a model for hard satisfiable instances using soft constraints. Soft constraints themselves are not necessarily maximally satisfied and may be relaxed if they are too strong to obtain a model. Appropriately given soft constraints can reduce search space drastically without losing many models, thus help find a model faster. In this way, we have succeeded to obtain several rare Ramsey graphs which contribute to raise the known best lower bound for the Ramsey number R(4,8) from 56 to 58.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing, SAT 2013 - 16th International Conference, Proceedings
Pages415-421
Number of pages7
DOIs
Publication statusPublished - 2013
Event16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013 - Helsinki, Finland
Duration: Jul 8 2013Jul 12 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7962 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013
Country/TerritoryFinland
CityHelsinki
Period7/8/137/12/13

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'SCSat: A soft constraint guided SAT solver'. Together they form a unique fingerprint.

Cite this