English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The Boolean SATisfiability problem (SAT) is of central importance in computerscience. Although SAT is known to be NP-complete, progress on the engineeringside, especially that of Conflict-Driven Clause Learning (CDCL) and LocalSearch SAT solvers, has been remarkable. Yet, while SAT solvers aimed atsolving industrial-scale benchmarks in Conjunctive Normal Form (CNF) havebecome quite mature, SAT solvers that are effective on other types ofconstraints, e.g., cardinality constraints and XORs, are less well studied; ageneral approach to handling non-CNF constraints is still lacking. In addition,previous work indicated that for specific classes of benchmarks, the runningtime of extant SAT solvers depends heavily on properties of the formula anddetails of encoding, instead of the scale of the benchmarks, which addsuncertainty to expectations of running time.  To address the issues above, we design FourierSAT, an incomplete SAT solverbased on Fourier analysis of Boolean functions, a technique to representBoolean functions by multilinear polynomials. By such a reduction to continuousoptimization, we propose an algebraic framework for solving systems consistingof different types of constraints. The idea is to leverage gradient informationto guide the search process in the direction of local improvements. Empiricalresults demonstrate that FourierSAT is more robust than other solvers oncertain classes of benchmarks.

FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints