Zaloguj się

Gotowe bibliografie tematyczne / SAT solver / Artykuły w czasopismach

Artykuły w czasopismach na temat „SAT solver”

Kliknij ten link, aby zobaczyć inne rodzaje publikacji na ten temat: SAT solver.

Autor: Grafiati

Data publikacji: 4 czerwca 2021

Data aktualizacji: 22 czerwca 2023

Utwórz poprawne odniesienie w stylach APA, MLA, Chicago, Harvard i wielu innych

Wybierz rodzaj źródła:

Sprawdź 50 najlepszych artykułów w czasopismach naukowych na temat „SAT solver”.

Przycisk „Dodaj do bibliografii” jest dostępny obok każdej pracy w bibliografii. Użyj go – a my automatycznie utworzymy odniesienie bibliograficzne do wybranej pracy w stylu cytowania, którego potrzebujesz: APA, MLA, Harvard, Chicago, Vancouver itp.

Możesz również pobrać pełny tekst publikacji naukowej w formacie „.pdf” i przeczytać adnotację do pracy online, jeśli odpowiednie parametry są dostępne w metadanych.

Przeglądaj artykuły w czasopismach z różnych dziedzin i twórz odpowiednie bibliografie.

1

Klyucharev, P. G. "Exploring Practicability for Solving a Task Based on the Generalized Cellular Automata via SAT Solvers". Mechanical Engineering and Computer Science, nr 11 (2.01.2019): 11–22. http://dx.doi.org/10.24108/1118.0001439.

Pełny tekst źródła

Streszczenie:

The paper deals with exploring practicability to solve a task of the recovery key of generalized cellular automata via SAT solvers.The problem, which we call a task of the key recovery of generalized cellular automata, is under consideration. This task is formulated as follows. The generalized cellular automata, the positive integer s, the initial values of some cells, and the values of some cells after the s steps of the automata are given. It is required to find the initial values of the remaining cells (their number will be called the key length).To solve the task, were tested Picosat, MiniSat, Glucose, Lingeling, and CryptoMiniSat SAT solvers. In further computational experiments, was used the MiniSat, which was the best.The key recovery task was solved for the generalized cellular automata of a small size via the MiniSat SAT solver. Pizer's graphs were used as graphs of the automata. The key length was approximately half the number of the cells in the automata. As a result of the study, it turned out that operation time of a SAT solver quite significantly (several orders of magnitude) exceeds the estimated time of solution using the FPGA exhaustive method, and the empirical dependencies of the SAT-solver operation time on the key length are exponential.The obtained results confirm that SAT solvers disable effective solving a task under consideration. This allows giving the better reasons for the cryptographic security of the crypto-algorithms based on the generalized cellular automata with regard to the cryptanalysis methods using SAT solvers.

Style APA, Harvard, Vancouver, ISO itp.

2

Audemard, Gilles, i Laurent Simon. "On the Glucose SAT Solver". International Journal on Artificial Intelligence Tools 27, nr 01 (luty 2018): 1840001. http://dx.doi.org/10.1142/s0218213018400018.

Pełny tekst źródła

Streszczenie:

The set of novelties introduced with the SAT solver Glucose is now considered as a standard for practical SAT solving. In this paper, we review the different strategies and technologies added in Glucose over the years. We detail each technique and discuss its impact on the final performances reached by Glucose. We also come back on one of the main developments of the solver over the very last years: its efficient parallelization. We extensively tested different versions of Glucose and Syrup (its parallel version) on all the benchmarks since 2011. By including, as a reference, the SAT solver Lingeling (and its parallel version Plingeling), we show that Glucose and Syrup are significantly faster than other solvers, even if they can solve fewer instances.

Style APA, Harvard, Vancouver, ISO itp.

3

Sonobe, Tomohiro. "An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle". Algorithms 15, nr 12 (16.12.2022): 479. http://dx.doi.org/10.3390/a15120479.

Pełny tekst źródła

Streszczenie:

It has been proven that extended resolution (ER) has more powerful reasoning than general resolution for the pigeonhole principle in Cook’s paper. This fact indicates the possibility that a solver based on extended resolution can exceed Boolean satisfiability problem solvers (SAT solvers for short) based on general resolution. However, few studies have provided practical evidence of this assumption. This paper explores how extended resolution can improve SAT solvers by using the pigeonhole principle, which was the first problem solved by ER in polynomial steps. In fact, although Cook’s paper introduced how to add auxiliary variables, there is no evidence that these variables are really useful for practical solvers. We try to answer the question: If the SAT solver can add appropriate auxiliary variables as proposed in Cook’s paper, can the solver enhance its performance by utilizing these variables? Experimental results show that if the solver properly prioritizes the extended variables in the search, the solver can end the search in a shorter time.

Style APA, Harvard, Vancouver, ISO itp.

4

Čapek, Martin, i Pavel Surynek. "DPLL(MAPF): an Integration of Multi-Agent Path Finding and SAT Solving Technologies". Proceedings of the International Symposium on Combinatorial Search 12, nr 1 (21.07.2021): 153–55. http://dx.doi.org/10.1609/socs.v12i1.18567.

Pełny tekst źródła

Streszczenie:

The task in multi-agent path finding (MAPF) is to find non-conflicting paths connecting agents' start and goal positions. The MAPF problem is often compiled to Boolean satisfiability (SAT) and solved by existing SAT solvers. Contemporary compilation approaches of MAPF to SAT regard the SAT solver as an external tool whose task is to return an assignment of all decision variables of a Boolean model of the input MAPF instance. We present in this paper a novel compilation scheme called DPLL(MAPF) in which the consistency checking of partial assignments of decision variables with respect to the MAPF rules is integrated directly into the SAT solver. This scheme allows for far more automated compilation where the SAT solver and the consistency checking procedure work together simultaneously to create the Boolean model and to search for its satisfying assignment.

