, Pour rappel, pour ce type d'arbre, tous les noeuds situés dans le sous-arbre gauche ou droit d'un noeud portant la valeur 0 ou 1 porte la même valeur. Lors de l'évaluation, pendant le parcours, d'un noeud portant la valeur 0, un backtrack est naturellement appliqué. Mais il est important de noter que, dans le cadre d'une recherche exhaustive de toutes les solutions, un backtrack peut également étre appliqué sur la valeur 1. Bien sûr, l'interprétation en est différente : dans le cas 0, les sous-arbres ne contiennent aucune solution, mais à l'opposé dans le cas 1, il ne contiennent que des solutions, Comme il avait été indiqué dans la section 2.5.1, l'état de certains noeuds peuvent être déterminés indirectement, sans être évalués, de la connaissance d'autres noeuds

. Dans, Cela est possible en « matérialisant » les clauses sous forme de données et non de circuit. Le circuit doit pouvoir traiter n'importe quelle clause d'arité k (paramètre de l'architecture) indépendamment de la clause elle-même. De ce fait, les clauses sont représentées dans le solveur sous forme de donnée, l'indépendance du solveur par rapport à l'instance SAT traitée est indispensable

, Mais, ce nombre est à priori dans la majorité des cas, bien inférieur au nombre de clauses du problème SAT à traiter. Ceci à une conséquence importante lors de l'évaluation de l'état d'un noeud : elle ne peut être faite en une seule étape. Plusieurs cycles sont nécessaires pour traiter les clauses, par groupes de clauses. Cette approche nécessite de pouvoir de disposer d'accès rapides à la mémoire pour changer de groupe de clauses. Alors que ceci est une opération qui peut s'avérer très lente, L'architecture doit être capable d'évaluer en parallèle et en une seule étape un nombre important de clauses

, a permis de mettre en évidence le problème de limitation sévère des performances que constitue la nécessité pour une architecture de solveur d'utiliser les données représentant les clauses en y accédant à partir d'une RAM. En effet, la largeur d'une RAM reste limitée à quelques dizaines de bits, voir une centaine de bits. Ceci limite sévèrement le débit de données auquel il est possible d'accéder

. C'est-ici-qu'intervient-notre-stratégie-de-parcours-en and . Bps, Au lieu d'attendre de pouvoir disposer d'un nouveau groupe de clauses, on suspend l'évaluation du noeud courant pour commencer l'évaluation d'un autre noeud. Il est à priori évident que cela n'a pas de sens de sélectionner un noeud situé dans l'un des sous-arbres du noeud courant. De ce fait, le parcours est susceptible d'abandonner, tout du moins momentanément

, Solveur matériel dédié à la résolution de k-SAT :contribution et résultats expérimentaux SAT_CACHE pour pouvoir la récupérer en tant que page active. Lorsque c'est enfin le cas, le traitement proprement dit peut enfin commencer avec une

, L'évaluation et parcours de l'arbre de recherche est matérialisé dans le graphe de contrôle à la base par des paires d'états évaluer et décider, ce qui requiert deux cycles. Ces paires d'états peuvent être regroupées en trois groupes

G. Le-premier, constitué des états std-e et std-d correspond à une situation où l'évaluation et le parcours du graphe peut être poursuivi sans nécessiter une page de clauses autre que la page active (celle actuellement présente dans SAT_CORE). L'évaluation du noeud courant est faite pendant l'état std-e et la décision

, Par contre, une évaluation à 1 de la page actuelle, lorsqu'il ne s'agit pas de la dernière page restant à évaluer, requiert le chargement d'une nouvelle page. Si c'est possible (SAT_CACHE étant pleine et un transfert pouvant avoir lieu entre SAT_CACHE et SAT_CORE), l'alternance enre std-e et std-d se poursuit. Dans le cas contraire, l'état actuel des variables doit être mis dans le journal de SAT_JOURNAL (pour une poursuite d'évaluation différée) et une, Aucune nouvelle page n'étant nécessaire pour un backtrack ou pour une descente dans l'arbre, dans ce cas on peut continuer à alterner entre ces deux états

. Le-groupe-d'états-wc-e-et-wc-d, correspond à une situation où le processus d'évaluation et le parcours du graphe se poursuivent (sur la page active de clause) alors que l'on est en attente d'une nouvelle page de clauses. Il est cependant important de noter que toutes les combinaisons de variables qui se trouvent dans le journal (c'est à dire, les noeuds dont la poursuite d'évaluation est différée)

, Lorsque une nouvelle page de clauses devient disponible, il est nécessaire temps de reprendre l'évaluation des noeuds en attente dans le journal. La paire pj-e et pj-d correspond au fonctionnement impératif tant qu'il reste des noeud dans SAT_JOURNAL à évaluer sur la page active

, Le noeud wc-i correspond à une situation d'attente imposée par la non disponibilité de place dans SAT_JOURNAL conjointement à la non disponibilité d'une nouvelle page de clauses

, Les état de décision std-d, wc-d et pj-d peuvent tous trois conduire vers l'un des états SAT et UNSAT, correspondant respectivement à la découverte d'une solution, ou la constatation de l'absence de solution

, Unité SAT_JOURNAL

. L'unité, SAT_JOURNAL est représentée dans la figure 3.14. Elle est constituée de deux séries de registres à décalage de type FIFO (First In First Out) et d'un bloc de contrôle les pilotant

, La série de registres (push FIFO buffer) est utilisée pour recevoir les combinaisons de variables des noeuds dont l'évaluation est suspendue/différée et qui ont déjà été évalués sur la -développement d'une plateforme logicielle permettant de doter le solveur d'un interface homme/machine un tant soit peu ergonomique afin d

, -développement des algorithmes de prétraitement des clauses permettant de les regrouper en pages de clauses « contradictoires », c'est-à-dire, où les contraintes entre clauses d'un même page favorise sur chaque page l'évaluation des noeuds à 0

, -découpage d'un problème SAT en plusieurs sous-problèmes SAT disjoints (par voie logicielle) et résolution indépendante de ces sous-problèmes

, SAT_CORE et SAT_JOURNAL, voire même, d'autres organisations internets sont à envisager. L'algorithme de parcours implémenté dans le solveur, bien qu'utilisant une stratégie astucieuse de parcours de l'arbre par suspension/report d'évaluation de noeud, peut être largement améliorer en y intégrant des heuristiques nouvelles. En effet, l'application telles quelles des heuristiques traditionnelles de l'approche logicielle est peu approprié, ces heuristiques étant difficilement parallélisables sans risque d, À plus long terme, l'exploration d'autres alternatives architecturales pour les trois unités SAT_CACHE

M. Yves, Analyse préliminaire de risques. Editions TI, Techniques de l'Ingénieur, 2002.

A. Heurtel, La gestion des risques techniques (sûreté de fonctionnement) et des risques de management, CNRS IN2P3/LAL Version, vol.2, p.6, 2003.

M. Sallak, C. Simon, and J. Aubry, Optimal design of safety instrumented systems : A graph reliability approach, 7ème Congrès International Pluridisciplinaire Qualité et Sûreté de Fonctionnement, pp.255-262, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00143145

J. Laprie, Sûreté de fonctionnement informatique : concepts, défis, directions. Computing, vol.1, pp.11-33, 2004.

R. Flanagan and G. Norman, Risk management and construction blackwell science ltd, 1993.

S. Ayed, S. Dellagi, and N. Rezg, Optimal integrated maintenance production strategy with variable production rate for random demand and subcontracting constraint, IFAC Proceedings Volumes, vol.44, pp.5207-5212, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00601441

S. Dellagi, A. Chelbi, and W. Trabelsi, Joint integrated production-maintenance policy with production plan smoothing through production rate control, Journal of manufacturing systems, vol.42, pp.262-270, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01493305

L. Mifdal, Z. Hajej, and S. Dellagi, Joint optimization approach of maintenance and production planning for a multiple-product manufacturing system, Mathematical Problems in Engineering, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01322485

S. Haddad, Modèle d'évaluation des performances d'une ligne de production d'une séquence de N produits distincts sur M machines avec (M-1) stocks tampons, 2012.

R. Impagliazzo, S. Lovett, R. Paturi, and S. Schneider, , pp.0-1, 2014.

O. Koné, C. Artigues, P. Lopez, and M. Mongeau, Comparison of mixed integer linear programming models for the resource-constrained project scheduling problem with consumption and production of resources, Flexible Services and Manufacturing Journal, vol.25, issue.1-2, pp.25-47, 2013.

G. Dantzig, Linear programming and extensions, 2016.

. Ignasi-abío-roig, Solving hard industrial combinatorial problems with sat, 2013.

G. António, J. Ramos, and . Leal, Ilp model for energy-efficient production scheduling of flake ice units in food retail stores, Journal of cleaner production, vol.156, pp.953-961, 2017.

K. Bousmar, F. Monteiro, and S. Dellagi, Zineb Habbas, and Abbas Dandache. Modelling industrial manufacturing problem using ilp solver : Case of production analysis, Microelectronics (ICM), 2017 29th International Conference on, pp.1-4, 2017.

K. Bousmar, F. Monteiro, and Z. Habbas, Sofiene Dellagi, and Abbas Dandache. A pure hardware k-sat solver architecture using fpga for developing decisionsupport tools for industrial problems, 6ème conférence international sur l'Innovation et Nouvelles Tendances dans les Systèmes d'Information INTIS 24-25 Novembre, 2017.

S. Cook, The p versus np problem. The millennium prize problems, pp.87-104, 2006.

C. Figueiredo, The p versus np-complete dichotomy of some challenging problems in graph theory, Discrete Applied Mathematics, vol.160, issue.18, pp.2681-2693, 2012.

F. Lardeux, Approches hybrides pour les problèmes de satisfiabilité (SAT et MAX-SAT), 2005.

A. Fadi-a-aloul, . Ramani, L. Igor, . Markov, and . Sakallah, Solving difficult sat instances in the presence of symmetry, Proceedings of the 39th annual Design Automation Conference, pp.731-736, 2002.

F. Luca, K. Samith, and S. Nader, Résolution pratique de problèmes np-complets, p.26, 2005.

X. Wang, A novel approach of solving the cnf-sat problem, 2013.

O. Fourdrinoy, Hybridation des méthodes de résolution pour sat. 7e Rencontres Jeunes Chercheurs en Intelligence Artificielle, 2005.

M. Davis, G. Logemann, and D. Loveland, A machine program for theoremproving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.

S. Arnborg, G. Derek, A. Corneil, and . Proskurowski, Complexity of finding embeddings in ak-tree, SIAM Journal on Algebraic Discrete Methods, vol.8, issue.2, pp.277-284, 1987.

A. Becker and D. Geiger, A sufficiently fast algorithm for finding close to optimal clique trees, Artificial Intelligence, vol.125, issue.1-2, pp.3-17, 2001.

I. Skliarova and A. Ferrari, Reconfigurable hardware sat solvers : A survey of systems, IEEE Transactions on Computers, vol.53, issue.11, pp.1449-1461, 2004.

L. Zhang and S. Malik, The quest for efficient boolean satisfiability solvers, International Conference on Computer Aided Verification, pp.17-36, 2002.

M. Davis and H. Putnam, A computing procedure for quantification theory, Journal of the ACM (JACM), vol.7, issue.3, pp.201-215, 1960.

M. Chu, A. Li, and . Anbulagan, Heuristics based on unit propagation for satisfiability problems, Proceedings of the 15th international joint conference on Artifical intelligence, vol.1, pp.366-371, 1997.

D. Loveland, Automatic theorem proving, 1978.

E. Richard and . Korf, Depth-first iterative-deepening : An optimal admissible tree search. Artificial intelligence, vol.27, pp.97-109, 1985.

M. Jp, . Silva, A. Karem, and . Sakallah, Conflict analysis in search algorithms for satisfiability, Proceedings Eighth IEEE International Conference on, pp.467-469, 1996.

. Matthew-w-moskewicz, F. Conor, Y. Madigan, L. Zhao, S. Zhang et al., Chaff : Engineering an efficient sat solver, Proceedings of the 38th annual Design Automation Conference, pp.530-535, 2001.

N. Maaroju, . Deepak-guide, and . Garg, Choosing the best heuristic for a NP-Problem, 2009.

L. Konlac and J. Garvin, Contributions à la résolution du problème de la Satisfiabilité Propositionnelle, 2014.

P. Carla, B. Gomes, H. Selman, and . Kautz, Boosting combinatorial search through randomization, vol.98, pp.431-437, 1998.

L. Zhang, F. Conor, . Madigan, H. Matthew, S. Moskewicz et al., Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, pp.279-285, 2001.

P. Carla, H. Gomes, A. Kautz, B. Sabharwal, and . Selman, Satisfiability solvers, Foundations of Artificial Intelligence, vol.3, pp.89-134, 2008.

P. Vander-swalmen, Aspects parallèles des problèmes de satisfaisabilité, 2009.

M. James, . Crawford, and . Larry-d-auton, Experimental results on the crossover point in random 3-sat, Artificial intelligence, vol.81, issue.1-2, pp.31-57, 1996.

G. Robert, J. Jeroslow, and . Wang, Solving propositional satisfiability problems, Annals of mathematics and Artificial Intelligence, vol.1, issue.1-4, pp.167-187, 1990.

M. Yokoo, T. Suyama, and H. Sawada, Solving satisfiability problems using field programmable gate arrays : First results, International Conference on Principles and Practice of Constraint Programming, pp.497-509, 1996.

T. Suyama, M. Yokoo, and H. Sawada, Solving satisfiability problems on fpgas, International Workshop on Field Programmable Logic and Applications, pp.136-145, 1996.

T. Suyama, M. Yokoo, and H. Sawada, Solving satisfiability problems using logic synthesis and reconfigurable hardware, Proceedings of the Thirty-First Hawaii International Conference on, vol.7, pp.179-186, 1998.

T. Suyama, M. Yokoo, H. Sawada, and A. Nagoya, Solving satisfiability problems using reconfigurable computing, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol.9, pp.109-116, 2001.

T. Suyama, M. Yokoo, and A. Nagoya, Solving satisfiability problems on fpgas using experimental unit propagation, International Conference on Principles and Practice of Constraint Programming, pp.434-445, 1999.

J. W. and F. , Improvements to propositional satisfiability search algorithms, 1995.

P. Zhong, M. Martonosi, P. Ashar, and S. Malik, Using configurable computing to accelerate boolean satisfiability, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.18, issue.6, pp.861-868, 1999.

P. Zhong, P. Ashar, S. Malik, and M. Martonosi, Using reconfigurable computing techniques to accelerate problems in the cad domain : a case study with boolean satisfiability, Proceedings of the 35th annual Design Automation Conference, pp.194-199, 1998.

P. Zhong, M. Martonosi, P. Ashar, and S. Malik, Solving boolean satisfiability with dynamic hardware configurations, International Workshop on Field Programmable Logic and Applications, pp.326-335, 1998.

P. João, . Marques-silva, A. Karem, and . Sakallah, Grasp : A search algorithm for propositional satisfiability, IEEE Transactions on Computers, vol.48, issue.5, pp.506-521, 1999.

O. Mencer and M. Plazner, Dynamic circuit generation for boolean satisfiability in an object-oriented design environment, Systems Sciences, 1999. HICSS-32. Proceedings of the 32nd Annual Hawaii International Conference on, 1999.

M. Abramovici and D. Saab, Satisfiability on reconfigurable hardware, ternational Workshop on Field Programmable Logic and Applications, pp.448-456

. Springer, , 1997.

P. Goel, An implicit enumeration algorithm to generate tests for combinational logic circuits, IEEE transactions on Computers, issue.3, pp.215-222, 1981.

M. Abramovici and J. Sousa, A sat solver using reconfigurable hardware and virtual logic, Journal of Automated Reasoning, vol.24, issue.1-2, pp.5-36, 2000.

A. Dandalis, K. Viktor, and . Prasanna, Run-time performance optimization of an fpgabased deduction engine for sat solvers, ACM Transactions on Design Automation of Electronic Systems (TODAES), vol.7, issue.4, pp.547-562, 2002.

M. Redekopp and A. Dandalis, A parallel pipelined sat solver for fpga's, International Workshop on Field Programmable Logic and Applications, pp.462-468

. Springer, , 2000.

Y. Wong-hiu, Y. Wing-seung, K. H. Lee, and P. Leong, A runtime reconfigurable implementation of the gsat algorithm, International Workshop on Field Programmable Logic and Applications, pp.526-531, 1999.

P. Heng, W. Leong, C. W. Sham, H. Y. Wong, and . Wong, Wing Seung Yuen, and Monk-Ping Leong. A bitstream reconfigurable fpga implementation of the wsat algorithm, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol.9, pp.197-201, 2001.

C. K. Chung and P. Leong, An architecture for solving boolean satisfiability using runtime configurable hardware, Proceedings. 1999 International Workshops on, pp.352-357, 1999.

D. José-t-de-sousa, M. Silva, and . Abramovici, A configurable hardware/software approach to sat solving, Field-Programmable Custom Computing Machines, 2001. FCCM'01. The 9th Annual IEEE Symposium on, pp.239-248, 2001.

N. A. Reis and J. Sousa, On implementing a configware/software sat solver, Field-Programmable Custom Computing Machines, pp.282-283, 2002.

. Rc-ripado and . Sousa, A simulation tool for a pipelined sat solver, 2001.

I. Skliarova and A. Ferrari, A software/reconfigurable hardware sat solver, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol.12, issue.4, pp.408-419, 2004.

K. Bousmar, F. Monteiro, and Z. Habbas, Sofiene Dellagi, and Abbas Dandache. A new fpga-based dpll algorithm to improve sat solvers, 27th International Conference on, pp.287-290, 2015.

S. Mokhtar, J. J. Bazaraa, H. Jarvis, and . Sherali, Linear programming and network flows, 2011.

R. Luc-de, Learning constraint satisfaction problems : An ilp perspective, Anton Dries, Tias Guns, and Christian Bessiere, pp.96-112, 2016.

R. Harry and . Lewis, Computers and intractability. a guide to the theory of np-completeness, 1983.

B. Peter-c-cheeseman, W. Kanefsky, and . Taylor, Where the really hard problems are, IJCAI, vol.91, pp.331-340, 1991.

S. Ravinderjit, N. Braich, C. Chelyapov, . Johnson, W. K. Paul et al., Solution of a 20-variable 3-sat problem on a dna computer, Science, vol.296, issue.5567, pp.499-502, 2002.

M. Buro and H. Büning, Report on a SAT competition, Fachbereich Math.-Informatik, 1992.

M. Platzner and G. D. Micheli, Acceleration of satisfiability algorithms by reconfigurable hardware, International Workshop on Field Programmable Logic and Applications, pp.69-78, 1998.

I. Skliarova, B. António, and . Ferrari, A hardware/software approach to accelerate boolean satisfiability, Proc. IEEE Design and Diagnostics of Electronic Circuits and Systems Workshop, pp.270-277, 2002.

K. Gulati, M. Waghmode, P. Sunil, W. Khatri, and . Shi, Efficient, scalable hardware engine for boolean satisfiability and unsatisfiable core extraction, IET Computers & Digital Techniques, vol.2, issue.3, pp.214-229, 2008.

M. Safar, M. El-kharashi, A. Shalan, and . Salem, A reconfigurable, pipelined, conflict directed jumping search sat solver, Design, Automation & Test in Europe Conference & Exhibition (DATE), pp.1-6, 2011.

J. Thong and N. Nicolici, Fpga acceleration of enhanced boolean constraint propagation for sat solvers, Proceedings of the International Conference on Computer-Aided Design, pp.234-241, 2013.

J. Thong and N. Nicolici, Sat solving using fpga-based heterogeneous computing, Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, pp.232-239, 2015.

K. Bousmar, F. Monteiro, and Z. Habbas, Sofiene Dellagi, and Abbas Dandache. A pure hardware k-sat solver architecture for fpga based on generic tree-search, Microelectronics (ICM), 2017 29th International Conference on, pp.1-5, 2017.

K. Bousmar, F. Monteiro, Z. Habbas, S. Dellagi, A. Dandache et al., Mohamed ans Alami. A pure hardware k-sat solver architecture using fpga for developing decision-support tools for industrial problems, International conference on complexe systems and logistics, ICOSYL'18, pp.11-13, 2018.