scholarly journals On Solving MaxSAT Through SAT

10.29007/vxm5 ◽  
2018 ◽  
Author(s):  
Carlos Ansótegui ◽  
María Luisa Bonet ◽  
Jordi Levy
Keyword(s):  
Cardinality Constraints ◽  
Additional Variable ◽  
Sat Solver

In this paper we present a Partial MaxSAT solver based on successive calls to a SAT solver. At the kth iteration the SAT solver tries to certify that there exist an assignment that satisfies all but k clauses. The key idea is to add an additional variable to each soft clause and to introduce, at each iteration, at-least and at-most cardinality constraints restricting the possible values of these variables. We prove the correctness of our algorithm and compare it with other (Partial) MaxSAT solvers.

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

2020 ◽  
Vol 34 (02) ◽  
pp. 1552-1560
Author(s):  
Anastasios Kyrillidis ◽  
Anshumali Shrivastava ◽  
Moshe Vardi ◽  
Zhiwei Zhang
Keyword(s):  
Boolean Functions ◽  
Continuous Optimization ◽  
Conjunctive Normal Form ◽  
Cardinality Constraints ◽  
Sat Solvers ◽  
Boolean Satisfiability Problem ◽  
Algebraic Framework ◽  
Clause Learning ◽  
Sat Solver ◽  
Analysis Of Boolean Functions

The Boolean SATisfiability problem (SAT) is of central importance in computer science. Although SAT is known to be NP-complete, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, SAT solvers that are effective on other types of constraints (e.g., cardinality constraints and XORs) are less well-studied; a general approach to handling non-CNF constraints is still lacking. In addition, previous work indicated that for specific classes of benchmarks, the running time of extant SAT solvers depends heavily on properties of the formula and details of encoding, instead of the scale of the benchmarks, which adds uncertainty to expectations of running time.To address the issues above, we design FourierSAT, an incomplete SAT solver based on Fourier analysis of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By such a reduction to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. Empirical results demonstrate that FourierSAT is more robust than other solvers on certain classes of benchmarks.

scholarly journals Decision levels are stable: towards better SAT heuristics

10.29007/cz1f ◽  
2020 ◽  
Author(s):  
Robert Nieuwenhuis ◽  
Adrià Lozano ◽  
Albert Oliveras ◽  
Enric Rodríguez-Carbonell
Keyword(s):  
Information Sharing ◽  
Experimental Setup ◽  
Cardinality Constraints ◽  
Sat Solvers ◽  
Parallel Solvers ◽  
Decision Level ◽  
Sat Solver ◽  
Real Value ◽  
Surprising Fact

We shed new light on the Literal Block Distance (LBD) and glue-based heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals we define, by a real value between 0 and 1, how sticky they are, basically, how frequently they are set at the same decision level.By means of a careful and detailed experimental setup and analysis, we confirm the following quite surprising fact: given a SAT instance, when running different CDCL SAT solvers on it, no matter their settings or random seeds, the stickiness relation between literals is always very similar, in a precisely defined sense.We analyze how quickly stickiness stabilizes in a run (quite quickly), and show that it is stable even under different encodings of cardinality constraints. We then describe how and why these solid new insights lead to heuristics refinements for SAT (and extensions, such as SMT) and improved information sharing in parallel solvers.

Features of the kinetics of cyclic elastoplastic deformation diagrams at dwells in cycles and superimposition of variable stresses on them

2020 ◽  
Vol 86 (12) ◽  
pp. 46-53
Author(s):  
M. M. Gadenin
Keyword(s):  
Experimental Data ◽  
Elastoplastic Deformation ◽  
Low Cycle Fatigue ◽  
Cycle Fatigue ◽  
Loading Cycle ◽  
Additional Variable ◽  
Dynamic Creep ◽  
Variable Stresses ◽  
Kinetics Of ◽  
Deformation Diagrams

The goal of the study is determination of the regularities of changes in cyclic strains and related deformation diagrams attributed to the existence of time dwells in the loading modes and imposition of additional variable stresses on them. Analysis of the obtained experimental data on the kinetics of cyclic elastoplastic deformation diagrams and their parameters revealed that in contrast to regular cyclic loading (equal in stresses), additional deformations of static and dynamic creep are developed. The results of the studys are especially relevant for assessing the cyclic strength of unique extremely loaded objects of technology, including nuclear power equipment, units of aviation and space systems, etc. The experiments were carried out on the samples of austenitic stainless steel under low-cycle loading and high temperatures of testing. Static and dynamic creep deformations arising under those loading conditions promote an increase in the range of cyclic plastic strain in each loading cycle and also stimulate an increase in the range of elastoplastic strain due to active cyclic deformation. At the same time the existence of dwells on extrema of stresses in cycles without imposition of additional variable stresses on them most strongly affects the growth of plastic strain ranges in cycles. Imposition of additional variable stresses on dwells also results in the development of creep strains, but their growth turns out to be somewhat less than in the presence of dwells without stresses imposed. The diagrams of cyclic deformation obtained in the experiments are approximated by power dependences, their kinetics being described in terms of the number of loading cycles using corresponding temperature-time functions. At the same time, it is shown that increase in the cyclic plastic deformation for cycles with dwells and imposition of additional variable stresses on them decreases low cycle fatigue life compared to regular loading without dwells at the same stress amplitudes, moreover, the higher the values of static and dynamic creep, the greater decrease in low-cycle fatigue life. This conclusion results from experimental data and analysis of conditions of damage accumulation for the considered forms of the loading cycle using the deformation criterion of reaching the limit state leading to fracture.

March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver

2005 ◽  
pp. 345-359 ◽  
Author(s):  
Marijn Heule ◽  
Mark Dufour ◽  
Joris van Zwieten ◽  
Hans van Maaren
Keyword(s):  
Look Ahead ◽  
Sat Solver

An Efficient Local Search SAT Solver with Effective Preprocessing for Structured Instances

2021 ◽  
Vol 2 (2) ◽  
Author(s):  
Md Shibbir Hossen ◽  
Md Masbaul Alam Polash
Keyword(s):  
Local Search ◽  
Sat Solver

scholarly journals Inaccuracy of self-evaluation as additional variable for prediction of students at risk of failing first-year chemistry

2010 ◽  
Vol 11 (1) ◽  
pp. 17-24 ◽  
Author(s):  
Marietjie Potgieter ◽  
Mia Ackermann ◽  
Lizelle Fletcher
Keyword(s):  
At Risk ◽  
First Year ◽  
Students At Risk ◽  
Additional Variable ◽  
Self Evaluation
Sign in / Sign up

Export Citation Format

Share Document