About: Designing New Phase Selection Heuristics

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Designing New Phase Selection Heuristics Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : wasabi.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	Designing New Phase Selection Heuristics
Creator	Meel, Kuldeep Shaw, Arijit
topic	covid:012168d42a11ee62575548f7c7dde4924b0711de#this
Source	PMC
abstract	CDCL-based SAT solvers have transformed the field of automated reasoning owing to their demonstrated efficiency at handling problems arising from diverse domains. The success of CDCL solvers is owed to the design of clever heuristics that enable the tight coupling of different components. One of the core components is phase selection, wherein the solver, during branching, decides the polarity of the branch to be explored for a given variable. Most of the state-of-the-art CDCL SAT solvers employ phase-saving as a phase selection heuristic, which was proposed to address the potential inefficiencies arising from far-backtracking. In light of the emergence of chronological backtracking in CDCL solvers, we re-examine the efficiency of phase saving. Our empirical evaluation leads to a surprising conclusion: The usage of saved phase and random selection of polarity for decisions following a chronological backtracking leads to an indistinguishable runtime performance in terms of instances solved and PAR-2 score. We introduce Decaying Polarity Score (DPS) to capture the trend of the polarities attained by the variable, and upon observing lack of performance improvement due to DPS, we turn to a more sophisticated heuristic seeking to capture the activity of literals and the trend of polarities: Literal State Independent Decaying Sum (LSIDS). We find the 2019 winning SAT solver, Maple_LCM_Dist_ChronoBTv3, augmented with LSIDS solves 6 more instances while achieving a reduction of over 125 seconds in PAR-2 score, a significant improvement in the context of the SAT competition.
has issue date	2020-06-26(xsd:dateTime)
bibo:doi	10.1007/978-3-030-51825-7_6
has license	no-cc
sha1sum (hex)	012168d42a11ee62575548f7c7dde4924b0711de
schema:url	https://doi.org/10.1007/978-3-030-51825-7_6
resource representing a document's title	Designing New Phase Selection Heuristics
has PubMed Central identifier	PMC7326467
schema:publication	Theory and Applications of Satisfiability Testing - SAT 2020
resource representing a document's body	covid:012168d42a11ee62575548f7c7dde4924b0711de#body_text
is http://vocab.deri.ie/void#inDataset of	proxy:http/ns.inria.fr/covid19/012168d42a11ee62575548f7c7dde4924b0711de
is schema:about of	named entity 'Selection' named entity 'Phase' named entity 'SAT' named entity 'problems' named entity 'enable' named entity 'backtracking' named entity 'heuristic' named entity 'heuristic' named entity 'PAR' named entity 'CDCL' named entity 'automated reasoning' named entity 'backtracking' named entity 'heuristic' named entity 'PAR-2' named entity 'PAR-2' named entity 'SAT' named entity 'PAR-2' named entity 'multiplication' named entity 'cryptographic hash functions' named entity 'clause learning' named entity 'PAR-2' named entity 'PAR-2' named entity 'scalability' named entity 'SAT' named entity 'floating-point number' named entity 'SAT' named entity 'heuristic' named entity 'heuristic' named entity 'SAT solving' named entity 'SAT' named entity 'heuristics' named entity 'heuristics' named entity 'PAR-2' named entity 'backtracks' named entity 'backtracks' named entity 'empirical results' named entity 'backtracks' named entity 'heuristic' named entity 'subroutine' named entity 'heuristic' named entity 'SAT' named entity 'heuristic' named entity 'heuristic' named entity 'SAT solvers' named entity 'statistically significant' named entity 'satisfying assignment' named entity 'heuristics' named entity 'satisfying assignment' named entity 'floating-point number' named entity 'PAR-2' named entity 'SAT solving' named entity 'PAR-2' named entity 'negation' named entity 'heuristic' named entity 'backtracking' named entity 'subset' named entity 'SAT solving' named entity 'heuristic' named entity 'backtracking' named entity 'heuristic' named entity 'SAT' named entity 'scatter plot' named entity 'heuristics' named entity 'Boolean Satisfiability' named entity 'SAT' named entity 'backtracking' named entity 'heuristics' named entity 'heuristics' named entity 'SAT' named entity 'heuristic' named entity 'SAT' named entity 'inc' named entity 'heuristics' named entity 'constraint satisfaction' named entity 'backtracks' named entity 'PAR-2' named entity 'NP-complete' named entity 'backtracking' named entity 'SAT solvers' named entity 'heuristic'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software