Style APA, Harvard, Vancouver, ISO itp.

5

Vieira, Bernardo C., Fabrício V. Andrade i Antônio O. Fernandes. "Framework for Generating Configurable SAT Solvers". Journal of Integrated Circuits and Systems 6, nr 1 (27.12.2011): 50–59. http://dx.doi.org/10.29292/jics.v6i1.338.

Pełny tekst źródła

Streszczenie:

The state-of-the-art SAT solvers usually share the same core techniques, for instance: the watched literals structure, conflict clause recording and non-chronological backtracking. Nevertheless, they might differ in the elimination of learnt clauses, as well as in the decision heuristic. This article presents a framework for generating configurable SAT solvers. The proposed framework is composed of the following components: a Base SAT Solver, a Perl Preprocessor, XML files (Solver Description and Heuristics Description files) to describe each heuristic as well as the set of heuristics that the generated solver uses. This solvers may use several techniques and heuristics such as those implemented in BerkMin, and in Equivalence Checking of Dissimilar Circuits, and also in Minisat. In order to demonstrate the effectiveness of the proposed framework, this article also presents three distinct SAT solver instances generated by the framework to address a complex and challenging industry problem: the Combinational Equivalence Checking problem (CEC).The first instance is a SAT solver that uses BerkMin and Dissimilar Circuits core techniques except the learnt clause elimination heuristic that has been adapted from Minisat; the second is another solver that combines BerkMin and Minisat decision heuristics at run-time; and the third is yet another SAT solver that changes the database reducing heuristic at run-time. The experiments demonstrate that the first SAT solver generated is a faster solver than state-of-the-art SAT solver BerkMin for several instances as well as for Minisat in almost every instance.

Style APA, Harvard, Vancouver, ISO itp.

6

Al-Yahya, Tasniem, Mohamed El Bachir Menai i Hassan Mathkour. "Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors". Algorithms 15, nr 9 (26.08.2022): 302. http://dx.doi.org/10.3390/a15090302.

Pełny tekst źródła

Streszczenie:

Boolean structural measures were introduced to explain the high performance of conflict-driven clause-learning (CDCL) SAT solvers on industrial SAT instances. Those considered in this study include measures related to backbones and backdoors: backbone size, backbone frequency, and backdoor size. A key area of research is to improve the performance of CDCL SAT solvers by exploiting these measures. For the purpose of guiding the CDCL SAT solver for branching on backbone and backdoor variables, this study proposes low-overhead heuristics for computing these variables. Through these heuristics, a set of modifications to the Variable State Independent Decaying Sum (VSIDS) decision heuristic is suggested to exploit backbones and backdoors and potentially improve the performance of CDCL SAT solvers. In total, fifteen variants of two competitive base solvers, MapleLCMDistChronoBT-DL-v3 and LSTech, were developed. Empirical evaluation was conducted on 32 industrial families from 2002–2021 SAT competitions. According to the results, modifying the VSIDS heuristic in the base solvers to exploit backbones and backdoors improves its performance. In particular, our new CDCL SAT solver, LSTech_BBsfcr_v1, solved more industrial SAT instances than the winning CDCL SAT solvers in 2020 and 2021 SAT competitions.

Style APA, Harvard, Vancouver, ISO itp.

7

Mueller, Matthias. "Polynomial Exact-3-SAT-Solving Algorithm". International Journal of Engineering & Technology 9, nr 3 (4.08.2020): 670. http://dx.doi.org/10.14419/ijet.v9i3.30749.

Pełny tekst źródła

Streszczenie:

This article describes an algorithm which is supposed by the author to be capable of solving any instance of a 3-SAT CNF in maximal O(n^15), whereby n is the variable index range within the 3-SAT CNF to solve. The presented algorithm imitates the proceeding of an exponential, fail-safe solver. This exponential solver stores internal data in m-SAT clauses, with 3 <= m <= n. The polynomial solver works similarly, but uses 3-SAT clauses only to save the same data. The paper explains how, and proves why this can be achieved. On the supposition the algorithm is correct, the P-NP-Problem would be solved with the result that the complexity classes NP and P are equal.

Style APA, Harvard, Vancouver, ISO itp.

8

Aono, Masashi, Song-Ju Kim, Liping Zhu, Makoto Naruse, Motoichi Ohtsu, Hirokazu Hori i Masahiko Hara. "Amoeba-inspired SAT Solver". IEICE Proceeding Series 1 (17.03.2014): 586–89. http://dx.doi.org/10.15248/proc.1.586.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

9

Surynek, Pavel, Roni Stern, Eli Boyarski i Ariel Felner. "Migrating Techniques from Search-based Multi-Agent Path Finding Solvers to SAT-based Approach". Journal of Artificial Intelligence Research 73 (10.02.2022): 553–618. http://dx.doi.org/10.1613/jair.1.13318.

Pełny tekst źródła

Streszczenie:

