Relevant bibliographies by topics / SAT solver

Academic literature on the topic 'SAT solver'

Author: Grafiati
Published: 4 June 2021
Last updated: 22 June 2023

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Contents

Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'SAT solver.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Journal articles on the topic "SAT solver"

1

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
2

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
3

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
4

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
5

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
6

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
7

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
8

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
9

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
10

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
More sources

Dissertations / Theses on the topic "SAT solver"

1

Izrael, Petr. "SAT Solver akcelerovaný pomocí GPU." Master's thesis, Vysoké učení technické v Brně. Fakulta informačních technologií, 2013. http://www.nusl.cz/ntk/nusl-236336.

Full text
Abstract:
This thesis is concerned with design and implementation of a complete SAT solver accelerated on GPU. The achitecture of modern graphics cards is described as well as the CUDA platform and a list of common algorithms used for solving the boolean satisfiability problem (the SAT problem). The presented solution is based on the 3-SAT DC alogirthm, which belongs to the family of well-known DPLL based algorithms. This work describes problems encountered during the design and implementation. The resulting application was then analyzed and optimized. The presented solver cannot compete with state of the art solvers, but proves that it can be up to 21x faster than an equivalent sequential version. Unfortunately, the current implementation can only handle formulas of a limited size. Suggestions on further improvements are given in final sections.
APA, Harvard, Vancouver, ISO, and other styles
2

Kokotov, Daniel (Daniel L. ). 1978. "PSolver : a distributed SAT solver framework." Thesis, Massachusetts Institute of Technology, 2001. http://hdl.handle.net/1721.1/86807.

