1,079 research outputs found
Lazy Reimplication in Chronological Backtracking
No full textChronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose
Faster LRAT Checking Than Solving with CaDiCaL
No full textDRAT is the standard proof format used in the SAT Competition. It is easy to generate but checking proofs often takes even more time than solving the problem. An alternative is to use the LRAT proof system. While LRAT is easier and way more efficient to check, it is more complex to generate directly. Due to this complexity LRAT is not supported natively by any state-of-the-art SAT solver. Therefore Carneiro and Heule proposed the mixed proof format FRAT which still suffers from costly intermediate translation. We present an extension to the state-of-the-art solver CaDiCaL which is able to generate LRAT natively for all procedures implemented in CaDiCaL. We further present Lrat-Trim, a tool which not only trims and checks LRAT proofs in both ASCII and binary format but also produces clausal cores and has been tested thoroughly. Our experiments on recent competition benchmarks show that our approach reduces time of proof generation and certification substantially compared to competing approaches using intermediate DRAT or FRAT proofs
Clausal Congruence Closure
No full textMany practical applications of satisfiability solving employ multiple steps to encode an original problem formulation into conjunctive normal form. Often circuits are used as intermediate representation before encoding those circuits into clausal form. These circuits however might contain redundant isomorphic sub-circuits. If blindly translated into clausal form, this redundancy is retained and increases solving time unless specific preprocessing algorithms are used. Furthermore, such redundant sub-formula structure might only emerge during solving and needs to be addressed by inprocessing. This paper presents a new approach which extracts gate information from the formula and applies congruence closure to match and eliminate redundant gates. Besides new algorithms for gate extraction, we also describe previous unpublished attempts to tackle this problem. Experiments focus on the important problem of combinational equivalence checking for hardware designs and show that our new approach yields a substantial gain in CNF solver performance
Mauersegler weiter Wege. Mathias Enard: Kompass
No full textAnalysis of the peculiar scientific narrative in the novel of the Prix-Goncourt winning author Mathias Enard
Les commissions électorales en Afrique de l'Ouest
No full text[author: Mathias Hounkpe ; Ismaila Madior Fall]Electronic ed.: Abuja ; Bonn : FES, 201
Valoração econômico-financeira do Grupo Fleury
No full textÉ observado no Brasil, há menos de dez anos, um crescente número de investidores locais na bolsa de valores do país, a B3. Dado que para se tomar decisões bem fundamentadas nesse mercado é preciso conhecer o valor intrínseco/justo dos ativos, torna-se essencial conhecer o processo de valuation. Nesse sentido, esse processo de avaliação de empresas vem se tornando ainda mais importante para a população. Diante disso, optou-se por apresentá-lo e explicá-lo por meio desta monografia. Para isso, foi imprescindível escolher uma empresa para ser analisada – no caso, decidiu-se pelo Grupo Fleury. O referido grupo brasileiro de serviços de medicina diagnóstica, listado na B3, tem quase 100 anos de atuação e está presente em 9 estados brasileiros e no Distrito Federal. A motivação dessa escolha se deve à sua interessante e sólida trajetória nesse longo tempo, bem como à sua enorme contribuição para o seu setor e para o Brasil. Diante disso, este trabalho visa fazer um valuation de empresa por meio do método do Fluxo de Caixa Descontado (FCD), o qual é mundialmente reconhecido. Além disso, objetiva-se conseguir concluir se é um bom negócio – de razoáveis retorno financeiro e risco –, no contexto atual, investir no Grupo Fleury via mercado
acionário (FLRY3). Ao considerar como o limite temporal da base de dados históricos o encerramento de 2022 e ao aplicar o método FCD pela sua variação denominada Fluxo de Caixa Livre da Empresa (FCLE), concluiu-se que o preço intrínseco/justo do FLRY3 - pelas premissas e modelo utilizados - é de R$20,14. Dado que esse valor representa um potencial – significativo – de valorização de 31% em relação ao seu preço de mercado ao final de 2022, concluiu-se como um bom negócio o investimento (compra) nessa ação
Paul Bourget, écrivain engagé
No full textPaul Bourget, A committed writer, Yehoshua Mathias.
In the France of the early twentieth century, Paul Bourget's figure is that of a successful novelist who became gradually a «committed author». A monarchist, deeply conservative, passionate defender of religion and the family as the vital bases of the social order, he thus became the bard of the bourgeois ethic faced with the destabilization of modernity.Mathias Yehoshua. Paul Bourget, écrivain engagé. In: Vingtième Siècle, revue d'histoire, n°45, janvier-mars 1995. pp. 14-29
- …