In the multi-agent path finding problem (MAPF) we are given a set of agents each with respective start and goal positions. The task is to find paths for all agents while avoiding collisions, aiming to minimize a given objective function. Many MAPF solvers were introduced in the past decade for optimizing two specific objective functions: sum-of-costs and makespan. Two prominent categories of solvers can be distinguished: search-based solvers and compilation-based solvers. Search-based solvers were developed and tested for the sum-of-costs objective, while the most prominent compilation-based solvers that are built around Boolean satisfiability (SAT) were designed for the makespan objective. Very little is known on the performance and relevance of solvers from the compilation-based approach on the sum-of-costs objective. In this paper, we start to close the gap between these cost functions in the compilation-based approach. Our main contribution is a new SAT-based MAPF solver called MDD-SAT, that is directly aimed to optimally solve the MAPF problem under the sum-of-costs objective function. Using both a lower bound on the sum-of-costs and an upper bound on the makespan, MDD-SAT is able to generate a reasonable number of Boolean variables in our SAT encoding. We then further improve the encoding by borrowing ideas from ICTS, a search-based solver. In addition, we show that concepts applicable in search-based solvers like ICTS and ICBS are applicable in the SAT-based approach as well. Specifically, we integrate independence detection, a generic technique for decomposing an MAPF instance into independent subproblems, into our SAT-based approach, and we design a relaxation of our optimal SAT-based solver that results in a bounded suboptimal SAT-based solver. Experimental evaluation on several domains shows that there are many scenarios where our SAT-based methods outperform state-of-the-art sum-of-costs search-based solvers, such as variants of the ICTS and ICBS algorithms.

Style APA, Harvard, Vancouver, ISO itp.

10

Järvisalo, Matti, Daniel Le Berre, Olivier Roussel i Laurent Simon. "The International SAT Solver Competitions". AI Magazine 33, nr 1 (15.03.2012): 89–92. http://dx.doi.org/10.1609/aimag.v33i1.2395.

Pełny tekst źródła

Streszczenie:

The International SAT Solver Competition is today an established series of competitive events aiming at objectively evaluating the progress in state-of-the-art procedures for solving Boolean satisfiability (SAT) instances. Over the years, the competitions have significantly contributed to the fast progress in SAT solver technology that has made SAT a practical success story of computer science. This short article provides an overview of the SAT solver competitions.

Style APA, Harvard, Vancouver, ISO itp.

11

Hamadi, Youssef, Said Jabbour i Lakhdar Sais. "ManySAT: a Parallel SAT Solver". Journal on Satisfiability, Boolean Modeling and Computation 6, nr 4 (1.06.2009): 245–62. http://dx.doi.org/10.3233/sat190070.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

12

Van Gelder, Allen. "Contrasat – A Contrarian SAT Solver". Journal on Satisfiability, Boolean Modeling and Computation 8, nr 3-4 (1.03.2012): 117–22. http://dx.doi.org/10.3233/sat190093.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

13

