4 ms·
Yup, I agree! After figuring it out by hand I was having fun encoding it for sat via this horrible pipeline: step 1 : write it out by hand in PBL [alpha] s
by shoo 11y ago
Yup, I agree! After figuring it out by hand I was having fun encoding it for sat via this horrible pipeline:
step 1 : write it out by hand in PBL [alpha]
step 2 : convert it to CNF format using [beta]
step 3 : hand-reformat it tediously to produce [gamma]
step 4 : plug machine readable CNF into [delta]
step 5 : receive a feasible solution! [epsilon]
[alpha]
Main_Exp : ((a <=> (b & c & d & e & f)) & (b <=> (~c & ~d & ~e & ~f)) & (c <=> (a & b)) & (d <=> (a | b | c)) & (e <=> (~a & ~b & ~c & ~d)) & (f <=> (~a & ~b & ~c & ~d & ~e)))
[beta] http://formal.cs.utah.edu:8080/pbl/PBL.php http://formal.cs.utah.edu:8080/pbl/PBL.php
... find replace, find replace, ...
[gamma]
c multiple choice
p cnf 6 29
-1 2 0
-1 3 0
-1 4 0
-1 5 0
-1 6 0
-2 -3 -4 -5 -6 1 0
-2 -3 0
-2 -4 0
-2 -5 0
-2 -6 0
3 4 5 6 2 0
-3 1 0
-3 2 0
-1 -2 3 0
-4 1 2 3 0
-1 4 0
-2 4 0
-3 4 0
-5 -1 0
-5 -2 0
-5 -3 0
-5 -4 0
1 2 3 4 5 0
-6 -1 0
-6 -2 0
-6 -3 0
-6 -4 0
-6 -5 0
1 2 3 4 5 6 0
[delta] http://www.msoos.org/2013/09/minisat-in-your-browser/ http://www.msoos.org/2013/09/minisat-in-your-browser/
[epsilon]
This is MiniSat 2.0 beta
============================[ Problem Statistics ]=============================
| |
| Number of variables: 6 |
| Number of clauses: 29 |
| Parsing time: 0.00 s |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 0 | 6 29 75 | 9 0 nan | 0.000 % |
===============================================================================
Verified 29 original clauses.
restarts : 1
conflicts : 2 (2 /sec)
decisions : 5 (0.00 % random) (5 /sec)
propagations : 10 (10 /sec)
conflict literals : 5 (28.57 % deleted)
CPU time : 1 s
SATISFIABLE
v -1 -2 -3 -4 5 -6 0
5 is true, aka e.
edit: I think I am someone who interprets "one of the above" as "at least one of the above but possibly more" not "exactly one of the above". not that the interpretation makes a difference for this problem.