PICOSAT(1) General Commands Manual PICOSAT(1)NAME
picosat - SAT solver with proof and core support
SYNOPSIS
picosat [options] input-file
DESCRIPTION
This manual page documents briefly the picosat command.
picosat is a SAT solver with proof and core capabilities. Use the picosat.trace binary to actually use these capabilities (these incur some
overhead).
OPTIONS -h Show summary of options.
--version
print version and exit
--config
print build configuration and exit
-v enable verbose output
-f ignore invalid header
-n do not print satisfying assignment
-p print formula in DIMACS format and exit
-i <0/1>
force FALSE respectively TRUE as default phase
-a <lit>
start with an assumption
-l <limit>
set decision limit
-s <seed>
set random number generator seed
-o <output>
set output file
-t <trace>
generate compact proof trace file (use picosat.trace, see above).
-T <trace>
generate extended proof trace file (use picosat.trace, see above).
-r <trace>
generate reverse unit propagation proof file (use picosat.trace, see above).
-c <core>
generate clausal core file in DIMACS format (use picosat.trace, see above).
-V <core>
generate file listing core variables
-U <core>
generate file listing used variables
AUTHOR
picosat was written by Armin Biere <biere@jku.at>.
This manual page was written by Michael Tautschnig <mt@debian.org>, for the Debian project (but may be used by others).
February 5, 2010 PICOSAT(1)
Check Out this Related Man Page
DEPQBF(1) General Commands Manual DEPQBF(1)NAME
depqbf - a solver for quantified boolean formulae
SYNOPSIS
depqbf [options ...] [NUM] [FILE]
DESCRIPTION
depqbf is a search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal form. It is based on the DPLL algorithm
for QBF with conflict-driven clause and solution-driven cube learning. By analyzing the structure of a formula, DepQBF tries to identify
independent variables. In addition to other benefits, this often increases freedom for decision making. See also the JSAT system descrip-
tion of DepQBF 0.1 from QBFEVAL'10 for references and a brief outline of the idea.
depqbf reads QBF formulas in QDIMACS format. If FILE is not given, it reads its input from stdin. It complies with input/output standards
as required by QBFEVAL'10.
OPTIONS
depqbf accepts the following options:
-h, --help
Print usage information.
--version
Print version.
--pretty-print
Only parse and print formula.
-v Increase verbosity incrementally.
NUM Optional: time-out after NUM seconds.
FILE Optional: read input from FILE.
EXIT STATUS
The exit status is 10 if the QBF formula given as input is satisfiable, and 20 if it is unsatisfiable; any other exit code indicates that
the formula was not solved.
SEE ALSO picosat(1), minisat(1), clasp(1).
AUTHOR
depqbf was written by Florian Lonsing <florian.lonsing@jku.at>.
This manual page was written by Thomas Krennwallner <tkren@kr.tuwien.ac.at>,
August 26, 2011 DEPQBF(1)
Hi All,
i am new to this forum.i want detail of reading the core file and trace the problem because of what the program get crashed.please help me.if any body knows any website or tutoril plese let me know.
sudhir (6 Replies)
Dear All,
I am debugging a pro c executable and I want to trace the variables. Using dbx I cant trace local variables.
Please let me know how I can do a breakpoint and trace of Pro C programs.
Regards,
Ramesh (5 Replies)
my progrme complaints 'Segmentation fault'.
How to let it print 'Segmentation fault(core dumped)' and generate core dump file?
$ulimit
unlimited (22 Replies)
Ok, this is really beyond my scripting skill level so I'm hoping somebody can help me out with this. I have a trace file in the following format:
<timestame> <devicenum> <sector address> <size in sectors> <0 or 1 (write or read)>
Here is what I need to do. I need to use the <sector address>,... (3 Replies)
Hi,
I am trying to analyze one core file on my RHEL 6.5, but I am getting below error related to the core file. So I am not getting any stack trace about the crash.
# gdb MyDebugBin /var/core/MyDebugBin.27005
GNU gdb (GDB) Red Hat Enterprise Linux (7.2-60.el6_4.1)
Copyright (C) 2010 Free... (2 Replies)