Кондратьев, В. С., А. А. Семенов i О. С. Заикин. "Duplicates of conflict clauses in CDCL derivation and their usage to invert some cryptographic functions". Numerical Methods and Programming (Vychislitel'nye Metody i Programmirovanie), nr 1 (20.01.2019): 54–66. http://dx.doi.org/10.26089/nummet.v20r106.

Pełny tekst źródła

Streszczenie:

Изучен феномен повторного порождения конфликтных ограничений SAT-решателями в процессе работы с трудными экземплярами задачи о булевой выполнимости. Данный феномен является следствием применения эвристических механизмов чистки конфликтных баз, которые реализованы во всех современных SAT-решателях, основанных на алгоритме CDCL (Conflict Driven Clause Learning). Описана новая техника, которая позволяет отслеживать повторно порождаемые дизъюнкты и запрещать их последующее удаление. На базе предложенных технических решений построен новый многопоточный SAT-решатель (SAT, SATisfiability), который на ряде SAT-задач, кодирующих обращение криптографических хеш-функций, существенно превзошел по эффективности многопоточные решатели, занимавшие в последние годы высокие места на специализированных соревнованиях. A phenomenon of conflict clauses generated repeatedly by SAT solvers is studied. Such clauses may appear during solving hard Boolean satisfiability problems (SAT). This phenomenon is caused by the fact that the modern SAT solvers are based on the CDCL algorithm that generates conflict clauses. A database of such clauses is periodically and partially cleaned. A new approach for practical SAT solving is proposed. According to this approach, the repeatedly generated conflict clauses are tracked, whereas their further generation is prohibited. Based on this approach, a multithreaded SAT solver was developed. This solver was compared with the best multithreaded SAT solvers awarded during the last SAT competitions. According to the experimental results, the developed solver greatly outperforms its competitors on several SAT instances encoding the inversion of some cryptographic hash functions.

Style APA, Harvard, Vancouver, ISO itp.

14

Stuckey, Peter J., Thibaut Feydy, Andreas Schutt, Guido Tack i Julien Fischer. "The MiniZinc Challenge 2008–2013". AI Magazine 35, nr 2 (19.06.2014): 55–60. http://dx.doi.org/10.1609/aimag.v35i2.2539.

Pełny tekst źródła

Streszczenie:

MiniZinc is a solver agnostic modeling language for defining and solver combinatorial satisfaction and optimization problems. MiniZinc provides a solver independent modeling language which is now supported by constraint programming solvers, mixed integer programming solvers, SAT and SAT modulo theory solvers, and hybrid solvers. Since 2008 we have run the MiniZinc challenge every year, which compares and contrasts the different strengths of different solvers and solving technologies on a set of MiniZinc models. Here we report on what we have learnt from running the competition for 6 years.

Style APA, Harvard, Vancouver, ISO itp.

15

Surynek, Pavel, Ariel Felner, Roni Stern i Eli Boyarski. "Sub-Optimal SAT-Based Approach to Multi-Agent Path-Finding Problem". Proceedings of the International Symposium on Combinatorial Search 9, nr 1 (1.09.2021): 99–105. http://dx.doi.org/10.1609/socs.v9i1.18456.

Pełny tekst źródła

Streszczenie:

In multi-agent path finding (MAPF) the task is to find nonconflicting paths for multiple agents. In this paper we focus on finding suboptimal solutions for MAPF for the sum-of-costs variant. Recently, a SAT-based approached was developed to solve this problem and proved beneficial in many cases when compared to other search-based solvers. In this paper, we present SAT-based unbounded- and bounded-suboptimal algorithms and compare them to relevant algorithms. Experimental results show that in many case the SAT-based solver significantly outperforms the search-based solvers.

Style APA, Harvard, Vancouver, ISO itp.

16

Xu, L., F. Hutter, H. H. Hoos i K. Leyton-Brown. "SATzilla: Portfolio-based Algorithm Selection for SAT". Journal of Artificial Intelligence Research 32 (1.07.2008): 565–606. http://dx.doi.org/10.1613/jair.2490.

Pełny tekst źródła

Streszczenie:

It has been widely observed that there is no single "dominant" SAT solver; instead, different solvers perform best on different instances. Rather than following the traditional approach of choosing the best solver for a given class of instances, we advocate making this decision online on a per-instance basis. Building on previous work, we describe SATzilla, an automated approach for constructing per-instance algorithm portfolios for SAT that use so-called empirical hardness models to choose among their constituent solvers. This approach takes as input a distribution of problem instances and a set of component solvers, and constructs a portfolio optimizing a given objective function (such as mean runtime, percent of instances solved, or score in a competition). The excellent performance of SATzilla was independently verified in the 2007 SAT Competition, where our SATzilla07 solvers won three gold, one silver and one bronze medal. In this article, we go well beyond SATzilla07 by making the portfolio construction scalable and completely automated, and improving it by integrating local search solvers as candidate solvers, by predicting performance score instead of runtime, and by using hierarchical hardness models that take into account different types of SAT instances. We demonstrate the effectiveness of these new techniques in extensive experimental results on data sets including instances from the most recent SAT competition.

Style APA, Harvard, Vancouver, ISO itp.

17

Audemard, Gilles, George Katsirelos i Laurent Simon. "A Restriction of Extended Resolution for Clause Learning SAT Solvers". Proceedings of the AAAI Conference on Artificial Intelligence 24, nr 1 (3.07.2010): 15–20. http://dx.doi.org/10.1609/aaai.v24i1.7553.

Pełny tekst źródła

Streszczenie:

Modern complete SAT solvers almost uniformly implement variations of the clause learning framework introduced by Grasp and Chaff. The success of these solvers has been theoretically explained by showing that the clause learning framework is an implementation of a proof system which is as poweful as resolution. However, exponential lower bounds are known for resolution, which suggests that significant advances in SAT solving must come from implementations of more powerful proof systems. We present a clause learning SAT solver that uses extended resolution. It is based on a restriction of the application of the extension rule. This solver outperforms existing solvers on application instances from recent SAT competitions as well as on instances that are provably hard for resolution.

Style APA, Harvard, Vancouver, ISO itp.

18

Heras, F., J. Larrosa i A. Oliveras. "MiniMaxSAT: An Efficient Weighted Max-SAT solver". Journal of Artificial Intelligence Research 31 (17.01.2008): 1–32. http://dx.doi.org/10.1613/jair.2347.

Pełny tekst źródła

Streszczenie:

In this paper we introduce MiniMaxSat, a new Max-SAT solver that is built on top of MiniSat+. It incorporates the best current SAT and Max-SAT techniques. It can handle hard clauses(clauses of mandatory satisfaction as in SAT), soft clauses (clauses whose falsification is penalized by a cost as in Max-SAT) as well as pseudo-boolean objective functions and constraints. Its main features are: learning and backjumping on hard clauses; resolution-based and substraction-based lower bounding; and lazy propagation with the two-watched literal scheme. Our empirical evaluation comparing a wide set of solving alternatives on a broad set of optimization benchmarks indicates that the performance of MiniMaxSat is usually close to the best specialized alternative and, in some cases, even better.

Style APA, Harvard, Vancouver, ISO itp.

19

Ansotegui, Carlos, Maria Luisa Bonet i Jordi Levy. "A New Algorithm for Weighted Partial MaxSAT". Proceedings of the AAAI Conference on Artificial Intelligence 24, nr 1 (3.07.2010): 3–8. http://dx.doi.org/10.1609/aaai.v24i1.7545.

Pełny tekst źródła

Streszczenie:

We present and implement a Weighted Partial MaxSAT solver based on successive calls to a SAT solver. We prove the correctness of our algorithm and compare our solver with other Weighted Partial MaxSAT solvers.

Style APA, Harvard, Vancouver, ISO itp.

20

Dantsin, Evgeny, i Alexander Wolpert. "An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF". Journal on Satisfiability, Boolean Modeling and Computation 14, nr 1 (4.01.2023): 1–15. http://dx.doi.org/10.3233/sat-220006.

Pełny tekst źródła

Streszczenie:

We define a distance function on propositional formulas in CNF as a measure of non-isomorphism of formulas: the larger the distance between two formulas is, the further they are from being isomorphic. This distance induces a metric on isomorphism classes of formulas. We show how this distance can be used for SAT solving, namely for per-instance algorithm selection where there is a “portfolio” of SAT solvers and there is a “meta-solver” that chooses a solver from the portfolio for a given input formula.

Style APA, Harvard, Vancouver, ISO itp.

21

Koshimura, Miyuki, Tong Zhang, Hiroshi Fujita i Ryuzo Hasegawa. "QMaxSAT: A Partial Max-SAT Solver". Journal on Satisfiability, Boolean Modeling and Computation 8, nr 1-2 (1.01.2012): 95–100. http://dx.doi.org/10.3233/sat190091.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

22

Skliarova, I., i A. B. Ferrari. "A software/reconfigurable hardware SAT solver". IEEE Transactions on Very Large Scale Integration (VLSI) Systems 12, nr 4 (kwiecień 2004): 408–19. http://dx.doi.org/10.1109/tvlsi.2004.825859.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

23

(Moti) Ben-Ari, Mordechai. "LearnSAT: A SAT Solver for Education". Journal of Open Source Software 3, nr 24 (26.04.2018): 639. http://dx.doi.org/10.21105/joss.00639.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

24

Siddiqi, Sajjad. "An extensible circuit-based SAT solver". Journal of Experimental & Theoretical Artificial Intelligence 32, nr 5 (3.10.2019): 751–68. http://dx.doi.org/10.1080/0952813x.2019.1672798.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

25

Hutter, Frank, Marius Lindauer, Adrian Balint, Sam Bayless, Holger Hoos i Kevin Leyton-Brown. "The Configurable SAT Solver Challenge (CSSC)". Artificial Intelligence 243 (luty 2017): 1–25. http://dx.doi.org/10.1016/j.artint.2016.09.006.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

26

Ansótegui, Carlos, Maria Luisa Bonet, Jesús Giráldez-Cru, Jordi Levy i Laurent Simon. "Community Structure in Industrial SAT Instances". Journal of Artificial Intelligence Research 66 (10.10.2019): 443–72. http://dx.doi.org/10.1613/jair.1.11741.

Pełny tekst źródła

Streszczenie:

Modern SAT solvers have experienced a remarkable progress on solving industrial instances. It is believed that most of these successful techniques exploit the underlying structure of industrial instances. Recently, there have been some attempts to analyze the structure of industrial SAT instances in terms of complex networks, with the aim of explaining the success of SAT solving techniques, and possibly improving them. In this paper, we study the community structure, or modularity, of industrial SAT instances. In a graph with clear community structure, or high modularity, we can find a partition of its nodes into communities such that most edges connect variables of the same community. Representing SAT instances as graphs, we show that most application benchmarks are characterized by a high modularity. On the contrary, random SAT instances are closer to the classical Erdös-Rényi random graph model, where no structure can be observed. We also analyze how this structure evolves by the effects of the execution of a CDCL SAT solver, and observe that new clauses learned by the solver during the search contribute to destroy the original structure of the formula. Motivated by this observation, we finally present an application that exploits the community structure to detect relevant learned clauses, and we show that detecting these clauses results in an improvement on the performance of the SAT solver. Empirically, we observe that this improves the performance of several SAT solvers on industrial SAT formulas, especially on satisfiable instances.

Style APA, Harvard, Vancouver, ISO itp.

27

Andrici, Cezar-Constantin, i Ștefan Ciobâcă. "A Verified Implementation of the DPLL Algorithm in Dafny". Mathematics 10, nr 13 (28.06.2022): 2264. http://dx.doi.org/10.3390/math10132264.

Pełny tekst źródła

Streszczenie:

We present a DPLL SAT solver, which we call TrueSAT, developed in the verification-enabled programming language Dafny. We have fully verified the functional correctness of our solver by constructing machine-checked proofs of its soundness, completeness, and termination. We present a benchmark of the execution time of TrueSAT and we show that it is competitive against an equivalent DPLL solver implemented in C++, although it is still slower than state-of-the-art CDCL solvers. Our solver serves as a significant case study of a machine-verified software system. The benchmark also shows that auto-active verification is a promising approach to increasing trust in SAT solvers, because it combines execution speed with a high degree of trustworthiness.

Style APA, Harvard, Vancouver, ISO itp.

28

L. Kaizer, Wesley, André G. Pereira i Marcus Ritt. "Sequencing Operator Counts with State-Space Search". Proceedings of the International Conference on Automated Planning and Scheduling 30 (1.06.2020): 166–74. http://dx.doi.org/10.1609/icaps.v30i1.6658.

Pełny tekst źródła

Streszczenie:

A search algorithm with an admissible heuristic function is the most common approach to optimally solve classical planning tasks. Recently Daviesetal.(2015) introduced the solver OpSeq using Logic-Based Benders Decomposition to solve planning tasks optimally. In this approach, the master problem is an integer program derived from the operator-counting framework that generates operator counts, i.e., an assignment of integer counts for each task operator. Then, the operator counts sequencing subproblem verifies if a plan satisfying these operator counts exists, or generates a necessary violated constraint to strengthen the master problem. In OpSeq the subproblem is solved by a SAT solver. In this paper we show that operator counts sequencing can be better solved by state-space search. We introduce OpSearch, an A∗-based algorithm to solve the operator counts sequencing subproblem: it either finds an optimal plan, or uses the frontier of the search to derive a violated constraint. We show that using a standard search framework has two advantages: i) search scales better than a SAT-based approach for solving the operator counts sequencing, ii) explicit information in the search frontier can be used to derive stronger constraints. We present results on the IPC-2011 benchmarks showing that this approach solves more planning tasks, using less memory. On tasks solved by both methods OpSearch usually requires to solve fewer operator counts sequencing problems than OpSeq, evidencing the stronger constraints generated by OpSearch.