Full text
Abstract:
Thesis (M.Eng. and S.B.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2001.
Includes bibliographical references (p. 129-130).
by Daniel Kokotov.
M.Eng.and S.B.
APA, Harvard, Vancouver, ISO, and other styles
3

Pilz, Enrico. "Boolsche Gleichungssysteme, SAT Solver und Stromchiffren." [S.l. : s.n.], 2008. http://nbn-resolving.de/urn:nbn:de:bsz:289-vts-65265.

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

Le, Piane Fabio. "Il teorema di Cook-Levin e i SAT-solver." Bachelor's thesis, Alma Mater Studiorum - Università di Bologna, 2015. http://amslaurea.unibo.it/9026/.

Full text
Abstract:
In questa tesi è trattato il tema della soddisfacibilità booleana o proposizionale, detta anche SAT, ovvero il problema di determinare se una formula booleana è soddisfacibile o meno. Soddisfacibile significa che è possibile assegnare le variabili in modo che la formula assuma il valore di verità vero; viceversa si dice insoddisfacibile se tale assegnamento non esiste e se quindi la formula esprime una funzione identicamente falsa. A tal fine si introducono degli strumenti preliminari che permetteranno di affrontare più approfonditamente la questione, partendo dalla definizione basilare di macchina di Turing, affrontando poi le classi di complessità e la riduzione, la nozione di NP-completezza e si dimostra poi che SAT è un problema NP-completo. Infine è fornita una definizione generale di SAT-solver e si discutono due dei principali algoritmi utilizzati a tale scopo.
APA, Harvard, Vancouver, ISO, and other styles
5

Zhao, Yuting. "Answer set programming : SAT based solver and phase transition /." View abstract or full-text, 2003. http://library.ust.hk/cgi/db/thesis.pl?COMP%202003%20ZHAOY.

Full text
APA, Harvard, Vancouver, ISO, and other styles
6

Pintjuk, Daniil. "Boosting SAT-solver Performance on FACT Instances with Automatic Parameter Tuning." Thesis, KTH, Skolan för datavetenskap och kommunikation (CSC), 2015. http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-166552.

Full text
Abstract:
Previous work by Asketorp [2014] has shown that integer factorization with the best SAT-solvers is orders of magnitude slower then with general number field sieve (GNFS). However only default configurations for the tested SAT-solvers ware considered in thous tests therefor this rapport attempts to explore what difference use of good configurations would have made. Our method involved using automatic parameter tunning with the algorithm iterated local search (ILS). ILS was used to tune the sat solver Minisat. And the tuned configuration was compared with the default by timing Minisat runs with respective configurations. The results show that performance gains are far from being big enough to suggest that the SAT-solvers tested by Asketorp [2014], would have come much closer to the performance of GNFS if tuned configurations were used. However the performance gains achieved in this report are impressive enough to advocate the use of automated parameter tuning of Sat-solvers for specific sets of instances.
APA, Harvard, Vancouver, ISO, and other styles
7

Subramanian, Rishi Bharadwaj. "FPGA Based Satisfiability Checking." University of Cincinnati / OhioLINK, 2020. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1583154848438753.

Full text
APA, Harvard, Vancouver, ISO, and other styles
8

Hoessen, Benoît. "Solving the Boolean satisfiability problem using the parallel paradigm." Thesis, Artois, 2014. http://www.theses.fr/2014ARTO0406/document.

Full text
Abstract:
Cette thèse présente différentes techniques permettant de résoudre le problème de satisfaction de formule booléenes utilisant le parallélisme et du calcul distribué. Dans le but de fournir une explication la plus complète possible, une présentation détaillée de l'algorithme CDCL est effectuée, suivi d'un état de l'art. De ce point de départ, deux pistes sont explorées. La première est une amélioration d'un algorithme de type portfolio, permettant d'échanger plus d'informations sans perte d'efficacité. La seconde est une bibliothèque de fonctions avec son interface de programmation permettant de créer facilement des solveurs SAT distribués
This thesis presents different technique to solve the Boolean satisfiability problem using parallel and distributed architectures. In order to provide a complete explanation, a careful presentation of the CDCL algorithm is made, followed by the state of the art in this domain. Once presented, two propositions are made. The first one is an improvement on a portfolio algorithm, allowing to exchange more data without loosing efficiency. The second is a complete library with its API allowing to easily create distributed SAT solver
APA, Harvard, Vancouver, ISO, and other styles
9

Silveira, Jaime Kirch da. "Parallel SAT solvers and their application in automatic parallelization." reponame:Biblioteca Digital de Teses e Dissertações da UFRGS, 2014. http://hdl.handle.net/10183/95373.

Full text
Abstract:
Desde a diminuição da tendência de aumento na frequência de processadores, uma nova tendência surgiu para permitir que softwares tirem proveito de harwares mais rápidos: a paralelização. Contudo, diferente de aumentar a frequência de processadores, utilizar parallelização requer um tipo diferente de programação, a programação paralela, que é geralmente mais difícil que a programação sequencial comum. Neste contexto, a paralelização automática apareceu, permitindo que o software tire proveito do paralelismo sem a necessidade de programação paralela. Nós apresentamos aqui duas propostas: SAT-PaDdlinG e RePaSAT. SAT-PaDdlinG é um SAT Solver DPLL paralelo que roda em GPU, o que permite que RePaSAT utilize esse ambiente. RePaSAT é a nossa proposta de uma máquina paralela que utiliza o Problema SAT para paralelizar automaticamente código sequencial. Como uma GPU provê um ambiente barato e massivamente paralelo, SAT-PaDdlinG tem como objetivo prover esse paralelismo massivo a baixo custo para RePaSAT, como para qualquer outra ferramenta ou problema que utilize SAT Solvers.
Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization. However, different from increasing the frequency of processors, using parallelization requires a different kind of programming, parallel programming, which is usually harder than common sequential programming. In this context, automatic parallelization has arisen, allowing software to take advantage of parallelism without the need of parallel programming. We present here two proposals: SAT-PaDdlinG and RePaSAT. SAT-PaDdlinG is a parallel DPLL SAT Solver on GPU, which allows RePaSAT to use this environment. RePaSAT is our proposal of a parallel machine that uses the SAT Problem to automatically parallelize sequential code. Because GPU provides a cheap, massively parallel environment, SATPaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.
APA, Harvard, Vancouver, ISO, and other styles
10

Kibria, Raihan Hassnain [Verfasser], and Hans [Akademischer Betreuer] Eveking. "Soft Computing Approaches to DPLL SAT Solver Optimization / Raihan Hassnain Kibria. Betreuer: Hans Eveking." Darmstadt : Universitäts- und Landesbibliothek Darmstadt, 2011. http://d-nb.info/1105563952/34.

Full text
APA, Harvard, Vancouver, ISO, and other styles
More sources

Books on the topic "SAT solver"

1

Halvorson, Christine. Solve it with salt and vinegar. Lincolnwood, Ill: Publications International, 2002.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
2

Mailer, Carol. Jumping problems solved: Gridwork, the secret to success. North Pomfret, VT: Trafalgar Square Pub., 2005.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
3

Corrigan, Peter. Soldier U: SAS: Bandit country. Rochester: 22 Books, 1995.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
4

Sam Houston: Soldier and statesman. Mankato, Minn: Bridgestone Books, 2003.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
5

San Martín: Argentine soldier, American hero. New Haven: Yale University Press, 2009.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
6

Soldier A : SAS: Behind Iraqui lines. London: 22, 1993.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
7

Soldier R: SAS: Death on Gibraltar. Rochester: 22 Books, 1994.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
8

Soldier N: SAS: The Gambian bluff. Rochester: 22 Books, 1994.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
9

Clarke, Shaun. Soldier A: SAS: Behind Iraqi lines. Bath: Chivers Large Print, 1994.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
10

Solve it with salt: 110 surprising and ingenious household uses for table salt. New York: Three Rivers Press, 1998.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
More sources

Book chapters on the topic "SAT solver"

1

Eén, Niklas, and Niklas Sörensson. "An Extensible SAT-solver." In Theory and Applications of Satisfiability Testing, 502–18. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004. http://dx.doi.org/10.1007/978-3-540-24605-3_37.

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

Fuchs, Tobias, Jakob Bach, and Markus Iser. "Active Learning for SAT Solver Benchmarking." In Tools and Algorithms for the Construction and Analysis of Systems, 407–25. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-30823-9_21.

Full text
Abstract:
AbstractBenchmarking is a crucial phase when developing algorithms. This also applies to solvers for the SAT (propositional satisfiability) problem. Benchmark selection is about choosing representative problem instances that reliably discriminate solvers based on their runtime. In this paper, we present a dynamic benchmark selection approach based on active learning. Our approach predicts the rank of a new solver among its competitors with minimum runtime and maximum rank prediction accuracy. We evaluated this approach on the Anniversary Track dataset from the 2022 SAT Competition. Our selection approach can predict the rank of a new solver after about 10 % of the time it would take to run the solver on all instances of this dataset, with a prediction accuracy of about 92 %. We also discuss the importance of instance families in the selection process. Overall, our tool provides a reliable way for solver engineers to determine a new solver’s performance efficiently.
APA, Harvard, Vancouver, ISO, and other styles
3

Fleury, Mathias. "Optimizing a Verified SAT Solver." In Lecture Notes in Computer Science, 148–65. Cham: Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-20652-9_10.

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

Audemard, Gilles, Jean-Marie Lagniez, Nicolas Szczepanski, and Sébastien Tabary. "An Adaptive Parallel SAT Solver." In Lecture Notes in Computer Science, 30–48. Cham: Springer International Publishing, 2016. http://dx.doi.org/10.1007/978-3-319-44953-1_3.

Full text
APA, Harvard, Vancouver, ISO, and other styles
5

Mahajan, Yogesh S., Zhaohui Fu, and Sharad Malik. "Zchaff2004: An Efficient SAT Solver." In Theory and Applications of Satisfiability Testing, 360–75. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005. http://dx.doi.org/10.1007/11527695_27.

Full text
APA, Harvard, Vancouver, ISO, and other styles
6

Ohmura, Kei, and Kazunori Ueda. "c-sat: A Parallel SAT Solver for Clusters." In Lecture Notes in Computer Science, 524–37. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009. http://dx.doi.org/10.1007/978-3-642-02777-2_47.

Full text
APA, Harvard, Vancouver, ISO, and other styles
7

Bryant, Randal E., Armin Biere, and Marijn J. H. Heule. "Clausal Proofs for Pseudo-Boolean Reasoning." In Tools and Algorithms for the Construction and Analysis of Systems, 443–61. Cham: Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-030-99524-9_25.

Full text
Abstract:
AbstractWhen augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs.
APA, Harvard, Vancouver, ISO, and other styles
8

Manthey, Norbert. "The MergeSat Solver." In Theory and Applications of Satisfiability Testing – SAT 2021, 387–98. Cham: Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-80223-3_27.

Full text
APA, Harvard, Vancouver, ISO, and other styles
9

Oe, Duckki, Aaron Stump, Corey Oliver, and Kevin Clancy. "versat: A Verified Modern SAT Solver." In Lecture Notes in Computer Science, 363–78. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. http://dx.doi.org/10.1007/978-3-642-27940-9_24.

Full text
APA, Harvard, Vancouver, ISO, and other styles
10

Jain, Siddhartha, Eoin O’Mahony, and Meinolf Sellmann. "A Complete Multi-valued SAT Solver." In Principles and Practice of Constraint Programming – CP 2010, 281–96. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010. http://dx.doi.org/10.1007/978-3-642-15396-9_24.

Full text
APA, Harvard, Vancouver, ISO, and other styles

Conference papers on the topic "SAT solver"

1

Safar, Mona, M. El-kharashi, and Ashraf Salem. "FPGA-Based SAT Solver." In 2006 Canadian Conference on Electrical and Computer Engineering. IEEE, 2006. http://dx.doi.org/10.1109/ccece.2006.277452.

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

Ustaoglu, Buse, Sebastian Huhn, Frank Sill Torres, Daniel Grosse, and Rolf Drechsler. "SAT-Hard: A Learning-Based Hardware SAT-Solver." In 2019 22nd Euromicro Conference on Digital System Design (DSD). IEEE, 2019. http://dx.doi.org/10.1109/dsd.2019.00021.

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

Browning, B., and A. Remshagen. "A SAT-based solver for Q-ALL SAT." In the 44th annual southeast regional conference. New York, New York, USA: ACM Press, 2006. http://dx.doi.org/10.1145/1185448.1185456.

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

Gong, Weiwei, and Xu Zhou. "A survey of SAT solver." In APPLIED MATHEMATICS AND COMPUTER SCIENCE: Proceedings of the 1st International Conference on Applied Mathematics and Computer Science. Author(s), 2017. http://dx.doi.org/10.1063/1.4981999.

Full text
APA, Harvard, Vancouver, ISO, and other styles
5

Ozolins, Emils, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Kozlovics. "Goal-Aware Neural SAT Solver." In 2022 International Joint Conference on Neural Networks (IJCNN). IEEE, 2022. http://dx.doi.org/10.1109/ijcnn55064.2022.9892733.

Full text
APA, Harvard, Vancouver, ISO, and other styles
6

Luo, Mao, Chu-Min Li, Fan Xiao, Felip Manyà, and Zhipeng Lü. "An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers." In Twenty-Sixth International Joint Conference on Artificial Intelligence. California: International Joint Conferences on Artificial Intelligence Organization, 2017. http://dx.doi.org/10.24963/ijcai.2017/98.

Full text
Abstract:
Learnt clauses in CDCL SAT solvers often contain redundant literals. This may have a negative impact on performance because redundant literals may deteriorate both the effectiveness of Boolean constraint propagation and the quality of subsequent learnt clauses. To overcome this drawback, we define a new inprocessing SAT approach which eliminates redundant literals from learnt clauses by applying Boolean constraint propagation. Learnt clause minimization is activated before the SAT solver triggers some selected restarts, and affects only some learnt clauses during the search process. Moreover, we conducted an empirical evaluation on instances coming from the hard combinatorial and application categories of recent SAT competitions. The results show that a remarkable number of additional instances are solved when the approach is incorporated into five of the best performing CDCL SAT solvers (Glucose, TC_Glucose, COMiniSatPS, MapleCOMSPS and MapleCOMSPS_LRB).
APA, Harvard, Vancouver, ISO, and other styles
7

Amendola, Giovanni, Carmine Dodaro, and Marco Maratea. "A Formal Approach for Cautious Reasoning in Answer Set Programming (Extended Abstract)." In Twenty-Ninth International Joint Conference on Artificial Intelligence and Seventeenth Pacific Rim International Conference on Artificial Intelligence {IJCAI-PRICAI-20}. California: International Joint Conferences on Artificial Intelligence Organization, 2020. http://dx.doi.org/10.24963/ijcai.2020/652.

Full text
Abstract:
The issue of describing in a formal way solving algorithms in various fields such as Propositional Satisfiability (SAT), Quantified SAT, Satisfiability Modulo Theories, Answer Set Programming (ASP), and Constraint ASP, has been relatively recently solved employing abstract solvers. In this paper we deal with cautious reasoning tasks in ASP, and design, implement and test novel abstract solutions, borrowed from backbone computation in SAT. By employing abstract solvers, we also formally show that the algorithms for solving cautious reasoning tasks in ASP are strongly related to those for computing backbones of Boolean formulas. Some of the new solutions have been implemented in the ASP solver WASP, and tested.
APA, Harvard, Vancouver, ISO, and other styles
8

Meyer, Q., F. Schönfeld, M. Stamminger, and R. Wanka. "3-SAT on CUDA: Towards a massively parallel SAT solver." In Simulation (HPCS 2010). IEEE, 2010. http://dx.doi.org/10.1109/hpcs.2010.5547116.

Full text
APA, Harvard, Vancouver, ISO, and other styles
9

Vieira, Bernardo C., Fabrício V. Andrade, and Antônio O. Fernandes. "A modular CNF-based SAT solver." In the 23rd symposium. New York, New York, USA: ACM Press, 2010. http://dx.doi.org/10.1145/1854153.1854202.

Full text
APA, Harvard, Vancouver, ISO, and other styles
10

Hara, Kazuaki, Naoki Takeuchi, Masashi Aono, and Yuko Hara-Azumi. "Amoeba-Inspired Stochastic Hardware SAT Solver." In 2019 20th International Symposium on Quality Electronic Design (ISQED). IEEE, 2019. http://dx.doi.org/10.1109/isqed.2019.8697729.

Full text
APA, Harvard, Vancouver, ISO, and other styles

Reports on the topic "SAT solver"

1

Baader, Franz, Pavlos Marantidis, and Alexander Okhotin. Approximately Solving Set Equations. Technische Universität Dresden, 2016. http://dx.doi.org/10.25368/2022.227.

Full text
Abstract:
Unification with constants modulo the theory ACUI of an associative (A), commutative (C) and idempotent (I) binary function symbol with a unit (U) corresponds to solving a very simple type of set equations. It is well-known that solvability of systems of such equations can be decided in polynomial time by reducing it to satisfiability of propositional Horn formulae. Here we introduce a modified version of this problem by no longer requiring all equations to be completely solved, but allowing for a certain number of violations of the equations. We introduce three different ways of counting the number of violations, and investigate the complexity of the respective decision problem, i.e., the problem of deciding whether there is an assignment that solves the system with at most l violations for a given threshold value l.
APA, Harvard, Vancouver, ISO, and other styles
2

Malik, Sharad. Augmenting SAT Solvers for Network Configuration/Planning. Fort Belvoir, VA: Defense Technical Information Center, November 2006. http://dx.doi.org/10.21236/ada459907.

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

Baader, Franz, and Barbara Morawska. Matching with respect to general concept inclusions in the Description Logic EL. Technische Universität Dresden, 2014. http://dx.doi.org/10.25368/2022.205.

Full text
Abstract:
Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics (DLs) almost 20 years ago, motivated by applications in the Classic system. For the DL EL, it was shown in 2000 that the matching problem is NP-complete. It then took almost 10 years before this NP-completeness result could be extended from matching to unification in EL. The next big challenge was then to further extend these results from matching and unification without a TBox to matching and unification w.r.t. a general TBox, i.e., a finite set of general concept inclusions. For unification, we could show some partial results for general TBoxes that satisfy a certain restriction on cyclic dependencies between concepts, but the general case is still open. For matching, we solve the general case in this paper: we show that matching in EL w.r.t. general TBoxes is NP-complete by introducing a goal-oriented matching algorithm that uses non-deterministic rules to transform a given matching problem into a solved form by a polynomial number of rule applications. We also investigate some tractable variants of the matching problem.
APA, Harvard, Vancouver, ISO, and other styles
4

Bannochie, C. Results of Hg speciation testing on 3Q15 tank 50, salt solution feed tank (SSFT), and solvent hold tank (SHT) materials. Office of Scientific and Technical Information (OSTI), August 2015. http://dx.doi.org/10.2172/1212656.

Full text
APA, Harvard, Vancouver, ISO, and other styles
5

Rodier, Caroline, Andrea Broaddus, Miguel Jaller, Jeffery Song, Joschka Bischoff, and Yunwan Zhang. Cost-Benefit Analysis of Novel Access Modes: A Case Study in the San Francisco Bay Area. Mineta Transportation Institute, November 2020. http://dx.doi.org/10.31979/mti.2020.1816.

Full text
Abstract:
The first-mile, last-mile problem is a significant deterrent for potential transit riders, especially in suburban neighborhoods with low density. Transit agencies have typically sought to solve this problem by adding parking spaces near transit stations and adding stops to connect riders to fixed-route transit. However, these measures are often only short-term solutions. In the last few years, transit agencies have tested whether new mobility services, such as ridehailing, ridesharing, and microtransit, can offer fast, reliable connections to and from transit stations. However, there is limited research that evaluates the potential impacts of these projects. Concurrently, there is growing interest in the future of automated vehicles (AVs) and the potential of AVs to solve this first-mile problem by reducing the cost of providing these new mobility services to promote access to transit. This paper expands upon existing research to model the simulate the travel and revenue impacts of a fleet of automated vehicles that provide transit access services in the San Francisco Bay Area offered over a range of fares. The model simulates a fleet of AVs for first-mile transit access at different price points for three different service models (door-to-door ridehailing and ridesharing and meeting point ridesharing services). These service models include home-based drop-off and pick-up for single passenger service (e.g., Uber and Lyft), home-based drop-off and pick-up for multi-passenger service (e.g., microtransit), and meeting point multi-passenger service (e.g., Via).
APA, Harvard, Vancouver, ISO, and other styles
6

Kolb, G., D. Neary, M. Ringham, and T. Greenlee. Dynamic simulation of a molten-salt solar receiver. Office of Scientific and Technical Information (OSTI), March 1989. http://dx.doi.org/10.2172/6346050.

Full text
APA, Harvard, Vancouver, ISO, and other styles
7

Gölles, Markus, Viktor Unterberger, Valentin Kaisermayer, Thomas Nigitz, and Daniel Muschick. Supervisory control of large-scale solar thermal systems. IEA SHC Task 55, January 2021. http://dx.doi.org/10.18777/ieashc-task55-2021-0001.

Full text
Abstract:
Overview on different approaches for supervisory control strategies, deciding on operating modes and set points for the controls of the different plants and components integrated in solar thermal systems.
APA, Harvard, Vancouver, ISO, and other styles
8

Rapp, Jim, Ken Duncan, and Steve Albert. Solar Feasibility Study May 2013 - San Carlos Apache Tribe. Office of Scientific and Technical Information (OSTI), May 2013. http://dx.doi.org/10.2172/1132530.

Full text
APA, Harvard, Vancouver, ISO, and other styles
9

Moridis, G. J. A new set of direct and iterative solvers for the TOUGH2 family of codes. Office of Scientific and Technical Information (OSTI), April 1995. http://dx.doi.org/10.2172/72891.

Full text
APA, Harvard, Vancouver, ISO, and other styles
10

Peters, T. B., F. F. Fondeur, and K. M. L. Taylor-Pashow. Results From The Salt Disposition Project Next Generation Solvent Demonstration Plan. Office of Scientific and Technical Information (OSTI), April 2014. http://dx.doi.org/10.2172/1127074.

Full text
APA, Harvard, Vancouver, ISO, and other styles
You might also be interested in the extended bibliographies on the topic 'SAT solver' for particular source types:
Journal articles Dissertations / Theses Books
We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!

To the bibliography