1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30 package org.sat4j.sat;
31
32 import java.awt.BorderLayout;
33 import java.awt.Dimension;
34 import java.awt.FlowLayout;
35 import java.awt.GridBagConstraints;
36 import java.awt.GridBagLayout;
37 import java.awt.event.ActionEvent;
38 import java.awt.event.ActionListener;
39 import java.io.File;
40 import java.io.FileNotFoundException;
41 import java.io.FileOutputStream;
42 import java.io.IOException;
43 import java.io.PrintStream;
44 import java.io.PrintWriter;
45 import java.io.StringWriter;
46 import java.util.ArrayList;
47 import java.util.Collections;
48 import java.util.List;
49
50 import javax.swing.BoxLayout;
51 import javax.swing.ButtonGroup;
52 import javax.swing.DefaultComboBoxModel;
53 import javax.swing.JButton;
54 import javax.swing.JCheckBox;
55 import javax.swing.JComboBox;
56 import javax.swing.JFileChooser;
57 import javax.swing.JLabel;
58 import javax.swing.JPanel;
59 import javax.swing.JRadioButton;
60 import javax.swing.JScrollPane;
61 import javax.swing.JTabbedPane;
62 import javax.swing.JTextArea;
63 import javax.swing.JTextField;
64 import javax.swing.border.CompoundBorder;
65 import javax.swing.border.EmptyBorder;
66 import javax.swing.border.TitledBorder;
67
68 import org.sat4j.core.ASolverFactory;
69 import org.sat4j.maxsat.WeightedMaxSatDecorator;
70 import org.sat4j.maxsat.reader.MSInstanceReader;
71 import org.sat4j.minisat.core.ICDCL;
72 import org.sat4j.minisat.core.IOrder;
73 import org.sat4j.minisat.core.IPhaseSelectionStrategy;
74 import org.sat4j.minisat.core.LearnedConstraintsEvaluationType;
75 import org.sat4j.minisat.core.RestartStrategy;
76 import org.sat4j.minisat.core.SearchParams;
77 import org.sat4j.minisat.core.SimplificationType;
78 import org.sat4j.minisat.core.SolverStats;
79 import org.sat4j.minisat.orders.RandomWalkDecorator;
80 import org.sat4j.minisat.orders.VarOrderHeap;
81 import org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator;
82 import org.sat4j.pb.IPBSolver;
83 import org.sat4j.pb.OptToPBSATAdapter;
84 import org.sat4j.pb.PseudoOptDecorator;
85 import org.sat4j.pb.orders.RandomWalkDecoratorObjective;
86 import org.sat4j.pb.orders.VarOrderHeapObjective;
87 import org.sat4j.pb.reader.PBInstanceReader;
88 import org.sat4j.pb.tools.ClausalConstraintsDecorator;
89 import org.sat4j.reader.InstanceReader;
90 import org.sat4j.reader.ParseFormatException;
91 import org.sat4j.reader.Reader;
92 import org.sat4j.sat.visu.ChartBasedVisualizationTool;
93 import org.sat4j.sat.visu.GnuplotBasedSolverVisualisation;
94 import org.sat4j.sat.visu.JChartBasedSolverVisualisation;
95 import org.sat4j.sat.visu.SolverVisualisation;
96 import org.sat4j.sat.visu.TraceComposite;
97 import org.sat4j.sat.visu.VisuPreferences;
98 import org.sat4j.specs.ContradictionException;
99 import org.sat4j.specs.IConstr;
100 import org.sat4j.specs.ILogAble;
101 import org.sat4j.specs.IOptimizationProblem;
102 import org.sat4j.specs.IProblem;
103 import org.sat4j.specs.ISolver;
104 import org.sat4j.specs.ISolverService;
105 import org.sat4j.specs.Lbool;
106 import org.sat4j.specs.RandomAccessModel;
107 import org.sat4j.specs.SearchListener;
108 import org.sat4j.specs.TimeoutException;
109 import org.sat4j.tools.ClausalCardinalitiesDecorator;
110 import org.sat4j.tools.ConflictDepthTracing;
111 import org.sat4j.tools.ConflictLevelTracing;
112 import org.sat4j.tools.DecisionTracing;
113 import org.sat4j.tools.FileBasedVisualizationTool;
114 import org.sat4j.tools.HeuristicsTracing;
115 import org.sat4j.tools.LearnedClausesSizeTracing;
116 import org.sat4j.tools.LearnedTracing;
117 import org.sat4j.tools.MultiTracing;
118 import org.sat4j.tools.SpeedTracing;
119 import org.sat4j.tools.encoding.EncodingStrategy;
120 import org.sat4j.tools.encoding.Policy;
121
122
123
124
125
126
127
128
129
130 public class DetailedCommandPanel extends JPanel implements SolverController,
131 SearchListener<ISolverService>, ILogAble {
132
133 private static final String EXACTLY_1 = "Exactly 1:";
134 private static final String EXACTLY_K = "Exactly K:";
135 private static final String AT_MOST_1 = "At Most 1:";
136 private static final String AT_MOST_K = "At Most K:";
137
138 private Policy encodingPolicy;
139
140 private static final long serialVersionUID = 1L;
141
142 public static final EmptyBorder BORDER5 = new EmptyBorder(5, 5, 5, 5);
143
144 private String ramdisk;
145
146 private RemoteControlStrategy telecomStrategy;
147 private RandomWalkDecorator randomWalk;
148 private ISolver solver;
149 private Reader reader;
150 private IProblem problem;
151 private ProblemType problemType;
152 private boolean optimizationMode;
153 private boolean equivalenceMode;
154 private boolean lowerMode;
155
156 private String[] commandLines;
157
158 private boolean firstStart;
159
160 private StartSolverEnum startConfig;
161
162 private StringWriter stringWriter;
163
164 private JPanel aboutSolverPanel;
165 private JTextArea textArea;
166
167 private JPanel instancePanel;
168 private static final String INSTANCE_PANEL = "Instance";
169 private JLabel instanceLabel;
170 private static final String INSTANCE = "Path to instance: ";
171 private JTextField instancePathField;
172 private String instancePath;
173 private JButton browseButton;
174 private static final String BROWSE = "Browse";
175
176 private String whereToWriteFiles;
177
178 private static final String MINISAT_PREFIX = "minisat";
179 private static final String PB_PREFIX = "pb";
180 private static final String MAXSAT_PREFIX = "maxsat";
181 private JPanel choixSolverPanel;
182 private static final String CHOIX_SOLVER_PANEL = "Solver";
183 private JLabel choixSolver;
184 private static final String CHOIX_SOLVER = "Choose solver: ";
185 private JComboBox listeSolvers;
186
187 private static final String OPTMIZATION_MODE = "Optimization problem";
188 private JCheckBox optimisationModeCB;
189
190 private static final String EQUIVALENCE = "Use equivalence instead of implication";
191 private JCheckBox equivalenceCB;
192
193 private static final String LOWER = "Search solution by lower bounding instead of upper bounding";
194 private JCheckBox lowerCB;
195
196 private JComboBox atMostKCB;
197 private JComboBox atMost1CB;
198 private JComboBox exactlyKCB;
199 private JComboBox exactly1CB;
200
201 private JRadioButton solverLineParamLineRadio;
202 private JRadioButton solverLineParamRemoteRadio;
203 private JRadioButton solverListParamListRadio;
204 private JRadioButton solverListParamRemoteRadio;
205
206 private static final String SOLVER_LINE_PARAM_LINE_CONFIG = "Start customized solver as given in command line";
207 private static final String SOLVER_LINE_PARAM_REMOTE_CONFIG = "Start customized solver as given in command line with configuration given in the remote";
208 private static final String SOLVER_LIST_PARAM_LIST_CONFIG = "Start solver as chosen in list with its default configuration";
209 private static final String SOLVER_LIST_PARAM_REMOTE_CONFIG = "Start solver as chosen in list with configuration given in the remote";
210
211 private static final String CHOOSE_START_CONFIG = "Choose start configuration : ";
212
213 private JButton startStopButton;
214 private static final String START = "Start";
215 private static final String STOP = "Stop";
216
217 private JButton pauseButton;
218 private static final String PAUSE = "Pause";
219 private static final String RESUME = "Resume";
220
221 private static final String RESTART_PANEL = "Restart strategy";
222 private RestartCommandComponent restartPanel;
223
224 private static final String RW_PANEL = "Random Walk";
225 private RandomWalkCommandComponent rwPanel;
226
227 private static final String CLEAN_PANEL = "Learned Constraint Deletion Strategy";
228 private CleanCommandComponent cleanPanel;
229
230 private PhaseCommandComponent phasePanel;
231 private static final String PHASE_PANEL = "Phase Strategy";
232
233 private SimplifierCommandComponent simplifierPanel;
234 private static final String SIMPLIFIER_PANEL = "Simplification strategy";
235
236 private HotSolverCommandComponent hotSolverPanel;
237 private static final String HOT_SOLVER_PANEL = "Hot solver";
238
239 private JTextArea console;
240
241 private boolean isPlotActivated;
242
243 private SolverVisualisation solverVisu;
244 private VisuPreferences visuPreferences;
245
246 private boolean gnuplotBased = false;
247 private boolean chartBased = false;
248
249 private RemoteControlFrame frame;
250
251 public DetailedCommandPanel(String filename, RemoteControlFrame frame) {
252 this(filename, "", frame);
253 }
254
255 public DetailedCommandPanel(String filename, String ramdisk,
256 RemoteControlFrame frame) {
257
258 this(filename, ramdisk, new String[0], frame);
259 }
260
261 public DetailedCommandPanel(String filename, String ramdisk, String[] args,
262 RemoteControlFrame frame) {
263 super();
264
265 this.encodingPolicy = new Policy();
266
267 this.frame = frame;
268
269 this.visuPreferences = new VisuPreferences();
270
271 this.telecomStrategy = new RemoteControlStrategy(this);
272 this.instancePath = filename;
273 this.ramdisk = ramdisk;
274
275 this.console = new JTextArea();
276
277 this.commandLines = args.clone();
278 if (args.length > 0) {
279 this.solver = Solvers.configureSolver(args, this);
280 this.optimizationMode = Solvers.containsOptValue(args);
281 }
282
283 this.equivalenceMode = false;
284 this.lowerMode = false;
285
286 this.isPlotActivated = false;
287
288 if (this.solver != null) {
289 this.startConfig = StartSolverEnum.SOLVER_LINE_PARAM_LINE;
290 } else {
291 this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
292 }
293
294 this.firstStart = true;
295
296 this.setPreferredSize(new Dimension(800, 800));
297 this.setLayout(new BoxLayout(this, BoxLayout.Y_AXIS));
298
299 createInstancePanel();
300 createChoixSolverPanel();
301
302 this.restartPanel = new RestartCommandComponent(RESTART_PANEL, this,
303 this.telecomStrategy.getRestartStrategy().getClass()
304 .getSimpleName(), this);
305 this.rwPanel = new RandomWalkCommandComponent(RW_PANEL, this);
306 this.cleanPanel = new CleanCommandComponent(CLEAN_PANEL, this);
307 this.phasePanel = new PhaseCommandComponent(PHASE_PANEL, this,
308 this.telecomStrategy.getPhaseSelectionStrategy().getClass()
309 .getSimpleName());
310 this.simplifierPanel = new SimplifierCommandComponent(SIMPLIFIER_PANEL,
311 this);
312 this.hotSolverPanel = new HotSolverCommandComponent(HOT_SOLVER_PANEL,
313 this);
314
315 JScrollPane scrollPane = new JScrollPane(this.console);
316
317 scrollPane.setPreferredSize(new Dimension(400, 200));
318 scrollPane.getVerticalScrollBar().setValue(
319 scrollPane.getVerticalScrollBar().getMaximum());
320
321 MyTabbedPane tabbedPane = new MyTabbedPane();
322
323 JPanel solverBigPanel = new JPanel();
324 solverBigPanel
325 .setLayout(new BoxLayout(solverBigPanel, BoxLayout.Y_AXIS));
326 solverBigPanel.add(this.instancePanel);
327 solverBigPanel.add(this.choixSolverPanel);
328
329 tabbedPane.addTab("Solver", null, solverBigPanel,
330 "instance & solver options");
331
332 JPanel restartBigPanel = new JPanel();
333 restartBigPanel.setLayout(new GridBagLayout());
334
335 GridBagConstraints cRestart = new GridBagConstraints();
336 cRestart.anchor = GridBagConstraints.PAGE_START;
337 cRestart.fill = GridBagConstraints.HORIZONTAL;
338 cRestart.weightx = 1;
339 cRestart.weighty = 1;
340
341 restartBigPanel.add(this.restartPanel, cRestart);
342
343 tabbedPane.addTab("Restart", null, restartBigPanel,
344 "restart strategy & options");
345
346 JPanel rwPhaseBigPanel = new JPanel();
347 rwPhaseBigPanel.setLayout(new GridBagLayout());
348
349 GridBagConstraints cP = new GridBagConstraints();
350 cP.anchor = GridBagConstraints.PAGE_START;
351 cP.fill = GridBagConstraints.HORIZONTAL;
352 cP.weightx = 1;
353 cP.weighty = 1;
354
355 JPanel tmpPhasePanel = new JPanel();
356 tmpPhasePanel.setLayout(new GridBagLayout());
357 GridBagConstraints cPhase = new GridBagConstraints();
358 cPhase.fill = GridBagConstraints.HORIZONTAL;
359 cPhase.weightx = 1;
360 cPhase.weighty = .2;
361
362 tmpPhasePanel.add(this.rwPanel, cPhase);
363
364 cPhase.gridy = 1;
365 cPhase.weighty = .2;
366 tmpPhasePanel.add(this.phasePanel, cPhase);
367
368 cPhase.gridy = 2;
369 tmpPhasePanel.add(this.hotSolverPanel, cPhase);
370
371 rwPhaseBigPanel.add(tmpPhasePanel, cP);
372
373 tabbedPane.addTab("Heuristics", null, rwPhaseBigPanel,
374 "random walk and phase strategy");
375
376 JPanel clausesBigPanel = new JPanel();
377 clausesBigPanel.setLayout(new GridBagLayout());
378
379 GridBagConstraints cC = new GridBagConstraints();
380 cC.anchor = GridBagConstraints.PAGE_START;
381 cC.fill = GridBagConstraints.HORIZONTAL;
382 cC.weightx = 1;
383 cC.weighty = 1;
384
385 JPanel tmpClausesPanel = new JPanel();
386 tmpClausesPanel.setLayout(new GridBagLayout());
387 GridBagConstraints cClauses = new GridBagConstraints();
388 cClauses.fill = GridBagConstraints.HORIZONTAL;
389 cClauses.weightx = 1;
390 cClauses.weighty = .2;
391
392 tmpClausesPanel.add(this.cleanPanel, cClauses);
393
394 cClauses.gridy = 1;
395 tmpClausesPanel.add(this.simplifierPanel, cClauses);
396
397 clausesBigPanel.add(tmpClausesPanel, cC);
398
399 tabbedPane.addTab("Learned Constraints", null, clausesBigPanel,
400 "deletion and simplification strategy");
401
402 this.aboutSolverPanel = new JPanel();
403 this.textArea = new JTextArea("No solver is running at the moment");
404 this.textArea.setColumns(50);
405 this.aboutSolverPanel.add(this.textArea);
406
407 tabbedPane.addTab("About Solver", null, this.aboutSolverPanel,
408 "information about solver");
409
410 this.add(tabbedPane);
411 this.add(scrollPane);
412
413 this.restartPanel.setRestartPanelEnabled(false);
414 this.rwPanel.setRWPanelEnabled(false);
415 this.cleanPanel.setCleanPanelEnabled(false);
416 this.phasePanel.setPhasePanelEnabled(false);
417 this.simplifierPanel.setSimplifierPanelEnabled(false);
418 this.hotSolverPanel.setKeepSolverHotPanelEnabled(false);
419
420 this.solverVisu = new JChartBasedSolverVisualisation(
421 this.visuPreferences);
422
423 updateWriter();
424 }
425
426 private void createInstancePanel() {
427 this.instancePanel = new JPanel();
428
429 this.instancePanel.setName(INSTANCE_PANEL);
430 this.instancePanel.setBorder(new CompoundBorder(new TitledBorder(null,
431 this.instancePanel.getName(), TitledBorder.LEFT,
432 TitledBorder.TOP), BORDER5));
433
434 this.instancePanel.setLayout(new BorderLayout(0, 0));
435
436 this.instanceLabel = new JLabel(INSTANCE);
437 this.instancePathField = new JTextField(20);
438 this.instancePathField.setText(this.instancePath);
439
440 this.instanceLabel.setLabelFor(this.instancePathField);
441
442 this.browseButton = new JButton(BROWSE);
443
444 this.browseButton.addActionListener(new ActionListener() {
445 public void actionPerformed(ActionEvent e) {
446 openFileChooser();
447 updateListOfSolvers();
448 }
449 });
450
451 this.optimisationModeCB = new JCheckBox(OPTMIZATION_MODE);
452 this.optimisationModeCB.setSelected(this.optimizationMode);
453
454 this.equivalenceCB = new JCheckBox(EQUIVALENCE);
455 this.equivalenceCB.setSelected(this.equivalenceMode);
456
457 this.lowerCB = new JCheckBox(LOWER);
458 this.lowerCB.setSelected(this.lowerMode);
459
460 JPanel tmpPanel11 = new JPanel();
461 tmpPanel11.add(this.instanceLabel);
462 tmpPanel11.add(this.instancePathField);
463 tmpPanel11.add(this.browseButton);
464
465 JPanel tmpPanel12 = new JPanel();
466 tmpPanel12.setLayout(new BoxLayout(tmpPanel12, BoxLayout.Y_AXIS));
467 tmpPanel12.add(this.optimisationModeCB);
468 tmpPanel12.add(this.equivalenceCB);
469 tmpPanel12.add(this.lowerCB);
470
471 this.optimisationModeCB.addActionListener(new ActionListener() {
472 public void actionPerformed(ActionEvent e) {
473 setOptimisationMode(optimisationModeCB.isSelected());
474 log("use optimization mode: "
475 + DetailedCommandPanel.this.optimizationMode);
476 updateListOfSolvers();
477 }
478 });
479
480 this.equivalenceCB.addActionListener(new ActionListener() {
481 public void actionPerformed(ActionEvent e) {
482 equivalenceMode = equivalenceCB.isSelected();
483 }
484 });
485
486 this.lowerCB.addActionListener(new ActionListener() {
487 public void actionPerformed(ActionEvent e) {
488 lowerMode = lowerCB.isSelected();
489 }
490 });
491
492 instancePanel.setLayout(new BoxLayout(instancePanel, BoxLayout.Y_AXIS));
493
494 instancePanel.add(tmpPanel11);
495 instancePanel.add(tmpPanel12);
496 }
497
498 private void createChoixSolverPanel() {
499 this.choixSolverPanel = new JPanel();
500
501 this.choixSolverPanel.setName(CHOIX_SOLVER_PANEL);
502 this.choixSolverPanel.setBorder(new CompoundBorder(new TitledBorder(
503 null, this.choixSolverPanel.getName(), TitledBorder.LEFT,
504 TitledBorder.TOP), BORDER5));
505
506 this.choixSolverPanel.setLayout(new BoxLayout(choixSolverPanel,
507 BoxLayout.Y_AXIS));
508
509 this.choixSolver = new JLabel(CHOIX_SOLVER);
510
511 this.listeSolvers = new JComboBox();
512
513 updateListOfSolvers();
514
515 JPanel tmpPanel1 = new JPanel();
516 tmpPanel1.add(this.choixSolver);
517 tmpPanel1.add(this.listeSolvers);
518
519 this.startStopButton = new JButton(START);
520
521 this.startStopButton.addActionListener(new ActionListener() {
522 public void actionPerformed(ActionEvent e) {
523 manageStartStopButton();
524 }
525 });
526
527 this.pauseButton = new JButton(PAUSE);
528 this.pauseButton.setEnabled(false);
529
530 this.pauseButton.addActionListener(new ActionListener() {
531 public void actionPerformed(ActionEvent e) {
532 if (DetailedCommandPanel.this.pauseButton.getText().equals(
533 PAUSE)) {
534 DetailedCommandPanel.this.pauseButton.setText(RESUME);
535 DetailedCommandPanel.this.telecomStrategy
536 .setInterrupted(true);
537 } else {
538 DetailedCommandPanel.this.pauseButton.setText(PAUSE);
539 DetailedCommandPanel.this.telecomStrategy
540 .setInterrupted(false);
541 }
542
543 }
544 });
545
546 JPanel tmpPanel = new JPanel();
547 tmpPanel.setLayout(new GridBagLayout());
548
549 GridBagConstraints c = new GridBagConstraints();
550
551 tmpPanel.setName("Cardinality Constraints Encodings");
552 tmpPanel.setBorder(new CompoundBorder(new TitledBorder(null, tmpPanel
553 .getName(), TitledBorder.LEFT, TitledBorder.TOP), BORDER5));
554
555 JLabel atMostKLabel = new JLabel(AT_MOST_K);
556 atMostKCB = new JComboBox(new DefaultComboBoxModel(getListOfEncodings(
557 AT_MOST_K).toArray()));
558
559 JLabel atMost1Label = new JLabel(AT_MOST_1);
560 atMost1CB = new JComboBox(new DefaultComboBoxModel(getListOfEncodings(
561 AT_MOST_1).toArray()));
562
563 JLabel exactlyKLabel = new JLabel(EXACTLY_K);
564 exactlyKCB = new JComboBox(new DefaultComboBoxModel(getListOfEncodings(
565 EXACTLY_K).toArray()));
566
567 JLabel exactly1Label = new JLabel(EXACTLY_1);
568 exactly1CB = new JComboBox(new DefaultComboBoxModel(getListOfEncodings(
569 EXACTLY_1).toArray()));
570
571 c.fill = GridBagConstraints.NONE;
572 c.weightx = 0.2;
573 c.gridx = 0;
574 c.gridy = 0;
575 c.anchor = GridBagConstraints.LINE_END;
576
577 tmpPanel.add(atMostKLabel, c);
578
579 c.gridx = 0;
580 c.gridy = 1;
581 tmpPanel.add(atMost1Label, c);
582
583 c.gridx = 2;
584 c.gridy = 1;
585 tmpPanel.add(exactly1Label, c);
586
587 c.gridx = 2;
588 c.gridy = 0;
589 tmpPanel.add(exactlyKLabel, c);
590
591 c.fill = GridBagConstraints.HORIZONTAL;
592 c.anchor = GridBagConstraints.LINE_START;
593 c.weightx = 0.8;
594 c.gridx = 1;
595 c.gridy = 0;
596 tmpPanel.add(atMostKCB, c);
597
598 c.gridx = 3;
599 c.gridy = 0;
600 tmpPanel.add(exactlyKCB, c);
601
602 c.gridx = 1;
603 c.gridy = 1;
604 tmpPanel.add(atMost1CB, c);
605
606 c.gridx = 3;
607 c.gridy = 1;
608 tmpPanel.add(exactly1CB, c);
609
610 JPanel tmpPanel2 = new JPanel();
611 tmpPanel2.setLayout(new GridBagLayout());
612
613 GridBagConstraints c2 = new GridBagConstraints();
614 c2.anchor = GridBagConstraints.LINE_START;
615 c2.fill = GridBagConstraints.NONE;
616 c2.weightx = 1;
617 c2.gridx = 0;
618
619 tmpPanel2.setName(CHOOSE_START_CONFIG);
620 tmpPanel2.setBorder(new CompoundBorder(new TitledBorder(null, tmpPanel2
621 .getName(), TitledBorder.LEFT, TitledBorder.TOP), BORDER5));
622
623 this.solverLineParamLineRadio = new JRadioButton(
624 SOLVER_LINE_PARAM_LINE_CONFIG);
625 this.solverLineParamRemoteRadio = new JRadioButton(
626 SOLVER_LINE_PARAM_REMOTE_CONFIG);
627 this.solverListParamRemoteRadio = new JRadioButton(
628 SOLVER_LIST_PARAM_REMOTE_CONFIG);
629 this.solverListParamListRadio = new JRadioButton(
630 SOLVER_LIST_PARAM_LIST_CONFIG);
631
632 ButtonGroup solverConfigGroup = new ButtonGroup();
633 solverConfigGroup.add(this.solverLineParamLineRadio);
634 solverConfigGroup.add(this.solverLineParamRemoteRadio);
635 solverConfigGroup.add(this.solverListParamListRadio);
636 solverConfigGroup.add(this.solverListParamRemoteRadio);
637
638 this.solverListParamListRadio.setSelected(true);
639 this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
640
641 c2.gridy = 0;
642 tmpPanel2.add(this.solverLineParamLineRadio, c2);
643 c2.gridy = 1;
644 tmpPanel2.add(this.solverLineParamRemoteRadio, c2);
645 c2.gridy = 2;
646 tmpPanel2.add(this.solverListParamListRadio, c2);
647 c2.gridy = 3;
648 tmpPanel2.add(this.solverListParamRemoteRadio, c2);
649
650 JPanel tmpPanel3 = new JPanel();
651 tmpPanel3.setLayout(new FlowLayout());
652 tmpPanel3.add(this.startStopButton);
653 tmpPanel3.add(this.pauseButton);
654
655 this.choixSolverPanel.add(tmpPanel1);
656 this.choixSolverPanel.add(tmpPanel);
657 this.choixSolverPanel.add(tmpPanel2);
658 this.choixSolverPanel.add(tmpPanel3);
659
660 atMostKCB.addActionListener(new ActionListener() {
661 public void actionPerformed(ActionEvent e) {
662 encodingPolicy.setAtMostKEncoding((EncodingStrategy) atMostKCB
663 .getSelectedItem());
664 }
665 });
666
667 atMost1CB.addActionListener(new ActionListener() {
668 public void actionPerformed(ActionEvent e) {
669 encodingPolicy
670 .setAtMostOneEncoding((EncodingStrategy) atMost1CB
671 .getSelectedItem());
672 }
673 });
674
675 exactlyKCB.addActionListener(new ActionListener() {
676 public void actionPerformed(ActionEvent e) {
677 encodingPolicy
678 .setExactlyKEncoding((EncodingStrategy) exactlyKCB
679 .getSelectedItem());
680 }
681 });
682
683 exactly1CB.addActionListener(new ActionListener() {
684 public void actionPerformed(ActionEvent e) {
685 encodingPolicy
686 .setExactlyOneEncoding((EncodingStrategy) exactly1CB
687 .getSelectedItem());
688 }
689 });
690
691 this.solverLineParamLineRadio.addActionListener(new ActionListener() {
692 public void actionPerformed(ActionEvent e) {
693 if (DetailedCommandPanel.this.solverLineParamLineRadio
694 .isSelected()) {
695 DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LINE_PARAM_LINE;
696 }
697 }
698 });
699
700 this.solverLineParamRemoteRadio.addActionListener(new ActionListener() {
701 public void actionPerformed(ActionEvent e) {
702 if (DetailedCommandPanel.this.solverLineParamRemoteRadio
703 .isSelected()) {
704 DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LINE_PARAM_REMOTE;
705 }
706 }
707 });
708
709 this.solverListParamListRadio.addActionListener(new ActionListener() {
710 public void actionPerformed(ActionEvent e) {
711 if (DetailedCommandPanel.this.solverListParamListRadio
712 .isSelected()) {
713 DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
714 }
715 }
716 });
717
718 this.solverListParamRemoteRadio.addActionListener(new ActionListener() {
719 public void actionPerformed(ActionEvent e) {
720 if (DetailedCommandPanel.this.solverListParamRemoteRadio
721 .isSelected()) {
722 DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_REMOTE;
723 }
724 }
725 });
726
727 setChoixSolverPanelEnabled(true);
728
729 if (this.solver == null) {
730 this.solverLineParamLineRadio.setEnabled(false);
731 this.solverLineParamRemoteRadio.setEnabled(false);
732 }
733
734 if (this.firstStart) {
735 this.solverLineParamRemoteRadio.setEnabled(false);
736 this.solverListParamRemoteRadio.setEnabled(false);
737 }
738
739 }
740
741 public void manageStartStopButton() {
742 if (DetailedCommandPanel.this.startStopButton.getText().equals(START)) {
743 launchSolverWithConfigs();
744 DetailedCommandPanel.this.pauseButton.setEnabled(true);
745 setInstancePanelEnabled(false);
746 DetailedCommandPanel.this.restartPanel.setRestartPanelEnabled(true);
747 DetailedCommandPanel.this.rwPanel.setRWPanelEnabled(true);
748 DetailedCommandPanel.this.cleanPanel.setCleanPanelEnabled(true);
749 DetailedCommandPanel.this.cleanPanel
750 .setCleanPanelOriginalStrategyEnabled(true);
751 DetailedCommandPanel.this.phasePanel.setPhasePanelEnabled(true);
752 setChoixSolverPanelEnabled(false);
753 DetailedCommandPanel.this.simplifierPanel
754 .setSimplifierPanelEnabled(true);
755 DetailedCommandPanel.this.hotSolverPanel
756 .setKeepSolverHotPanelEnabled(true);
757 DetailedCommandPanel.this.startStopButton.setText(STOP);
758 solverListParamListRadio.setSelected(true);
759 startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
760 getThis().paintAll(getThis().getGraphics());
761 DetailedCommandPanel.this.frame
762 .setActivateTracingEditableUnderCondition(false);
763 frame.setActivateRadioTracing(false);
764 } else {
765
766 ((ISolver) DetailedCommandPanel.this.problem).expireTimeout();
767 DetailedCommandPanel.this.pauseButton.setEnabled(false);
768 log("Asked the solver to stop");
769 setInstancePanelEnabled(true);
770 setChoixSolverPanelEnabled(true);
771 DetailedCommandPanel.this.startStopButton.setText(START);
772 getThis().paintAll(getThis().getGraphics());
773 DetailedCommandPanel.this.frame.setActivateTracingEditable(true);
774 frame.setActivateRadioTracing(true);
775 }
776 }
777
778 public String getStartStopText() {
779 return this.startStopButton.getText();
780 }
781
782 public void setOptimisationMode(boolean optimizationMode) {
783 this.optimizationMode = optimizationMode;
784 this.optimisationModeCB.setSelected(optimizationMode);
785 }
786
787 public void launchSolverWithConfigs() {
788 ICDCL<?> cdclSolver;
789 ASolverFactory<?> factory;
790 String[] partsSelectedSolver;
791 IOrder order;
792 double proba;
793
794 String selectedSolver;
795
796 switch (startConfig) {
797 case SOLVER_LIST_PARAM_REMOTE:
798 selectedSolver = (String) this.listeSolvers.getSelectedItem();
799 partsSelectedSolver = selectedSolver.split("\\.");
800
801 assert partsSelectedSolver.length == 2;
802 assert partsSelectedSolver[0].equals(MINISAT_PREFIX)
803 || partsSelectedSolver[0].equals(PB_PREFIX)
804 || partsSelectedSolver[0].equals(MAXSAT_PREFIX);
805
806 if (partsSelectedSolver[0].equals(MINISAT_PREFIX)) {
807 factory = org.sat4j.minisat.SolverFactory.instance();
808 } else if (partsSelectedSolver[0].equals(PB_PREFIX)) {
809 factory = org.sat4j.pb.SolverFactory.instance();
810 } else {
811 factory = org.sat4j.maxsat.SolverFactory.instance();
812 }
813 this.solver = (ICDCL<?>) factory
814 .createSolverByName(partsSelectedSolver[1]);
815
816 cdclSolver = (ICDCL<?>) this.solver.getSolvingEngine();
817
818 this.telecomStrategy.setSolver(cdclSolver);
819
820 cdclSolver.setRestartStrategy(this.telecomStrategy);
821 cdclSolver.setOrder(this.randomWalk);
822 cdclSolver.getOrder().setPhaseSelectionStrategy(
823 this.telecomStrategy);
824
825 this.restartPanel.hasClickedOnRestart();
826 this.rwPanel.hasClickedOnApplyRW();
827 this.phasePanel.hasClickedOnApplyPhase();
828 this.simplifierPanel.hasClickedOnApplySimplification();
829 break;
830
831 case SOLVER_LINE_PARAM_LINE:
832 this.solver = Solvers.configureSolver(this.commandLines, this);
833
834 cdclSolver = (ICDCL<?>) this.solver.getSolvingEngine();
835
836 this.telecomStrategy.setSolver(cdclSolver);
837 this.telecomStrategy.setRestartStrategy(cdclSolver
838 .getRestartStrategy());
839 cdclSolver.setRestartStrategy(this.telecomStrategy);
840
841 this.restartPanel.setCurrentRestart(this.telecomStrategy
842 .getRestartStrategy().getClass().getSimpleName());
843
844 order = cdclSolver.getOrder();
845
846 proba = 0;
847
848 if (this.optimizationMode) {
849 if (order instanceof RandomWalkDecoratorObjective) {
850 this.randomWalk = (RandomWalkDecorator) order;
851 proba = this.randomWalk.getProbability();
852 } else if (order instanceof VarOrderHeapObjective) {
853 this.randomWalk = new RandomWalkDecoratorObjective(
854 (VarOrderHeapObjective) order, 0);
855 }
856 } else if (cdclSolver.getOrder() instanceof RandomWalkDecorator) {
857 this.randomWalk = (RandomWalkDecorator) order;
858 proba = this.randomWalk.getProbability();
859 } else {
860 this.randomWalk = new RandomWalkDecorator((VarOrderHeap) order,
861 0);
862 }
863
864 this.randomWalk.setProbability(proba);
865 this.rwPanel.setProba(proba);
866 cdclSolver.setOrder(this.randomWalk);
867 this.telecomStrategy.setPhaseSelectionStrategy(cdclSolver
868 .getOrder().getPhaseSelectionStrategy());
869 cdclSolver.getOrder().setPhaseSelectionStrategy(
870 this.telecomStrategy);
871 this.phasePanel.setPhaseListSelectedItem(this.telecomStrategy
872 .getPhaseSelectionStrategy().getClass().getSimpleName());
873 this.simplifierPanel.setSelectedSimplification(cdclSolver
874 .getSimplifier().toString());
875
876 this.phasePanel.repaint();
877 break;
878
879 case SOLVER_LINE_PARAM_REMOTE:
880 this.solver = Solvers.configureSolver(this.commandLines, this);
881
882 cdclSolver = (ICDCL<?>) this.solver.getSolvingEngine();
883
884 cdclSolver.setRestartStrategy(this.telecomStrategy);
885 cdclSolver.setOrder(this.randomWalk);
886 cdclSolver.getOrder().setPhaseSelectionStrategy(
887 this.telecomStrategy);
888
889 this.restartPanel.hasClickedOnRestart();
890 this.rwPanel.hasClickedOnApplyRW();
891 this.phasePanel.hasClickedOnApplyPhase();
892 this.simplifierPanel.hasClickedOnApplySimplification();
893 break;
894
895 default:
896 selectedSolver = (String) this.listeSolvers.getSelectedItem();
897 partsSelectedSolver = selectedSolver.split("\\.");
898
899 assert partsSelectedSolver.length == 2;
900 assert partsSelectedSolver[0].equals(MINISAT_PREFIX)
901 || partsSelectedSolver[0].equals(PB_PREFIX)
902 || partsSelectedSolver[0].equals(MAXSAT_PREFIX);
903
904 if (partsSelectedSolver[0].equals(MINISAT_PREFIX)) {
905 factory = org.sat4j.minisat.SolverFactory.instance();
906 } else if (partsSelectedSolver[0].equals(PB_PREFIX)) {
907 factory = org.sat4j.pb.SolverFactory.instance();
908 } else {
909 factory = org.sat4j.maxsat.SolverFactory.instance();
910 }
911
912 this.solver = factory.createSolverByName(partsSelectedSolver[1]);
913
914 cdclSolver = (ICDCL<?>) this.solver.getSolvingEngine();
915
916 this.telecomStrategy.setSolver(cdclSolver);
917 this.telecomStrategy.setRestartStrategy(cdclSolver
918 .getRestartStrategy());
919 cdclSolver.setRestartStrategy(this.telecomStrategy);
920
921 this.restartPanel.setCurrentRestart(this.telecomStrategy
922 .getRestartStrategy().getClass().getSimpleName());
923
924 order = cdclSolver.getOrder();
925
926 proba = 0;
927
928 if (this.optimizationMode) {
929 if (order instanceof RandomWalkDecoratorObjective) {
930 this.randomWalk = (RandomWalkDecorator) order;
931 proba = this.randomWalk.getProbability();
932 } else if (order instanceof VarOrderHeapObjective) {
933 this.randomWalk = new RandomWalkDecoratorObjective(
934 (VarOrderHeapObjective) order, 0);
935 }
936 } else if (cdclSolver.getOrder() instanceof RandomWalkDecorator) {
937 this.randomWalk = (RandomWalkDecorator) order;
938 proba = this.randomWalk.getProbability();
939 } else {
940 this.randomWalk = new RandomWalkDecorator((VarOrderHeap) order,
941 0);
942 }
943
944 this.randomWalk.setProbability(proba);
945 this.rwPanel.setProba(proba);
946
947 cdclSolver.setOrder(this.randomWalk);
948
949 this.telecomStrategy.setPhaseSelectionStrategy(cdclSolver
950 .getOrder().getPhaseSelectionStrategy());
951 this.phasePanel.setPhaseListSelectedItem(this.telecomStrategy
952 .getPhaseSelectionStrategy().getClass().getSimpleName());
953 cdclSolver.getOrder().setPhaseSelectionStrategy(
954 this.telecomStrategy);
955 this.simplifierPanel.setSelectedSimplification(cdclSolver
956 .getSimplifier().toString());
957 break;
958 }
959
960 this.whereToWriteFiles = this.instancePath;
961
962 if (this.ramdisk.length() > 0) {
963 String[] instancePathSplit = this.instancePath.split("/");
964 this.whereToWriteFiles = this.ramdisk + "/"
965 + instancePathSplit[instancePathSplit.length - 1];
966 }
967
968 this.solver.setVerbose(true);
969 initSearchListeners();
970 cdclSolver.setLogger(this);
971
972 try {
973 switch (problemType) {
974 case PB_OPT:
975 this.solver = new ClausalConstraintsDecorator(
976 (IPBSolver) this.solver, this.encodingPolicy);
977 if (lowerMode) {
978 this.solver = new ConstraintRelaxingPseudoOptDecorator(
979 (IPBSolver) solver);
980 } else {
981 this.solver = new PseudoOptDecorator((IPBSolver) solver);
982 }
983
984 this.reader = createReader(this.solver, this.instancePath);
985 this.problem = this.reader.parseInstance(this.instancePath);
986 this.problem = new OptToPBSATAdapter(
987 (IOptimizationProblem) this.problem);
988 break;
989 case CNF_MAXSAT:
990 case WCNF_MAXSAT:
991 this.solver = new ClausalConstraintsDecorator(
992 (IPBSolver) this.solver, this.encodingPolicy);
993 this.solver = new WeightedMaxSatDecorator(
994 (IPBSolver) this.solver, equivalenceMode);
995
996 this.reader = createReader(this.solver, this.instancePath);
997 this.problem = this.reader.parseInstance(this.instancePath);
998
999 if (lowerMode) {
1000 this.problem = new ConstraintRelaxingPseudoOptDecorator(
1001 (WeightedMaxSatDecorator) this.problem);
1002 } else {
1003 this.problem = new PseudoOptDecorator(
1004 (WeightedMaxSatDecorator) this.problem, false,
1005 false);
1006 }
1007
1008 this.problem = new OptToPBSATAdapter(
1009 (IOptimizationProblem) this.problem);
1010 break;
1011 case PB_SAT:
1012 this.solver = new ClausalConstraintsDecorator(
1013 (IPBSolver) this.solver, this.encodingPolicy);
1014 this.reader = createReader(this.solver, this.instancePath);
1015 this.problem = this.reader.parseInstance(this.instancePath);
1016 break;
1017 case CNF_SAT:
1018 default:
1019 this.solver = new ClausalCardinalitiesDecorator<ISolver>(
1020 this.solver, this.encodingPolicy);
1021 this.reader = createReader(this.solver, this.instancePath);
1022 this.problem = this.reader.parseInstance(this.instancePath);
1023 break;
1024 }
1025
1026 } catch (FileNotFoundException e) {
1027 log(e.getMessage());
1028 } catch (ParseFormatException e) {
1029 log(e.getMessage());
1030 } catch (IOException e) {
1031 log(e.getMessage());
1032 } catch (ContradictionException e) {
1033 log("Unsatisfiable (trivial)!");
1034 return;
1035 }
1036
1037 log("# Started solver "
1038 + this.solver.getSolvingEngine().getClass().getSimpleName());
1039 log("# on instance " + this.instancePath);
1040 log("# Optimisation = " + this.optimizationMode);
1041 log("# Restart strategy = "
1042 + this.telecomStrategy.getRestartStrategy().getClass()
1043 .getSimpleName());
1044 log("# Random walk probability = " + this.randomWalk.getProbability());
1045 log("# variables : " + this.solver.nVars());
1046
1047 Thread solveurThread = new Thread() {
1048 @Override
1049 public void run() {
1050
1051 try {
1052 DetailedCommandPanel.this.stringWriter = new StringWriter();
1053 if (DetailedCommandPanel.this.problem.isSatisfiable()) {
1054 log("Satisfiable !");
1055
1056 if (DetailedCommandPanel.this.problem instanceof OptToPBSATAdapter) {
1057 log(((OptToPBSATAdapter) DetailedCommandPanel.this.problem)
1058 .getCurrentObjectiveValue() + "");
1059 DetailedCommandPanel.this.reader
1060 .decode(((OptToPBSATAdapter) DetailedCommandPanel.this.problem)
1061 .model(new PrintWriter(
1062 DetailedCommandPanel.this.stringWriter)),
1063 new PrintWriter(
1064 DetailedCommandPanel.this.stringWriter));
1065 } else {
1066 DetailedCommandPanel.this.reader
1067 .decode(DetailedCommandPanel.this.problem
1068 .model(),
1069 new PrintWriter(
1070 DetailedCommandPanel.this.stringWriter));
1071 }
1072 log(DetailedCommandPanel.this.stringWriter.toString());
1073 } else {
1074 log("Unsatisfiable !");
1075 }
1076 } catch (TimeoutException e) {
1077 log("Timeout, sorry!");
1078 }
1079 }
1080 };
1081 solveurThread.start();
1082
1083 if (this.isPlotActivated) {
1084 this.solverVisu.setnVar(this.solver.nVars());
1085 startVisu();
1086 }
1087 }
1088
1089 public void initSearchListeners() {
1090 List<SearchListener<ISolverService>> listeners = new ArrayList<SearchListener<ISolverService>>();
1091
1092 if (this.isPlotActivated) {
1093 if (this.gnuplotBased) {
1094 this.solverVisu = new GnuplotBasedSolverVisualisation(
1095 this.visuPreferences, this.solver.nVars(),
1096 this.instancePath, this);
1097 if (this.visuPreferences.isDisplayClausesEvaluation()) {
1098 listeners.add(new LearnedTracing(
1099 new FileBasedVisualizationTool(
1100 this.whereToWriteFiles + "-learned")));
1101 }
1102 if (this.visuPreferences.isDisplayClausesSize()) {
1103 listeners.add(new LearnedClausesSizeTracing(
1104 new FileBasedVisualizationTool(
1105 this.whereToWriteFiles
1106 + "-learned-clauses-size"),
1107 new FileBasedVisualizationTool(
1108 this.whereToWriteFiles
1109 + "-learned-clauses-size-restart"),
1110 new FileBasedVisualizationTool(
1111 this.whereToWriteFiles
1112 + "-learned-clauses-size-clean")));
1113 }
1114 if (this.visuPreferences.isDisplayConflictsDecision()) {
1115 listeners
1116 .add(new ConflictLevelTracing(
1117 new FileBasedVisualizationTool(
1118 this.whereToWriteFiles
1119 + "-conflict-level"),
1120 new FileBasedVisualizationTool(
1121 this.whereToWriteFiles
1122 + "-conflict-level-restart"),
1123 new FileBasedVisualizationTool(
1124 this.whereToWriteFiles
1125 + "-conflict-level-clean")));
1126 }
1127 if (this.visuPreferences.isDisplayConflictsTrail()) {
1128 listeners
1129 .add(new ConflictDepthTracing(
1130 new FileBasedVisualizationTool(
1131 this.whereToWriteFiles
1132 + "-conflict-depth"),
1133 new FileBasedVisualizationTool(
1134 this.whereToWriteFiles
1135 + "-conflict-depth-restart"),
1136 new FileBasedVisualizationTool(
1137 this.whereToWriteFiles
1138 + "-conflict-depth-clean")));
1139 }
1140
1141 if (this.visuPreferences.isDisplayDecisionIndexes()) {
1142 listeners.add(new DecisionTracing(
1143 new FileBasedVisualizationTool(
1144 this.whereToWriteFiles
1145 + "-decision-indexes-pos"),
1146 new FileBasedVisualizationTool(
1147 this.whereToWriteFiles
1148 + "-decision-indexes-neg"),
1149 new FileBasedVisualizationTool(
1150 this.whereToWriteFiles
1151 + "-decision-indexes-restart"),
1152 new FileBasedVisualizationTool(
1153 this.whereToWriteFiles
1154 + "-decision-indexes-clean")));
1155 }
1156
1157 if (this.visuPreferences.isDisplaySpeed()) {
1158 listeners
1159 .add(new SpeedTracing(
1160 new FileBasedVisualizationTool(
1161 this.whereToWriteFiles + "-speed"),
1162 new FileBasedVisualizationTool(
1163 this.whereToWriteFiles
1164 + "-speed-clean"),
1165 new FileBasedVisualizationTool(
1166 this.whereToWriteFiles
1167 + "-speed-restart")));
1168 }
1169 if (this.visuPreferences.isDisplayVariablesEvaluation()) {
1170 listeners.add(new HeuristicsTracing(
1171 new FileBasedVisualizationTool(
1172 this.whereToWriteFiles + "-heuristics")));
1173 }
1174 }
1175
1176 else if (this.chartBased) {
1177
1178 if (this.solverVisu != null) {
1179 this.solverVisu.end();
1180 }
1181
1182 this.solverVisu = new JChartBasedSolverVisualisation(
1183 this.visuPreferences);
1184
1185 ((JChartBasedSolverVisualisation) this.solverVisu)
1186 .setnVar(this.solver.nVars());
1187 if (this.visuPreferences.isDisplayClausesEvaluation()) {
1188 listeners
1189 .add(new LearnedTracing(
1190 new ChartBasedVisualizationTool(
1191 ((JChartBasedSolverVisualisation) this.solverVisu)
1192 .getClausesEvaluationTrace())));
1193 }
1194 if (this.visuPreferences.isDisplayClausesSize()) {
1195 listeners
1196 .add(new LearnedClausesSizeTracing(
1197 new ChartBasedVisualizationTool(
1198 ((JChartBasedSolverVisualisation) this.solverVisu)
1199 .getLearnedClausesSizeTrace()),
1200 new ChartBasedVisualizationTool(
1201 ((JChartBasedSolverVisualisation) this.solverVisu)
1202 .getLearnedClausesSizeRestartTrace()),
1203 new ChartBasedVisualizationTool(
1204 ((JChartBasedSolverVisualisation) this.solverVisu)
1205 .getLearnedClausesSizeCleanTrace())));
1206 }
1207 if (this.visuPreferences.isDisplayConflictsDecision()) {
1208 listeners
1209 .add(new ConflictLevelTracing(
1210 new ChartBasedVisualizationTool(
1211 ((JChartBasedSolverVisualisation) this.solverVisu)
1212 .getConflictLevelTrace()),
1213 new ChartBasedVisualizationTool(
1214 ((JChartBasedSolverVisualisation) this.solverVisu)
1215 .getConflictLevelRestartTrace()),
1216 new ChartBasedVisualizationTool(
1217 ((JChartBasedSolverVisualisation) this.solverVisu)
1218 .getConflictLevelCleanTrace())));
1219 }
1220 if (this.visuPreferences.isDisplayConflictsTrail()) {
1221 listeners
1222 .add(new ConflictDepthTracing(
1223 new ChartBasedVisualizationTool(
1224 ((JChartBasedSolverVisualisation) this.solverVisu)
1225 .getConflictDepthTrace()),
1226 new ChartBasedVisualizationTool(
1227 ((JChartBasedSolverVisualisation) this.solverVisu)
1228 .getConflictDepthRestartTrace()),
1229 new ChartBasedVisualizationTool(
1230 ((JChartBasedSolverVisualisation) this.solverVisu)
1231 .getConflictDepthCleanTrace())));
1232 }
1233 if (this.visuPreferences.isDisplayDecisionIndexes()) {
1234 listeners
1235 .add(new DecisionTracing(
1236 new ChartBasedVisualizationTool(
1237 ((JChartBasedSolverVisualisation) this.solverVisu)
1238 .getPositiveDecisionTrace()),
1239 new ChartBasedVisualizationTool(
1240 ((JChartBasedSolverVisualisation) this.solverVisu)
1241 .getNegativeDecisionTrace()),
1242 new ChartBasedVisualizationTool(
1243 new TraceComposite(
1244 ((JChartBasedSolverVisualisation) this.solverVisu)
1245 .getRestartPosDecisionTrace(),
1246 ((JChartBasedSolverVisualisation) this.solverVisu)
1247 .getRestartNegDecisionTrace())),
1248 new ChartBasedVisualizationTool(
1249 new TraceComposite(
1250 ((JChartBasedSolverVisualisation) this.solverVisu)
1251 .getCleanPosDecisionTrace(),
1252 ((JChartBasedSolverVisualisation) this.solverVisu)
1253 .getCleanNegDecisionTrace()))));
1254 }
1255 if (this.visuPreferences.isDisplaySpeed()) {
1256 listeners
1257 .add(new SpeedTracing(
1258 new ChartBasedVisualizationTool(
1259 ((JChartBasedSolverVisualisation) this.solverVisu)
1260 .getSpeedTrace()),
1261 new ChartBasedVisualizationTool(
1262 ((JChartBasedSolverVisualisation) this.solverVisu)
1263 .getSpeedCleanTrace()),
1264 new ChartBasedVisualizationTool(
1265 ((JChartBasedSolverVisualisation) this.solverVisu)
1266 .getSpeedRestartTrace())));
1267 }
1268 if (this.visuPreferences.isDisplayVariablesEvaluation()) {
1269 listeners
1270 .add(new HeuristicsTracing(
1271 new ChartBasedVisualizationTool(
1272 ((JChartBasedSolverVisualisation) this.solverVisu)
1273 .getHeuristicsTrace())));
1274 }
1275 }
1276
1277 }
1278 listeners.add(this);
1279
1280 this.solver.setSearchListener(new MultiTracing<ISolverService>(listeners));
1281
1282 }
1283
1284 public int getNVar() {
1285 if (this.solver != null) {
1286 return this.solver.nVars();
1287 }
1288 return 0;
1289 }
1290
1291 public void setPhaseSelectionStrategy(IPhaseSelectionStrategy phase) {
1292 this.telecomStrategy.setPhaseSelectionStrategy(phase);
1293 log("Told the solver to apply a new phase strategy :"
1294 + phase.getClass().getSimpleName());
1295 }
1296
1297 public void shouldRestartNow() {
1298 this.telecomStrategy.setHasClickedOnRestart(true);
1299 }
1300
1301 public void setRestartStrategy(RestartStrategy strategy) {
1302 this.telecomStrategy.setRestartStrategy(strategy);
1303 log("Set Restart to " + strategy);
1304 }
1305
1306 public RestartStrategy getRestartStrategy() {
1307 return this.telecomStrategy.getRestartStrategy();
1308 }
1309
1310 public SearchParams getSearchParams() {
1311 return this.telecomStrategy.getSearchParams();
1312 }
1313
1314 public SolverStats getSolverStats() {
1315 return this.telecomStrategy.getSolverStats();
1316 }
1317
1318 public void init(SearchParams params, SolverStats stats) {
1319 this.telecomStrategy.init(params, stats);
1320 log("Init restart with params");
1321 }
1322
1323 public void setNbClausesAtWhichWeShouldClean(int nbConflicts) {
1324 this.telecomStrategy.setNbClausesAtWhichWeShouldClean(nbConflicts);
1325 log("Changed number of conflicts before cleaning to " + nbConflicts);
1326 }
1327
1328 public void setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy() {
1329 this.telecomStrategy
1330 .setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy(true);
1331 log("Solver now cleans clauses every "
1332 + this.cleanPanel.getCleanSliderValue()
1333 + " conflicts and bases evaluation of clauses on activity");
1334 }
1335
1336 public void setLearnedDeletionStrategyTypeToSolver(
1337 LearnedConstraintsEvaluationType type) {
1338 ((ICDCL<?>) this.solver.getSolvingEngine())
1339 .setLearnedConstraintsDeletionStrategy(this.telecomStrategy,
1340 type);
1341 log("Changed clauses evaluation type to " + type);
1342 }
1343
1344 public LearnedConstraintsEvaluationType getLearnedConstraintsEvaluationType() {
1345 return LearnedConstraintsEvaluationType.ACTIVITY;
1346 }
1347
1348 public void shouldCleanNow() {
1349 log("Told the solver to clean");
1350 this.telecomStrategy.setHasClickedOnClean(true);
1351 }
1352
1353 public void setKeepSolverHot(boolean keepHot) {
1354 this.solver.setKeepSolverHot(keepHot);
1355 if (keepHot) {
1356 log("Keep hot solver is now activated");
1357 } else {
1358 log("Keep hot solver is now desactivated");
1359 }
1360 }
1361
1362 public boolean isGnuplotBased() {
1363 return this.gnuplotBased;
1364 }
1365
1366 public void setGnuplotBased(boolean gnuplotBased) {
1367 this.gnuplotBased = gnuplotBased;
1368 }
1369
1370 public boolean isChartBased() {
1371 return this.chartBased;
1372 }
1373
1374 public void setChartBased(boolean chartBased) {
1375 this.chartBased = chartBased;
1376 }
1377
1378 public boolean isPlotActivated() {
1379 return this.isPlotActivated;
1380 }
1381
1382 public void setPlotActivated(boolean isPlotActivated) {
1383 this.isPlotActivated = isPlotActivated;
1384 }
1385
1386 public void setRandomWalkProba(double proba) {
1387 this.randomWalk.setProbability(proba);
1388 log("Set probability to " + proba);
1389 }
1390
1391 public void setSimplifier(SimplificationType type) {
1392 ((ICDCL<?>) this.solver.getSolvingEngine()).setSimplifier(type);
1393 log("Told the solver to use " + type);
1394 }
1395
1396 public List<String> getListOfSolvers() {
1397 ASolverFactory<?> factory;
1398
1399 List<String> result = new ArrayList<String>();
1400
1401 factory = org.sat4j.minisat.SolverFactory.instance();
1402 for (String s : factory.solverNames()) {
1403 result.add(MINISAT_PREFIX + "." + s);
1404 }
1405
1406 factory = org.sat4j.pb.SolverFactory.instance();
1407 for (String s : factory.solverNames()) {
1408 result.add(PB_PREFIX + "." + s);
1409 }
1410
1411 Collections.sort(result);
1412
1413 factory = org.sat4j.maxsat.SolverFactory.instance();
1414 for (String s : factory.solverNames()) {
1415 result.add(MAXSAT_PREFIX + "." + s);
1416 }
1417
1418 Collections.sort(result);
1419
1420 return result;
1421 }
1422
1423 public List<String> getListOfSatSolvers() {
1424 ASolverFactory<?> factory;
1425
1426 List<String> result = new ArrayList<String>();
1427
1428 factory = org.sat4j.minisat.SolverFactory.instance();
1429 for (String s : factory.solverNames()) {
1430 result.add(MINISAT_PREFIX + "." + s);
1431 }
1432 Collections.sort(result);
1433
1434 return result;
1435 }
1436
1437 public List<String> getListOfPBSolvers() {
1438 ASolverFactory<?> factory;
1439
1440 List<String> result = new ArrayList<String>();
1441
1442 factory = org.sat4j.pb.SolverFactory.instance();
1443 for (String s : factory.solverNames()) {
1444 result.add(PB_PREFIX + "." + s);
1445 }
1446 Collections.sort(result);
1447
1448 return result;
1449 }
1450
1451 public List<String> getListOfMaxsatSolvers() {
1452 ASolverFactory<?> factory;
1453
1454 List<String> result = new ArrayList<String>();
1455
1456 factory = org.sat4j.pb.SolverFactory.instance();
1457 for (String s : factory.solverNames()) {
1458 result.add(MAXSAT_PREFIX + "." + s);
1459 }
1460 Collections.sort(result);
1461
1462 return result;
1463 }
1464
1465 public List<EncodingStrategy> getListOfEncodings(String typeOfConstraint) {
1466 List<EncodingStrategy> v = new ArrayList<EncodingStrategy>();
1467
1468 v.add(EncodingStrategy.NATIVE);
1469
1470 if (typeOfConstraint.equals(AT_MOST_K)
1471 || typeOfConstraint.equals(AT_MOST_1)) {
1472 v.add(EncodingStrategy.BINARY);
1473 v.add(EncodingStrategy.BINOMIAL);
1474 v.add(EncodingStrategy.COMMANDER);
1475 }
1476 if (typeOfConstraint.equals(AT_MOST_K)) {
1477 v.add(EncodingStrategy.SEQUENTIAL);
1478 }
1479 if (typeOfConstraint.equals(AT_MOST_1)
1480 || typeOfConstraint.equals(EXACTLY_1)) {
1481 v.add(EncodingStrategy.LADDER);
1482 }
1483 if (typeOfConstraint.equals(AT_MOST_1)) {
1484 v.add(EncodingStrategy.PRODUCT);
1485 }
1486
1487 return v;
1488 }
1489
1490 public void log(String message) {
1491 logsameline(message + "\n");
1492 }
1493
1494 public void logsameline(String message) {
1495 if (this.console != null) {
1496 this.console.append(message);
1497 this.console.setCaretPosition(this.console.getDocument()
1498 .getLength());
1499 this.console.repaint();
1500 }
1501 this.repaint();
1502 }
1503
1504 public void openFileChooser() {
1505 JFileChooser fc = new JFileChooser();
1506 int returnVal = fc.showDialog(this, "Choose instance");
1507 if (returnVal == JFileChooser.APPROVE_OPTION) {
1508 File file = fc.getSelectedFile();
1509 this.instancePath = file.getAbsolutePath();
1510 this.instancePathField.setText(this.instancePath);
1511 updateListOfSolvers();
1512 }
1513 }
1514
1515 protected Reader createReader(ISolver theSolver, String problemname) {
1516 InstanceReader instance = new InstanceReader(theSolver);
1517 switch (problemType) {
1518 case CNF_MAXSAT:
1519 case WCNF_MAXSAT:
1520 instance = new MSInstanceReader((WeightedMaxSatDecorator) theSolver);
1521 break;
1522 case PB_OPT:
1523 case PB_SAT:
1524 instance = new PBInstanceReader((IPBSolver) theSolver);
1525 break;
1526 case CNF_SAT:
1527 instance = new InstanceReader(theSolver);
1528 break;
1529 }
1530
1531 return instance;
1532 }
1533
1534 public void updateListOfSolvers() {
1535 List<String> theList = new ArrayList<String>();
1536 String defaultSolver = "";
1537
1538 if (instancePath == null || instancePath.length() == 0) {
1539 theList = getListOfSolvers();
1540 defaultSolver = "minisat.Default";
1541 problemType = ProblemType.CNF_SAT;
1542 equivalenceCB.setEnabled(false);
1543 lowerCB.setEnabled(false);
1544 } else if (instancePath.endsWith(".cnf")) {
1545 optimisationModeCB.setEnabled(true);
1546 if (optimizationMode) {
1547 theList.addAll(getListOfMaxsatSolvers());
1548 theList.addAll(getListOfPBSolvers());
1549 defaultSolver = "maxsat.Default";
1550 equivalenceCB.setEnabled(true);
1551 lowerCB.setEnabled(true);
1552 problemType = ProblemType.CNF_MAXSAT;
1553 log("cnf file + opt => pb/maxsat solvers");
1554 } else {
1555 theList.addAll(getListOfSatSolvers());
1556 theList.addAll(getListOfPBSolvers());
1557 defaultSolver = "minisat.Default";
1558 log("cnf file + non opt => sat/pb solvers");
1559 problemType = ProblemType.CNF_SAT;
1560 equivalenceCB.setEnabled(false);
1561 lowerCB.setEnabled(false);
1562 }
1563 } else if (instancePath.endsWith(".opb")) {
1564 optimisationModeCB.setEnabled(true);
1565 theList.addAll(getListOfPBSolvers());
1566 defaultSolver = "pb.Default";
1567 if (optimizationMode) {
1568 problemType = ProblemType.PB_OPT;
1569 equivalenceCB.setEnabled(true);
1570 lowerCB.setEnabled(true);
1571 } else {
1572 problemType = ProblemType.PB_SAT;
1573 equivalenceCB.setEnabled(false);
1574 lowerCB.setEnabled(false);
1575 }
1576 log("opb file => pb solvers");
1577 } else if (instancePath.endsWith(".wcnf")) {
1578 equivalenceCB.setEnabled(true);
1579 lowerCB.setEnabled(true);
1580 theList.addAll(getListOfMaxsatSolvers());
1581 theList.addAll(getListOfPBSolvers());
1582 defaultSolver = "maxsat.Default";
1583 optimisationModeCB.setSelected(true);
1584 optimisationModeCB.setEnabled(false);
1585 problemType = ProblemType.WCNF_MAXSAT;
1586 log("wcnf file => pb/maxsat solvers");
1587 }
1588 this.listeSolvers.setModel(new DefaultComboBoxModel(theList.toArray()));
1589 this.listeSolvers.setSelectedItem(defaultSolver);
1590 this.choixSolverPanel.repaint();
1591 }
1592
1593 public void setInstancePanelEnabled(boolean enabled) {
1594 this.instanceLabel.setEnabled(enabled);
1595 this.instancePathField.setEnabled(enabled);
1596 this.browseButton.setEnabled(enabled);
1597 this.instancePanel.repaint();
1598 }
1599
1600 public void setChoixSolverPanelEnabled(boolean enabled) {
1601 this.listeSolvers.setEnabled(enabled);
1602 this.choixSolver.setEnabled(enabled);
1603 this.solverLineParamLineRadio.setEnabled(enabled);
1604 this.solverLineParamRemoteRadio.setEnabled(enabled);
1605 this.solverListParamListRadio.setEnabled(enabled);
1606 this.solverListParamRemoteRadio.setEnabled(enabled);
1607 this.choixSolverPanel.repaint();
1608 }
1609
1610 public void setSolverVisualisation(SolverVisualisation visu) {
1611 this.solverVisu = visu;
1612 }
1613
1614 public void activateGnuplotTracing(boolean b) {
1615 this.isPlotActivated = b;
1616 if (this.solver != null) {
1617 initSearchListeners();
1618 }
1619 }
1620
1621 public void startVisu() {
1622 this.solverVisu.start();
1623 }
1624
1625 public void stopVisu() {
1626 this.solverVisu.end();
1627 }
1628
1629 public VisuPreferences getGnuplotPreferences() {
1630 return this.visuPreferences;
1631 }
1632
1633 public void setGnuplotPreferences(VisuPreferences gnuplotPreferences) {
1634 this.visuPreferences = gnuplotPreferences;
1635 }
1636
1637 public DetailedCommandPanel getThis() {
1638 return this;
1639 }
1640
1641 public ISolver getSolver() {
1642 return (ISolver) this.problem;
1643 }
1644
1645 private long begin, end;
1646 private int propagationsCounter;
1647
1648 private int conflictCounter;
1649
1650 private PrintStream outSolutionFound;
1651
1652 private void updateWriter() {
1653 try {
1654 this.outSolutionFound = new PrintStream(new FileOutputStream(
1655 this.whereToWriteFiles + "_solutions.dat"));
1656 } catch (FileNotFoundException e) {
1657 this.outSolutionFound = System.out;
1658 }
1659
1660 }
1661
1662 public void init(ISolverService solverService) {
1663 this.conflictCounter = 0;
1664 }
1665
1666 public void assuming(int p) {
1667 }
1668
1669 public void propagating(int p, IConstr reason) {
1670 this.end = System.currentTimeMillis();
1671 if (this.end - this.begin >= 2000) {
1672 long tmp = this.end - this.begin;
1673
1674 this.cleanPanel.setSpeedLabeltext(this.propagationsCounter / tmp
1675 * 1000 + "");
1676
1677 this.begin = System.currentTimeMillis();
1678 this.propagationsCounter = 0;
1679 }
1680 this.propagationsCounter++;
1681 }
1682
1683 public void backtracking(int p) {
1684 }
1685
1686 public void adding(int p) {
1687 }
1688
1689 public void learn(IConstr c) {
1690 }
1691
1692 public void learnUnit(int p) {
1693 }
1694
1695 public void delete(int[] clause) {
1696 }
1697
1698 public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
1699 this.conflictCounter++;
1700 }
1701
1702 public void conflictFound(int p) {
1703 }
1704
1705 public void solutionFound(int[] model,RandomAccessModel lazyModel) {
1706 log("Found a solution !! ");
1707 logsameline(this.stringWriter.toString());
1708 this.stringWriter.getBuffer().delete(0,
1709 this.stringWriter.getBuffer().length());
1710 this.outSolutionFound.println(this.conflictCounter + "\t");
1711 }
1712
1713 public void beginLoop() {
1714 }
1715
1716 public void start() {
1717 }
1718
1719 public void end(Lbool result) {
1720 }
1721
1722 public void restarting() {
1723 this.end = System.currentTimeMillis();
1724 if (this.end != this.begin) {
1725 this.cleanPanel.setSpeedLabeltext(this.propagationsCounter
1726 / (this.end - this.begin) * 1000 + "");
1727 }
1728 }
1729
1730 public void backjump(int backjumpLevel) {
1731 }
1732
1733 public void cleaning() {
1734 this.end = System.currentTimeMillis();
1735 this.cleanPanel.setSpeedLabeltext(this.propagationsCounter
1736 / (this.end - this.begin) * 1000 + "");
1737 }
1738
1739 public class MyTabbedPane extends JTabbedPane {
1740 private static final long serialVersionUID = 1L;
1741
1742 @Override
1743 public void setSelectedIndex(int index) {
1744 if (this.getTabCount() == 5 && index == 4) {
1745 if (DetailedCommandPanel.this.solver != null
1746 && DetailedCommandPanel.this.startStopButton.getText()
1747 .equals(STOP)) {
1748 String s = DetailedCommandPanel.this.solver.toString();
1749 String res = DetailedCommandPanel.this.solver.toString();
1750 int j = 0;
1751 for (int i = 0; i < s.length(); i++) {
1752 if (s.charAt(i) != '\n') {
1753 j++;
1754 } else {
1755 j = 0;
1756 }
1757 if (j > 80) {
1758 res = new StringBuffer(res).insert(i, '\n')
1759 .toString();
1760 j = 0;
1761 }
1762 }
1763 DetailedCommandPanel.this.textArea.setText(res);
1764 DetailedCommandPanel.this.textArea.setEditable(false);
1765 DetailedCommandPanel.this.textArea.repaint();
1766 DetailedCommandPanel.this.aboutSolverPanel
1767 .paint(DetailedCommandPanel.this.aboutSolverPanel
1768 .getGraphics());
1769 DetailedCommandPanel.this.aboutSolverPanel.repaint();
1770 } else {
1771 DetailedCommandPanel.this.textArea
1772 .setText("No solver is running at the moment");
1773 DetailedCommandPanel.this.textArea.repaint();
1774 DetailedCommandPanel.this.textArea.setEditable(false);
1775 DetailedCommandPanel.this.aboutSolverPanel
1776 .paint(DetailedCommandPanel.this.aboutSolverPanel
1777 .getGraphics());
1778 DetailedCommandPanel.this.aboutSolverPanel.repaint();
1779 }
1780 }
1781 super.setSelectedIndex(index);
1782 };
1783 }
1784
1785 }