Style APA, Harvard, Vancouver, ISO itp.

29

Gange, G., P. J. Stuckey i V. Lagoon. "Fast Set Bounds Propagation Using a BDD-SAT Hybrid". Journal of Artificial Intelligence Research 38 (25.06.2010): 307–38. http://dx.doi.org/10.1613/jair.3014.

Pełny tekst źródła

Streszczenie:

Binary Decision Diagram (BDD) based set bounds propagation is a powerful approach to solving set-constraint satisfaction problems. However, prior BDD based techniques in- cur the significant overhead of constructing and manipulating graphs during search. We present a set-constraint solver which combines BDD-based set-bounds propagators with the learning abilities of a modern SAT solver. Together with a number of improvements beyond the basic algorithm, this solver is highly competitive with existing propagation based set constraint solvers.

Style APA, Harvard, Vancouver, ISO itp.

30

Fichte, Johannes K., Markus Hecher, Michael Morak i Stefan Woltran. "DynASP2.5: Dynamic Programming on Tree Decompositions in Action". Algorithms 14, nr 3 (2.03.2021): 81. http://dx.doi.org/10.3390/a14030081.

Pełny tekst źródła

Streszczenie:

Efficient exact parameterized algorithms are an active research area. Such algorithms exhibit a broad interest in the theoretical community. In the last few years, implementations for computing various parameters (parameter detection) have been established in parameterized challenges, such as treewidth, treedepth, hypertree width, feedback vertex set, or vertex cover. In theory, instances, for which the considered parameter is small, can be solved fast (problem evaluation), i.e., the runtime is bounded exponential in the parameter. While such favorable theoretical guarantees exists, it is often unclear whether one can successfully implement these algorithms under practical considerations. In other words, can we design and construct implementations of parameterized algorithms such that they perform similar or even better than well-established problem solvers on instances where the parameter is small. Indeed, we can build an implementation that performs well under the theoretical assumptions. However, it could also well be that an existing solver implicitly takes advantage of a structure, which is often claimed for solvers that build on Sat-solving. In this paper, we consider finding one solution to instances of answer set programming (ASP), which is a logic-based declarative modeling and solving framework. Solutions for ASP instances are so-called answer sets. Interestingly, the problem of deciding whether an instance has an answer set is already located on the second level of the polynomial hierarchy. An ASP solver that employs treewidth as parameter and runs dynamic programming on tree decompositions is DynASP2. Empirical experiments show that this solver is fast on instances of small treewidth and can outperform modern ASP when one counts answer sets. It remains open, whether one can improve the solver such that it also finds one answer set fast and shows competitive behavior to modern ASP solvers on instances of low treewidth. Unfortunately, theoretical models of modern ASP solvers already indicate that these solvers can solve instances of low treewidth fast, since they are based on Sat-solving algorithms. In this paper, we improve DynASP2 and construct the solver DynASP2.5, which uses a different approach. The new solver shows competitive behavior to state-of-the-art ASP solvers even for finding just one solution. We present empirical experiments where one can see that our new implementation solves ASP instances, which encode the Steiner tree problem on graphs with low treewidth, fast. Our implementation is based on a novel approach that we call multi-pass dynamic programming (M-DPSINC). In the paper, we describe the underlying concepts of our implementation (DynASP2.5) and we argue why the techniques still yield correct algorithms.

