Enhancing Reasoning with the Extension Rule in CDCL SAT Solvers

The extension rule first introduced by G. Tseitin is a simple but powerful rule that, when added to resolution, leads to an exponentially stronger proof system known as extended resolution (ER). Despite the outstanding theoretical results obtained with ER, its exploitation in practice to improve SAT solvers' efficiency still poses some challenging issues. There have been several attempts in the literature aiming at integrating the extension rule within CDCL SAT solvers but the results are in general not as promising as in theory. An important remark that can be made on these attempts is that most of them focus on reducing the sizes of the proofs using the extended variables introduced in the solver. We adopt in this work a different view. We see extended variables as a means to enhance reasoning in solvers and therefore to give them the ability of reasoning on various semantic aspects of variables. Experiments carried out on the 2018 and 2020 SAT competitions' benchmarks show the use of the extension rule in CDCL SAT solvers to be practically beneficial for both satisfiable and unsatisfiable instances. La règle d'extension introduite pour la première fois par G. Tseitin est une règle simple mais puissante qui, ajoutée à la résolution, conduit à un système de preuves plus puissant appelé résolution étendue (ER). Malgré les résultats théoriques remarquables obtenus avec ER, son exploitation pratique pour améliorer l'efficacité des solveurs SAT pose encore quelques problèmes. Plusieurs tentatives visant à intégrer la règle d'extension aux solveurs CDCL SAT existent dans la littérature, mais les résultats ne sont en général pas aussi prometteurs qu'en théorie. Une remarque importante à faire sur ces tentatives est qu'elles se concentrent pour la plupart sur la réduction de la taille des preuves à l'aide des variables étendues introduites dans le solveur. Nous adoptons dans ce travail un point de vue différent. Nous considérons les variables étendues comme un moyen d'améliorer le raisonnement dans les solveurs et donc de leur donner la capacité de raisonner sur différents aspects sémantiques des variables. Les expérimentations réalisées sur les instances tirées des compétition SAT 2018 et 2020 montrent que l'utilisation de la règle d'extension dans les solveurs CDCL est bénéfique aussi bien pour les instances satisfiables que celles insatisfiables.

HUBUNGAN ANTARA PERAN PENYULUH PERTANIAN DENGAN PARTISIPASI PETANI DALAM USAHATANI PADI HITAM DI KELURAHAN CIKALANG KECAMATAN TAWANG KOTA TASIKMALAYA

Food is the basic need of human beings, and to fulfill it is our right to secure food. Then lead to safe the food as better nutrition needs and lifestyle. Balck rice can meet both food safety and a healthy lifestyle. The research was conducted to investigate the correlation between agricultural extension role and farmer participation in black rice crops. The method used case study by the amount of sample by Yamane, Isaac, and Michel Formula accordingly. The collected data was primary and secondary data by direct questionnaire and literature study from internet and related institutions. Data analysis used Rank Spearman Test. The result showed a significant correlation and one direction deal with agricultural extension rule and farmer participation in black rice crops. The more agricultural extension rule, the more farmer participation in black rice crops. Black rice consumer was not as much as white rice. Black rice consumer refers to consume deal with healthy lifestyle.

Augmenting the Power of (Partial) MaxSat Resolution with Extension

The refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof system with an extension rule. The new proof system MaxResE is sound and complete, and more powerful than plain MaxSAT resolution, since it can refute the soft and hard PHP in polynomial time. We show that MaxResE refutations actually subtract lower bounds from the objective function encoded by the formulas. The resulting formula is the residual after the lower bound extraction. We experimentally show that the residual of the soft PHP (once its necessary cost of 1 has been efficiently subtracted with MaxResE) is a concise, easy to solve, satisfiable problem.