No description available.

Made available in DSpace on 2016-12-23T14:33:34Z (GMT). No. of bitstreams: 1 dissertacao.pdf: 412800 bytes, checksum: 479ec97937646fdcffeadd81d19f1b7a (MD5) Previous issue date: 2006-06-01 / Computar a solução ótima para uma unidade de problema MAX-SAT Ponderado (weighted maximum satisfiability) é difícil mesmo se cada cláusula contiver apenas dois literais. Neste trabalho, será descrita a implementação de uma nova heurística aplicada a instâncias de problema do tipo MAX-SAT Ponderado, mas perfeitamente extensível a outros problemas. Para comparação, serão geradas soluções para uma quantidade significativa de problemas e seus resultados serão comparados com os de outras heurísticas já desenvolvidas para esse tipo de problema, dentre elas as heurísticas consideradas "estado da arte", ou seja, heurísticas que têm obtido os melhores resultados no universo das heurísticas existentes.

Programmers often have to spend a significant amount of time inspecting the software code and execution traces to identify the root cause of a software bug. For a multithreaded program, debugging is even more challenging due to the subtle interactions between concurrent threads and the often astronomical number of possible interleavings. In this work, we propose a logical constraint-based symbolic analysis method to aid in the diagnosis of concurrency bugs and find their root causes, which can be later used to recommend repairs. In our method, the diagnosis process is formulated as a set of constraint solving problems. By leveraging the power of constraint satisfiability (SAT) solvers and a bounded model checker, we perform a semantic analysis of the sequential computation as well as the thread interactions. The analysis is ideally suited for handling software with small to medium code size but complex concurrency control, such as device drivers, synchronization protocols, and concurrent data structures. We have implemented our method in a software tool and demonstrated its effectiveness in diagnosing subtle concurrency bugs in multithreaded C programs. / Master of Science

Cette thèse porte sur la résolution du problème d'optimisation Maximum Satisfiability (Max-SAT). Nous y étudions en particulier les mécanismes liés à la détection et à la transformation des sous-ensembles inconsistants par la règle de la max-résolution. Dans le contexte des solveurs de type séparation et évaluation, nous présentons plusieurs contributions liées au calcul de la borne inférieure. Cela va du schéma d'application de la propagation unitaire utilisé pour détecter les sous-ensembles inconsistants à l'extension des critères d'apprentissage et à l'évaluation de l'impact des transformations par max-résolution sur l'efficacité des solveurs. Nos contributions ont permis l'élaboration d'un nouvel outil de résolution compétitif avec les meilleurs solveurs de l'état de l'art. Elles permettent également de mieux comprendre le fonctionnement des méthodes de type séparation et évaluation et apportent des éléments théoriques pouvant expliquer l'efficacité et les limites des solveurs existants. Cela ouvre de nouvelles perspectives d'amélioration, en particulier sur l'augmentation de l'apprentissage et la prise en compte de la structure interne des instances. Nous présentons également un exemple d'utilisation de la règle de la max-résolution dans un algorithme de recherche local. / This PhD thesis is about solving the Maximum Satisfiability (Max-SAT) problem. We study the mechanisms related to the detection and transformations of the inconsistent subsets by the max-resolution rule. In the context of the branch and bound (BnB) algorithms, we present several contributions related to the lower bound computation. They range from the study of the unit propagation scheme used to detect inconsistent subsets to the extension of the learning criteria and to the evaluation of the impact of the max-resolution transformations on the BnB solvers efficiency. Thanks to our contributions, we have implemented a new solver which is competitive with the state of art ones. We give insights allowing a better understanding of the behavior of BnB solvers as well as theoretical elements which contribute to explain the efficiency of these solvers and their limits. It opens new development perspectives on the learning mechanisms used by BnB solvers which may lead to a better consideration of the instances structural properties. We also present an example of integration of the max-resolution inference rule in a local search algorithm.

Due to the widespread demands for efficient Propositional Satisfiability (SAT) solvers and its derivatives in Electronic Design Automation applications, methods to boost the performance of the SAT solver are highly desired. This dissertation aims to enhance the performance of SAT and related SAT solving problems. A hybrid solution to boost SAT solver performance is proposed as an initial attack in this dissertation, via an integration of local and DPLL-based search approaches. Next, a different hybrid strategy is attempted that takes advantage of the conflicts in the SAT search, which plays a critical role in modern SAT solvers. Usually a learned conflict-induced clause is added back to the clause database. Although conflict-induced clauses help to block a portion of the search space, they can also become a burden due to the added cost in memory consumption and Boolean Constraint Propagation (BCP). We thus propose a novel double-layer conflict-driven learning to store only those "primary" conflict clauses back into the clause database while keeping the other clauses as pseudo Boolean constraints. With this approach our experiments demonstrate that the approach can improve both in performance and memory consumption. This work opens the door on how to assess the usefulness of conflict induced clauses. Besides the aforementioned works about enhancing SAT solver performance and reducing memory cost, this dissertation also proposed a contributing work on the extended SAT problem solving. The current SAT solvers can provide an assignment for a satisfiable propositional formula. However, the capability for a SAT solver to return an "optimal" solution for a given objective function is severely lacking. MIN-ONE SAT is an optimization problem which requires the satisfying assignment with the minimal number of Ones, and it can be easily extended to minimize an arbitrary linear objective function. While some research has been conducted on MIN-ONE SAT, the existing algorithms do not scale very well on large formulas. This dissertation presents a novel approximation algorithm (RelaxSAT) for MIN-ONE SAT. RelaxSAT generates a set of constraints from the objective function to guide the search. The constraints are gradually relaxed to eliminate the conflicts with the original Boolean SAT formula until a solution is found. The experiments demonstrate that RelaxSAT is able to handle very large instances which cannot be solved by existing MIN-ONE algorithms; furthermore, RelaxSAT is able to obtain a very tight bound on the solution with one to two orders of magnitude speedup. Based on the proposed powerful MIN-ONE SAT algorithm, we built a MAX-SAT solver which achieved more than one order of magnitude speed up compared with the-state-of-art MAX-SAT solver. We also discuss a promising application of this MAX-SAT solver in formal verification. / Ph. D.

Στην εργασία αυτή ασχοληθήκαμε με το πρόβλημα της Πιθανοτικής Ικανοποιησιμότητας. Παρουσιάσαμε ανάλυση της πολυπλοκότητας του προβλήματος και το επιλύσαμε με την βοήθεια του λογισμικού πακέτου CPLEX. Περιγράψαμε προσεγγιστικούς αλγόριθμους για το πρόβλημα της Μέγιστης Ικανοποιησιμότητας που χρησιμοποιείται στην διαδικασία της Column Generation. Τέλος, πριγράψαμε το αντίστροφο πρόβλημα των συχνών στοιχειοσυνόλων και την σχέση του με το πρόβλημα της Μέγιστης Ικανοποιησιμότητας. / This thesis is about the problem of probabilistic satisfiability. We describe its computational complexity, we solve the problem using CPLEX, we discribe some approximations on Maximum Satisfiability. Finally, we describe the connection between the problem of Probabilistic Satisfiability and the inverse frequent itemset mining.