Style APA, Harvard, Vancouver, ISO itp.

31

Li, C. M., F. Manya i J. Planes. "New Inference Rules for Max-SAT". Journal of Artificial Intelligence Research 30 (23.10.2007): 321–59. http://dx.doi.org/10.1613/jair.2215.

Pełny tekst źródła

Streszczenie:

Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving the Max-SAT problem for the simplified formula is not equivalent to solving it for the original formula. In this paper, we define a number of original inference rules that, besides being applied efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution adapted to Max-SAT, are proved in a novel and simple way via an integer programming transformation. With the aim of finding out how powerful the inference rules are in practice, we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules, and performed an experimental investigation. The results provide empirical evidence that MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, Max-Cut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.

Style APA, Harvard, Vancouver, ISO itp.

32

Vaezipoor, Pashootan, Gil Lederman, Yuhuai Wu, Chris Maddison, Roger B. Grosse, Sanjit A. Seshia i Fahiem Bacchus. "Learning Branching Heuristics for Propositional Model Counting". Proceedings of the AAAI Conference on Artificial Intelligence 35, nr 14 (18.05.2021): 12427–35. http://dx.doi.org/10.1609/aaai.v35i14.17474.

Pełny tekst źródła

Streszczenie:

Propositional model counting, or #SAT, is the problem of computing the number of satisfying assignments of a Boolean formula. Many problems from different application areas, including many discrete probabilistic inference problems, can be translated into model counting problems to be solved by #SAT solvers. Exact #SAT solvers, however, are often not scalable to industrial size instances. In this paper, we present Neuro#, an approach for learning branching heuristics to improve the performance of exact #SAT solvers on instances from a given family of problems. We experimentally show that our method reduces the step count on similarly distributed held-out instances and generalizes to much larger instances from the same problem family. It is able to achieve these results on a number of different problem families having very different structures. In addition to step count improvements, Neuro# can also achieve orders of magnitude wall-clock speedups over the vanilla solver on larger instances in some problem families, despite the runtime overhead of querying the model.

Style APA, Harvard, Vancouver, ISO itp.

33

Sheini, Hossein M., i Karem A. Sakallah. "Pueblo: A Hybrid Pseudo-Boolean SAT Solver". Journal on Satisfiability, Boolean Modeling and Computation 2, nr 1-4 (1.03.2006): 165–89. http://dx.doi.org/10.3233/sat190020.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

34

DING, Min. "Integrating advanced reasoning into a SAT solver". Science in China Series F 48, nr 3 (2005): 366. http://dx.doi.org/10.1360/04yf0171.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

35

Takeuchi, Naoki, Masashi Aono, Yuko Hara-Azumi i Christopher L. Ayala. "A Circuit-Level Amoeba-Inspired SAT Solver". IEEE Transactions on Circuits and Systems II: Express Briefs 67, nr 10 (październik 2020): 2139–43. http://dx.doi.org/10.1109/tcsii.2019.2951181.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

