README
¶
dimacscnf
A parser for DIMACS CNF files written in Go.
DIMACS cnf is a format often used in SAT competitions or everywhere CNF formulae are required. This is a parser for the Go programming language that follows this simplified specification.
For more details see the documentation on GoDoc.
License
Licensed under the MIT license, see the LICENSE file for details.
Documentation
¶
Overview ¶
Package dimacscnf provides a parser for the simplified DIMACS cnf format. This input format is often used in SAT competations or anywhere else where cnf formulae are processed.
A more detailed description can be found on http://www.satcompetition.org/2009/format-benchmarks2009.html
The easiest way to use this package is to use ParseDimacs, ParseDimacsWithBounds or ParseDimacsCheck. They all will try to parse a cnf from a io.Reader and return the information to you. The only difference between them is that they do different checks (is the input valid in accordance with the problem line?).
If you know only correct files should be parsed use ParseDimacs, if it is important that the specification in the problem line is correct use ParseDimacsWithBounds and if it's also important if each variable occurs only once in each clause (it is a set without repetitions) and l and ¬l are not allowed in the same clause use ParseDimacsCheck.
These three methods all return the clauses a [][]int, problem 'name' (usually "cnf") and nbvar from the problem line.
If you want to create the clauses in a different way you can do that as well: Implement DimacsParserHandler and then use ParseGenericDimacs.
Index ¶
- func ParseDimacs(r io.Reader, initialClauseSize int) (string, int, [][]int, error)
- func ParseDimacsCheck(r io.Reader, initialClauseSize int) (string, int, [][]int, error)
- func ParseDimacsWithBounds(r io.Reader, initialClauseSize int) (string, int, [][]int, error)
- func ParseGenericDimacs(h DimacsParserHandler, r io.Reader) error
- type DimacsParserHandler
- type ParseError
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func ParseDimacs ¶
ParseDimacs parses the contents of the io.Reader as DIMACS and returns the problem name (usually "cnf"), the number of variables and the clauses as a slice. If something with the syntax is wrong a ParseError is returned, otherwise the error from the underlying reader is returned. If the error is nil everything was ok.
initialClauseSize may be specified to give the parser a hint about the size of clauses. That is when a new clause gets generated it will have this value as its initial capacity. Of course clauses can grow bigger, but less memory reallocation may be required. By setting it to a value >= 0 all clauses will have this clause size as the initial capacity. If it is set to a value < 0 it will compute the average clause size of clauses parsed so far and use this value as the initial clause size. This may help, but is not guaranteed to. If the length of the clauses differs very much too much or to less memory may be allocated.
func ParseDimacsCheck ¶
ParseDimacsCheck does the same as ParseDimacsWithBounds but also checks if no variable occurs more than once in each clause. That is the literal l must not occur twice in the clause, also l and ¬l are not allowed in the same clause.
For this a set must be stored, so this consumes more memory.
func ParseDimacsWithBounds ¶
ParseDimacsWithBounds does the same as ParseDimacs but also checks the bounds specified in the problem line. This is if exactly the right number of clauses were parsed and if all variables are valid (i.e. in the range of nbvar). It will however not check if all variables occur at least once somewhere in the formula (so specifying ten variables and using only two in the input would be ok).
func ParseGenericDimacs ¶
func ParseGenericDimacs(h DimacsParserHandler, r io.Reader) error
ParseGenericDimacs tries to parse the content of the io.Reader as DIMACS and calls the handle methods of the DimacsParserHandler. If one of the handle methods return an error the parsing stops.
Types ¶
type DimacsParserHandler ¶
type DimacsParserHandler interface {
ProblemLine(problem string, nbvar, nbclauses int) error
NewClause() error
NewVariable(value int) error
Done() error
}
DimacsParserHandler provides method to receive commands from the parser when a new clause or variable is encountered.
The method ProblemLine is called once with the problem specification, where problem is the name of the problem (usually "cnf"), nbvar is the number of variables and nbclauses the number of clauses.
NewClause gets called for each new clause in the file, NewVariable for each variable (so NewClause should be called before).
Done gets called once everything is done.
The parsing procedure will stop if one of the methods return an error.
type ParseError ¶
type ParseError struct {
// contains filtered or unexported fields
}
ParseError is a special error that wraps another error and also stores the line number from the input file.
func NewParseError ¶
func NewParseError(err error, lineNumber int) ParseError
NewParseError returns a new ParseError.
func (ParseError) Error ¶
func (err ParseError) Error() string
Source Files