1,382 research outputs found
Popularity-similarity random SAT formulas
No full text[EN]In the last decades, we have witnessed a remarkable success of algorithms solving the Boolean Satisfiability problem (SAT) on instances encoding application or real-world problems arising from a very diverse number of domains, such as hardware and software verification, planning or cryptography. These algorithms are the so known Conflict-Driven Clause Learning (CDCL) SAT solvers. Interestingly enough, the reasons for the success of these solvers on this diverse range of problems are not completely understood yet.
A common issue when facing this open challenge is the heterogeneity of this set of benchmarks. Another problem is the limited number of existing instances. In this context, random models of SAT formulas capturing features shared by the majority of these application benchmarks become crucial, for both theoretical and practical purposes. On the one hand, it is undoubtedly necessary to have random models where theoretical properties, like hardness, can be studied. Therefore, realistic random SAT models may contribute to explain the success of these solvers on these industrial problems. On the other hand, the limited number of benchmarks and their hardness in practice makes the evaluation of new solving techniques a costly task. Therefore, these realistic random SAT generators can provide an unlimited number of pseudo-industrial random SAT instances with some desired properties.
In this work, we present a random SAT instances generator based on the notion of locality. This notion is complementary to the popularity of variables, which is present in the scale-free structure, observable in actual application problems and achievable by previous generators. Our random SAT model combines both locality and popularity, and we show that they are two decisive dimensions of attractiveness among the variables of a formula, and how CDCL SAT solvers take advantage of them. Locality is closely related to the community structure, another important feature of application SAT benchmarks, which is indirectly achieved by this model. To the best of our knowledge, this is the first random SAT model that generates both scale-free structure and community structure at once.This work is partially supported by the EU H2020 Research and Innovation Programme under the LOGISTAR
project (Grant Agreement No. 769142), and by the Spanish Ministry of Science, Innovation and Universities and
the Spanish National Agency of Research (AEI) under the projects RASO (TIN2015-71799-C2-1-P) and EXASOCO
(PGC2018-101216-B-I00), and by the Andalusian Government and the University of Granada under project AIMAR
(A-TIC-284-UGR18), including European Regional Development Funds (ERDF). The first author is also supported
by a MICINN Juan de la Cierva fellowship (grant FJCI-2017-32420).Peer reviewe
Enhancing SAT Based Planning with Landmark Knowledge
No full textSeveral approaches exist to solve Artificial Intelligence planning problems, but little attention has been given to the combination of using landmark knowledge and satisfiability (SAT). Landmark knowledge has been exploited successfully in the heuristics of classical planning. Recently it was also shown that landmark knowledge can improve the performance of SAT based planners, but it was unclear how and in which domains they were effective. We investigate the relationship between landmarks and plan generation performance in SAT. We discuss a recently proposed heuristic for planning using SAT and suggest improvements. We compare the effects of landmark knowledge in parallel and sequential planning, also looking at previous research. It turns out that landmark knowledge can be beneficial, but performance highly depends on the planning domain and the planning problem itself.Software Computer TechnologyElectrical Engineering, Mathematics and Computer Scienc
Algorithmic QUBO formulations for k-SAT and hamiltonian cycles
No full textQuadratic Unconstrained Binary Optimization (QUBO) can be seen as a generic language for optimization problems. QUBOs attract particular attention since they can be solved with quantum hardware, like quantum annealers or quantum gate computers running QAOA. In this paper, we present two novel QUBO formulations for k-SAT and Hamiltonian Cycles that scale significantly better than existing approaches. For k-SAT we reduce the growth of the QUBO matrix from O(k) to O(log(k)). For Hamiltonian Cycles the matrix no longer grows quadratically in the number of nodes, as currently, but linearly in the number of edges and logarithmically in the number of nodes. We present these two formulations not as mathematical expressions, as most QUBO formulations are, but as meta-algorithms that facilitate the design of more complex QUBO formulations and allow easy reuse in larger and more complex QUBO formulations.Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.Quantum Circuit Architectures and Technolog
VDE-SAT Ranging for Critical Navigation: Characteristics of Experimental VDE-SAT Ranging Signals and System Performance Analysis for Critical Navigation
No full textTraditional Global Navigation Satellite Systems (GNSS) are subject to intentional or unintentional disturbances in the northern regions of Norway, leading to loss of critical infrastructure. The novel VHF Data Exchange System (VDES) has been suggested as an alternative positioning, navigation and timing (PNT) system for a possible GNSS contingency service, based on signal simulations and statistical estimates. However, an empirical investigation into the feasibility of such a GNSS contingency service remains to be done, and has only recently become possible after the launch of the NorSat-TD satellite with purpose-designed VDES ranging capabilities. This paper presents an analysis of the characteristics of empirical VDE-SAT range measurements and a system-level performance analysis of a GNSS-contingency system based on the signal performance of empirical ranging data gathered from NorSat-TD. Using the equated error level of the signal, the positioning performance of simulated autonomous systems of VDE-SAT PNT-sources is analysed, followed by an assessment of the combination of the empirical VDE-SAT range measurements and traditional GNSS measurements in a critical GNSS contingency scenario. In total, 236 VDE-SAT pseudorange observations obtained from eleven satellite passes recorded in July 2023 were used. Residual analysis shows that these observations have a large and constant mean error of about 416 km, with a standard deviation of 260.8 m. The previously neglected atmospheric propagation effects on a VDE-SAT range measurement is shown to be significant, and the largest effect is likely to be the time-delay due to the ionosphere. The system performance analysis shows that VDE-SAT as a PNT-source could be used as a possible future general navigation backup system, with a positioning accuracy within 1000 m. Finally, an important conclusion is that a contemporary GNSS-contingency system is possible with the measured signal performance, where NorSat-TD acting as a PNT-source can, under the correct geometric conditions, allow a positioning accuracy within 1000 m in combination with partial GNSS coverage at the user.Aerospace Engineerin
Mai sat
No full textThe author explains the development of intonation and the use of ""Mai sat"", a mark for an intonation in Lanna language, which is dialect used by people in the North of Thailand
Width-parameterized SAT: time-space tradeoffs,
No full textAlekhnovich and Razborov (2002) presented an algorithm that solves SAT on instances ϕ of size n and tree-width TW(ϕ), using time and space bounded by 2O(TW(ϕ))nO(1). Although several follow-up works appeared over the last decade, the first open question of Alekhnovich and Razborov remained essentially unresolved: Can one check satisfiability of formulas with small tree-width in polynomial space and time as above? We essentially resolve this question, by (1) giving a polynomial space algorithm with a slightly worse run-time, (2) providing a complexity-theoretic characterization of bounded tree-width SAT, which strongly suggests that no polynomial-space algorithm can run significantly faster, and (3) presenting a spectrum of algorithms trading off time for space, between our PSPACE algorithm and the fastest known algorithm.
First, we give a simple algorithm that runs in polynomial space and achieves run-time 3TW(ϕ)lognnO(1), which approaches the run-time of Alekhnovich and Razborov (2002), but has an additional log n factor in the exponent. Then, we conjecture that this annoying log n factor is in general unavoidable.
Our negative results show our conjecture true if one believes a well-known complexity assumption, which is the SC ≠ NC conjecture and its scaled variants. Technically, we base our result on the following lemma. For arbitrary k, SAT of tree-width logkn is complete for the class of problems computed by circuits of logarithmic depth, semi-unbounded fan-in and size 2O(logkn) (SAC1 when k=1). Problems in this class can be solved simultaneously in time-space (2O(logk+1n),O(logk+1n)), and also in (2O(logkn), 2O(logkn)). Then, we show that our conjecture (for SAT instances with poly-log tree-width) is equivalent to the question of whether the small-space simulation of semi-unbounded circuit classes can be sped up without incurring a large space penalty. This is a recasting of the conjecture that SAC1 (and even its subclass NL) is not contained in SC.
Although we cannot hope for an improvement asymptotically in the exponent of time and space, we introduce a new algorithmic technique which trades constants in the exponents: for each ε with 0<ε<1, we give an algorithm in time-space
(31.441(1−ε)TW(ϕ)log|ϕ||ϕ|O(1),22εTW(ϕ)|ϕ|O(1)).
We systematically study the limitations of our technique for trading off time and space, and we show that our bounds are the best achievable using this technique.Licensed under a Creative Commons Attribution License (CC-BY) http://creativecommons.org/licenses/by/3.0/Peer reviewe
New inference rules for max-SAT
No full textExact 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. © 2007 AI Access Foundation. All rights reserved.Research partially supported by projects TIN2004-07933-C03-03 and TIN2006-15662-C02-02 funded by the
Ministerio de Educación y Ciencia. The first author was partially supported by National 973 Program of China under Grant No. 2005CB321900. The second author was supported by a grant Ramón y Cajal.Peer Reviewe
SDP-based Max-2-Sat Decomposition
No full textThe Max-Sat problem has been intensively studied during the past few decades. Semi-definite programming based approximation algorithms provide good approximation ratios and polynomial runtime solutions to this problem. Unfortunately the high degree of their polynomial runtime prevents their application to problems with a large number of variables. We've investigated the possibility of decomposing Max-Sat problems to reduce the number of variables in the problems supplied to SDP solvers. We've considered several forms of decomposition and evaluated these empirically. The methods we investigated were able to approach the lower bounds of SDP within 2% but do not provide performance guarantees and cannot compete with conventional local search methods.AlgorithmicsSoftware TechnologyElectrical Engineering, Mathematics and Computer Scienc
Structured problems for SAT
No full textTitle: Structured problems for SAT Author: Jan Klátil Department: Department of Theoretical Computer Science and Mathematical Logic Supervisor: RNDr. Jan Hric, Department of Theoretical Computer Science and Mathematical Logic Abstract: Aim of this thesis is to implement generator of unstructured data of CSP model RB in format XCSP and several other generators of structured data in formats XCSP and DIMACS, which are based on problems of placing N-Queens, finding Hamiltonian cycle and dividing set of integers into two distinct subsets with equal sum. We compare generated data in both XCSP and DIMACS format based on same problem by comparing time spent by SAT solver RSAT solving this data. Both forced satisfiable and unsatisfiable data and joined unstructured a structured data in XCSP format were compared in this thesis. Keywords: structured problems, SAT
Incorporating flexible track use in the SAT model of the Dutch railway timetabling problem
No full textThe construction of cyclic railway timetables is an important task for Netherlands Railways (NS).This construction can be formulated as a Periodic Event Scheduling Problem (PESP). The most powerful technique for solving cyclic railway timetabling problems is constraint programming, especially via SAT solvers when PESP instances are encoded as SAT instances. SAT solvers can determine the feasibility of problem instances of NS quickly and reliably. However, in previous implementations the problem specification must explicitly indicate the track use within stations and on four-track sections. As a result, the solver also reports infeasibility if a small adjustment of the track allocation could lead to a feasible timetable. In this thesis, the Open Periodic Event Scheduling Problem (OPESP) is introduced, which is used in a new method to incorporate flexible track use in the SAT formulation. This method yields promising results that could help improve the timetabling process at NS
- …