36

Goldberg, Eugene, i Yakov Novikov. "BerkMin: A fast and robust Sat-solver". Discrete Applied Mathematics 155, nr 12 (czerwiec 2007): 1549–61. http://dx.doi.org/10.1016/j.dam.2006.10.007.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

37

Moon, Seongsoo, i Mary Inaba. "Boost SAT Solver with Hybrid Branching Heuristic". Proceedings of the International Symposium on Combinatorial Search 8, nr 1 (1.09.2021): 56–63. http://dx.doi.org/10.1609/socs.v8i1.18422.

Pełny tekst źródła

Streszczenie:

Most state-of-the-art satisfiability (SAT) solvers are capable of solving large application instances with efficient branching heuristics. The VSIDS heuristic is widely used because of its robustness. This paper focuses on the inherent ties in VSIDS and proposes a new branching heuristic called TBVSIDS, which attempts to break the ties with the consideration of the interplay between the branching heuristic and learned clauses. However, a branching heuristic cannot cover all problems, and its performance improves when combined with an appropriate configuration. Therefore, we also propose a hybrid model of branching heuristics based on random forest. The efficiencies of TBVSIDS and hybrid branching heuristics are evaluated on benchmarks in SAT Competitions. By constructing a model that reduces the overfitting problem, we hope to realize a hybrid branching heuristic that is widely applicable to other solvers.

Style APA, Harvard, Vancouver, ISO itp.

38

Alsinet, Teresa, Felip Manyà i Jordi Planes. "An efficient solver for weighted Max-SAT". Journal of Global Optimization 41, nr 1 (29.06.2007): 61–73. http://dx.doi.org/10.1007/s10898-007-9166-9.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

39

Zhang, Zaijun, Daoyun Xu i Jincheng Zhou. "A Structural Entropy Measurement Principle of Propositional Formulas in Conjunctive Normal Form". Entropy 23, nr 3 (4.03.2021): 303. http://dx.doi.org/10.3390/e23030303.

Pełny tekst źródła

Streszczenie:

The satisfiability (SAT) problem is a core problem in computer science. Existing studies have shown that most industrial SAT instances can be effectively solved by modern SAT solvers while random SAT instances cannot. It is believed that the structural characteristics of different SAT formula classes are the reasons behind this difference. In this paper, we study the structural properties of propositional formulas in conjunctive normal form (CNF) by the principle of structural entropy of formulas. First, we used structural entropy to measure the complex structure of a formula and found that the difficulty solving the formula is related to the structural entropy of the formula. The smaller the compressing information of a formula, the more difficult it is to solve the formula. Secondly, we proposed a λ-approximation strategy to approximate the structural entropy of large formulas. The experimental results showed that the proposed strategy can effectively approximate the structural entropy of the original formula and that the approximation ratio is more than 92%. Finally, we analyzed the structural properties of a formula in the solution process and found that a local search solver tends to select variables in different communities to perform the next round of searches during a search and that the structural entropy of a variable affects the probability of the variable being flipped. By using these conclusions, we also proposed an initial candidate solution generation strategy for a local search for SAT, and the experimental results showed that this strategy effectively improves the performance of the solvers CCAsat and Sparrow2011 when incorporated into these two solvers.

Style APA, Harvard, Vancouver, ISO itp.

40

Soos, Mate, i Kuldeep S. Meel. "BIRD: Engineering an Efficient CNF-XOR SAT Solver and Its Applications to Approximate Model Counting". Proceedings of the AAAI Conference on Artificial Intelligence 33 (17.07.2019): 1592–99. http://dx.doi.org/10.1609/aaai.v33i01.33011592.

Pełny tekst źródła

Streszczenie:

Given a Boolean formula φ, the problem of model counting, also referred to as #SAT is to compute the number of solutions of φ. Model counting is a fundamental problem in artificial intelligence with a wide range of applications including probabilistic reasoning, decision making under uncertainty, quantified information flow, and the like. Motivated by the success of SAT solvers, there has been surge of interest in the design of hashing-based techniques for approximate model counting for the past decade. We profiled the state of the art approximate model counter ApproxMC2 and observed that over 99.99% of time is consumed by the underlying SAT solver, CryptoMiniSat. This observation motivated us to ask: Can we design an efficient underlying CNF-XOR SAT solver that can take advantage of the structure of hashing-based algorithms and would this lead to an efficient approximate model counter? The primary contribution of this paper is an affirmative answer to the above question. We present a novel architecture, called BIRD, to handle CNF-XOR formulas arising from hashingbased techniques. The resulting hashing-based approximate model counter, called ApproxMC3, employs the BIRD framework in its underlying SAT solver, CryptoMiniSat. To the best of our knowledge, we conducted the most comprehensive study of evaluation performance of counting algorithms involving 1896 benchmarks with computational effort totaling 86400 computational hours. Our experimental evaluation demonstrates significant runtime performance improvement for ApproxMC3 over ApproxMC2. In particular, we solve 648 benchmarks more than ApproxMC2, the state of the art approximate model counter and for all the formulas where both ApproxMC2 and ApproxMC3 did not timeout and took more than 1 seconds, the mean speedup is 284.40 – more than two orders of magnitude.

Style APA, Harvard, Vancouver, ISO itp.

41

Nadel, Alexander. "Polarity and Variable Selection Heuristics for SAT-Based Anytime MaxSAT". Journal on Satisfiability, Boolean Modeling and Computation 12, nr 1 (11.09.2020): 17–22. http://dx.doi.org/10.3233/sat-200126.

Pełny tekst źródła

Streszczenie:

