.\"                                      Hey, EMACS: -*- nroff -*-
.\" First parameter, NAME, should be all caps
.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
.\" other parameters are allowed: see man(7), man(1)
.TH PICOSAT 1 "February  5, 2010"
.\" Please adjust this date whenever revising the manpage.
.\"
.\" Some roff macros, for reference:
.\" .nh        disable hyphenation
.\" .hy        enable hyphenation
.\" .ad l      left justify
.\" .ad b      justify to both left and right margins
.\" .nf        disable filling
.\" .fi        enable filling
.\" .br        insert line break
.\" .sp <n>    insert n+1 empty lines
.\" for manpage-specific macros, see man(7)
.SH NAME
picosat \- SAT solver with proof and core support
.SH SYNOPSIS
.B picosat
.RI [ options ] " input-file
.SH DESCRIPTION
This manual page documents briefly the
.B picosat
command.
.PP
.\" TeX users may be more comfortable with the \fB<whatever>\fP and
.\" \fI<whatever>\fP escape sequences to invode bold face and italics, 
.\" respectively.
\fBpicosat\fP is a SAT solver with proof and core capabilities. Use the
\fBpicosat.trace\fP binary to actually use these capabilities (these incur some
overhead).
.SH OPTIONS
.B \-h
Show summary of options.
.TP
.B \-\-version
print version and exit
.TP
.B \-\-config
print build configuration and exit
.TP
.B \-v
enable verbose output
.TP
.B \-f
ignore invalid header
.TP
.B \-n
do not print satisfying assignment
.TP
.B \-p
print formula in DIMACS format and exit
.TP
.B \-i <0/1>
force FALSE respectively TRUE as default phase
.TP
.B \-a <lit>
start with an assumption
.TP
.B \-l <limit>
set decision limit
.TP
.B \-s <seed>
set random number generator seed
.TP
.B \-o <output>
set output file
.TP
.B \-t <trace>
generate compact proof trace file (use picosat.trace, see above).
.TP
.B \-T <trace>
generate extended proof trace file (use picosat.trace, see above).
.TP
.B \-r <trace>
generate reverse unit propagation proof file (use picosat.trace, see above).
.TP
.B \-c <core>
generate clausal core file in DIMACS format (use picosat.trace, see above).
.TP
.B \-V <core>
generate file listing core variables
.TP
.B \-U <core>
generate file listing used variables
.PP
.SH AUTHOR
picosat was written by Armin Biere <biere@jku.at>.
.PP
This manual page was written by Michael Tautschnig <mt@debian.org>,
for the Debian project (but may be used by others).