8 results
Now showing1 - 8 of 8
- Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: without files , SLS-enhanced core-boosted linear search for anytime maximum satisfiability(Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, 2025-08-08); Maximum Satisfiability (MaxSAT), the constraint paradigm of minimizing a linear expression over Boolean (0-1) variables subject to a set of propositional clauses, is today used for solving NP-hard combinatorial optimization problems in various domains. Especially anytime MaxSAT solvers that compute low-cost solutions within a limited available computational time have significantly improved in recent years. Such solvers can be divided into SAT-based methods that use sophisticated reasoning, and stochastic local search (SLS) methods that heuristically explore the search space. The two are complementary; roughly speaking, SLS struggles with finding feasible solutions, and SAT-based methods with minimizing cost. Consequently, most state-of-the-art anytime MaxSAT solvers run SLS before a SAT-based algorithm with minimal communication between the two. In this paper, we aim to harness the complementary strengths of SAT-based, and SLS approaches in the context of anytime MaxSAT. More precisely, we describe several ways to enhance the performance of the so-called core-boosted linear search algorithm for anytime MaxSAT with SLS techniques. Core-boosted linear search is a three-phase algorithm where each phase uses different types of reasoning. Beyond MaxSAT, core-boosted search has also been successful in the related paradigms of pseudo-boolean optimization and constraint programming. We describe how an SLS approach to MaxSAT can be tightly integrated with all three phases of the algorithm, resulting in non-trivial information exchange in both directions between the SLS algorithm and the reasoning methods. We evaluate our techniques on standard benchmarks from the latest MaxSAT Evaluation and demonstrate that our techniques can noticeably improve on implementations of core-boosted search and SLS.Publicationtype: Conference Paper24 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , IGMaxHS - An Incremental MaxSAT Solver with Support for XOR Clauses(2024-10-21)Recently, a novel, MaxSAT-based method for error correction in quantum computing has been proposed that requires both incremental MaxSAT solving capabilities and support for XOR constraints, but no dedicated MaxSAT solver fulfilling these criteria existed yet. We alleviate that and introduce IGMaxHS, which is based on the existing solvers iMaxHS and GaussMaxHS, but poses fewer restrictions on the XOR constraints than GaussMaxHS. IGMaxHS is fuzz tested with xwcnfuzz, an extension of wcnfuzz that can directly output XOR constraints. As a result, IGMaxHS is the only solver that reported neither incorrect unsatisfiability verdicts nor invalid models nor incoherent cost model combinations in a final fuzz testing comparison of all three solvers with 10000 instances. We detail the steps required for implementing Gaussian elimination on XOR constraints in CDCL SAT solvers, and extend the recently proposed re-entrant incremental MaxSAT solver application program interface to allow for incremental addition of XOR constraints. Finally, we show that IGMaxHS is capable of decoding quantum color codes through simulation with the Munich Quantum Toolkit.Publicationtype: Conference Paper not in Proceedings28 41 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , noSAT-MaxSATv3Using a SAT solver to solve MaxSAT is a well-established and efficient method. However, in resource-constrained computing environments, e.g., embedded systems, such algorithm designs can be hard to realize. With noSAT-MaxSAT, we explore alternatives that do not rely on an external, dedicated SAT solver. Compared to the previous version, the most notable changes in noSAT-MaxSATv3 include an update of the base algorithm to NuWLS-2.0, new rules for restarting, the integration of a new Frequency Fitness Assignment-inspired variable selection heuristic in local optima, and the inclusion of fixed-precision integer arithmetic to increase precision in weight calculations without resorting to floating-point numbers.Publicationtype: Conference Paper52 81 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , Sliced online model checking for optimizing the beam scheduling problem in robotic radiation therapyIn robotic radiation therapy, high-energy photon beams from different directions are directed at a target within the patient. Target motion can be tracked by robotic ultrasound and then compensated by synchronous beam motion. However, moving the beams may result in beams passing through the ultrasound transducer or the robot carrying it. While this can be avoided by pausing the beam delivery, the treatment time would increase. Typically, the beams are delivered in an order which minimizes the robot motion and thereby the overall treatment time. However, this order can be changed, i.e., instead of pausing beams, other feasible beam could be delivered. We address this problem of dynamically ordering the beams by applying a model checking paradigm to select feasible beams. Since breathing patterns are complex and change rapidly, any offline model would be too imprecise. Thus, model checking must be conducted online, predicting the patient's current breathing pattern for a short amount of time and checking which beams can be delivered safely. Monitoring the treatment delivery online provides the option to reschedule beams dynamically in order to avoid pausing and hence to reduce treatment time. While human breathing patterns are complex and may change rapidly, we need a model which can be verified quickly and use approximation by a superposition of sine curves. Further, we simplify the 3D breathing motion into separate 1D models. We compensate the simplification by adding noise inside the model itself. In turn, we synchronize between the multiple models representing the different spatial directions, the treatment simulation, and corresponding verification queries. Our preliminary results show a 16.02 % to 37.21 % mean improvement on the idle time compared to a static beam schedule, depending on an additional safety margin. Note that an additional safety margin around the ultrasound robot can decrease idle times but also compromises plan quality by limiting the range of available beam directions. In contrast, the approach using online model checking maintains the plan quality. Further, we compare to a naive machine learning approach that does not achieve its goals while being harder to reason about.Publicationtype: Conference Paper35 62 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , Computer aided design and grading for an electronic functional programming exam(Association for Computing Machinery (ACM), 2023-01); ; ; ; Electronic exams (e-exams) have the potential to substantially reduce the effort required for conducting an exam through automation. Yet, care must be taken to sacrifice neither task complexity nor constructive alignment nor grading fairness in favor of automation. To advance automation in the design and fair grading of (functional programming) e-exams, we introduce the following: A novel algorithm to check Proof Puzzles based on finding correct sequences of proof lines that improves fairness compared to an existing, edit distance based algorithm; an open-source static analysis tool to check source code for task relevant features by traversing the abstract syntax tree; a higher-level language and open-source tool to specify regular expressions that makes creating complex regular expressions less error-prone. Our findings are embedded in a complete experience report on transforming a paper exam to an e-exam. We evaluated the resulting e-exam by analyzing the degree of automation in the grading process, asking students for their opinion, and critically reviewing our own experiences. Almost all tasks can be graded automatically at least in part (correct solutions can almost always be detected as such), the students agree that an e-exam is a fitting examination format for the course but are split on how well they can express their thoughts compared to a paper exam, and examiners enjoy a more time-efficient grading process while the point distribution in the exam results was almost exactly the same compared to a paper exam.Publicationtype: Conference Paper97 57 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , noSAT-MaxSATv2Using a SAT solver to solve MaxSAT is a well-established and efficient method. However, in resource-constrained computing environments, e.g., embedded systems, such algorithm designs can be hard to realize. With noSAT-MaxSAT, we explore alternatives that do not rely on an external, dedicated SAT solver, by executing an anytime local-search MaxSAT solving algorithm only on the hard clauses of the formula instead. In many real-world problems a significant portion of the hard clauses feature not more than two literals. Therefore, in noSAT-MaxSATv2 we integrated a linear-time algorithm for 2-SAT as a preprocessing step to find a good initial assignment before proceeding to solve the remaining hard clauses with local search. Additionally, compared to the previous version of noSAT-MaxSAT, we updated the local-search algorithm from SATLike to NuWLS, the algorithm which won all incomplete tracks of the MaxSAT Evaluation 2022.Publicationtype: Conference Paper25 61 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , noSAT-MaxSATSince 2019, all solvers in the incomplete track of the MaxSAT Evaluation (MSE) include a dedicated SAT solver. In resource-constrained computing environments, e.g., embedded systems, such algorithm designs can be hard to realize. Yet, the MSE results show an undeniable increase in efficiency when using a SAT solver. With noSAT-MaxSAT, we propose to replace the call to a SAT solver by executing the MaxSAT solver only on the hard clauses of the formula instead. The algorithm is based on SATLike, which was was the only algorithm that did not rely on a SAT solver in the MaxSAT Evaluation 2018. Additionally, our implementation satisfies a set of requirements often found in embedded system software.Publicationtype: Conference Paper113 190 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: without files , WCET-aware reachability for verified simplex design: work-in-progress(2021-09-30); Previous online reachability algorithms for hybrid automata reduced conservatism in verified Simplex controller architectures, but were restricted to the imprecise real-time paradigm, i.e., their precision increases over time. Yet, many safety-critical cyber-physical systems are hard real-time systems, requiring an upper bound on the worst-case execution time (WCET) of each task to be known. We show that the iteration bound of the reachability loop can be parameterized by a single factor which determines the precision. Consequently, an algorithm could select a fixed precision depending on the time left until its deadline. In this paper we present such a WCET-aware reachability algorithm, based on an existing algorithm for imprecise real-time. Its smallest WCET bound on an Infineon XMC4500 microprocessor is 32.861 milliseconds.Publicationtype: Conference Paper98