This paper is a system description of the anytime MaxSAT solver TT-Open-WBO-Inc, which won both of the weighted incomplete tracks of MaxSAT Evaluation 2019. We implemented the recently introduced polarity and variable selection heuristics, TORC and TSB, respectively, in the Open-WBO-Inc-BMO algorithm within the open-source anytime MaxSAT solver Open-WBO-Inc. As a result, the solver is substantially more efficient.

Style APA, Harvard, Vancouver, ISO itp.

42

Heule, Marijn, Matti Järvisalo, Florian Lonsing, Martina Seidl i Armin Biere. "Clause Elimination for SAT and QSAT". Journal of Artificial Intelligence Research 53 (26.06.2015): 127–68. http://dx.doi.org/10.1613/jair.4694.

Pełny tekst źródła

Streszczenie:

The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of various computationally hard problems can be efficiently solved. This success has been achieved through several breakthroughs in practical implementations of decision procedures for SAT and QSAT, that is, in SAT and QSAT solvers. Here, simplification techniques for conjunctive normal form (CNF) for SAT and for prenex conjunctive normal form (PCNF) for QSAT---the standard input formats of SAT and QSAT solvers---have recently proven very effective in increasing solver efficiency when applied before (i.e., in preprocessing) or during (i.e., in inprocessing) satisfiability search. In this article, we develop and analyze clause elimination procedures for pre- and inprocessing. Clause elimination procedures form a family of (P)CNF formula simplification techniques which remove clauses that have specific (in practice polynomial-time) redundancy properties while maintaining the satisfiability status of the formulas. Extending known procedures such as tautology, subsumption, and blocked clause elimination, we introduce novel elimination procedures based on asymmetric variants of these techniques, and also develop a novel family of so-called covered clause elimination procedures, as well as natural liftings of the CNF-level procedures to PCNF. We analyze the considered clause elimination procedures from various perspectives. Furthermore, for the variants not preserving logical equivalence under clause elimination, we show how to reconstruct solutions to original CNFs from satisfying assignments to simplified CNFs, which is important for practical applications for the procedures. Complementing the more theoretical analysis, we present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It turns out that the importance of applying the clause elimination procedures developed in this work is empirically emphasized in the context of state-of-the-art QSAT solving.

Style APA, Harvard, Vancouver, ISO itp.

43

Kullmann, Oliver. "The SAT 2005 Solver Competition on Random Instances". Journal on Satisfiability, Boolean Modeling and Computation 2, nr 1-4 (1.03.2006): 61–102. http://dx.doi.org/10.3233/sat190017.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

44

Spence, Ivor. "tts: A SAT-Solver for Small, Difficult Instances". Journal on Satisfiability, Boolean Modeling and Computation 4, nr 2-4 (1.06.2008): 173–90. http://dx.doi.org/10.3233/sat190043.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

45

Park, Sa-Choun, i Gi-Hwon Kwon. "Extracting Subsequence of Boolean Variables using SAT-solver". KIPS Transactions:PartD 15D, nr 6 (31.12.2008): 777–84. http://dx.doi.org/10.3745/kipstd.2008.15-d.6.777.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

46

Inui, Nobuo, i Akiko Aizawa. "Generation of Minimum-Consistent DFA Using SAT Solver". Transactions of the Japanese Society for Artificial Intelligence 27, nr 3 (2012): 151–62. http://dx.doi.org/10.1527/tjsai.27.151.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

47

Horbach, Andrei, Thomas Bartsch i Dirk Briskorn. "Using a SAT-solver to schedule sports leagues". Journal of Scheduling 15, nr 1 (16.09.2010): 117–25. http://dx.doi.org/10.1007/s10951-010-0194-9.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

48

Ulyantsev, Vladimir I., i Fedor N. Tsarev. "Extended Finite-State Machine Induction using SAT-Solver". IFAC Proceedings Volumes 45, nr 6 (maj 2012): 236–41. http://dx.doi.org/10.3182/20120523-3-ro-2023.00179.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

49

Böhm, Max, i Ewald Speckenmeyer. "A fast parallel SAT-solver — efficient workload balancing". Annals of Mathematics and Artificial Intelligence 17, nr 2 (wrzesień 1996): 381–400. http://dx.doi.org/10.1007/bf02127976.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

50

DUCK, GREGORY J. "SMCHR: Satisfiability modulo constraint handling rules". Theory and Practice of Logic Programming 12, nr 4-5 (lipiec 2012): 601–18. http://dx.doi.org/10.1017/s1471068412000208.

Pełny tekst źródła

Streszczenie:

AbstractConstraint Handling Rules (CHRs) are a high-level rule-based programming language for specification and implementation of constraint solvers. CHR manipulates a global store representing a flat conjunction of constraints. By default, CHR does not support goals with a more complex propositional structure including disjunction, negation, etc., or CHR relies on the host system to provide such features. In this paper we introduce Satisfiability Modulo Constraint Handling Rules (SMCHR): a tight integration of CHR with a modern Boolean Satisfiability (SAT) solver for quantifier-free formulae with an arbitrary propositional structure. SMCHR is essentially a Satisfiability Modulo Theories (SMT) solver where the theory T is implemented in CHR. The execution algorithm of SMCHR is based on lazy clause generation, where a new clause for the SAT solver is generated whenever a rule is applied. We shall also explore the practical aspects of building an SMCHR system, including extending a “built-in” constraint solver supporting equality with unification and justifications.

Style APA, Harvard, Vancouver, ISO itp.

Oferujemy zniżki na wszystkie plany premium dla autorów, których prace zostały uwzględnione w tematycznych zestawieniach literatury. Skontaktuj się z nami, aby uzyskać unikalny kod promocyjny!