Hi,
the attached file is not parsed successfully:
$ java -jar /usr/share/java/sat4j-maxsat.jar saved.wcnf
c SAT4J: a SATisfiability library for Java (c) 2004-2010 Daniel Le Berre
c This is free software under the dual EPL/GNU LGPL licenses.
c See www.sat4j.org for details.
c This software uses some libraries from the Jakarta Commons project. See jakarta.apache.org for details.
c version 2.3.1.WHEEZY
c java.runtime.name Java(TM) SE Runtime Environment
c java.vm.name Java HotSpot(TM) 64-Bit Server VM
c java.vm.version 20.1-b02
c java.vm.vendor Sun Microsystems Inc.
c sun.arch.data.model 64
c java.version 1.6.0_26
c os.name Linux
c os.version 3.2.0-3-amd64
c os.arch amd64
c Free memory 92022936
c Max memory 1379467264
c Total memory 92995584
c Number of processors 2
c Pseudo Boolean Optimization by upper bound
c --- Begin Solver configuration ---
c org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@296672d6
c Learn all clauses as in MiniSAT
c claDecay=0.999 varDecay=0.95 conflictBoundIncFactor=1.5 initConflictBound=100
c VSIDS like heuristics from MiniSAT using a heap lightweight component caching from RSAT taking into account the objective function
c Expensive reason simplification
c Armin Biere (Picosat) restarts strategy
c Glucose learned constraints deletion strategy
c timeout=2147483s
c DB Simplification allowed=false
c --- End Solver configuration ---
c solving saved.wcnf
c reading problem ...
FATAL Parsing Errorwrong nbclauses parameter. Found 479075, 479079 expected
c starts : 0
c conflicts : 0
c decisions : 0
c propagations : 0
c inspects : 0
c shortcuts : 0
c learnt literals : 0
c learnt binary clauses : 0
c learnt ternary clauses : 0
c learnt constraints : 0
c ignored constraints : 0
c root simplifications : 0
c removed literals (reason simplification) : 0
c reason swapping (by a shorter reason) : 0
c Calls to reduceDB : 0
c number of reductions to clauses (during analyze) : 0
c number of learned constraints concerned by reduction : 0
c number of learning phase by resolution : 0
c number of learning phase by cutting planes : 0
c speed (assignments/second) : 0.0
c non guided choices 0
c learnt constraints type
c constraints type
c org.sat4j.minisat.constraints.cnf.OriginalWLClause => 26228
c org.sat4j.minisat.constraints.cnf.OriginalBinaryClause => 452120
c 478348 constraints processed.
s UNKNOWN
c Total wall clock time (in seconds): 1.64
The input looks ok and other tools do parse it:
$ clasp saved.wcnf
c clasp version 2.0.6
c Reading from saved.wcnf
s UNSATISFIABLE
c Models : 0
c Time : 0.315s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
c CPU Time : 0.310s
Thanks,
Joachim
- -- System Information:
Debian Release: wheezy/sid
APT prefers unstable
APT policy: (500, 'unstable'), (101, 'experimental')
Architecture: amd64 (x86_64)
Foreign Architectures: i386
Kernel: Linux 3.2.0-3-amd64 (SMP w/2 CPU cores)
Locale: LANG=de_DE.utf8, LC_CTYPE=de_DE.utf8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/dash
Versions of packages sat4j depends on:
ii default-jre [java6-runtime] 1:1.6-47
ii jarwrapper 0.43
ii libcommons-cli-java 1.2-3
ii openjdk-6-jre [java6-runtime] 6b24-1.11.3-2
ii sun-java5-jre [java5-runtime] 1.5.0-17-0.1
ii sun-java6-jre [java6-runtime] 6.26-3
sat4j recommends no packages.
sat4j suggests no packages.
- -- no debconf information
iEYEARECAAYFAk/61XsACgkQ9ijrk0dDIGxVPACgkDHNuJTC8nnswlNPaDLmO2T1
4VUAn3xgV05l7chFzevwapnT4B+vDZJz
=alLX
-----END PGP SIGNATURE-----