Linux and UNIX Man Pages

Linux & Unix Commands - Search Man Pages

picosat(1) [debian man page]

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)
Man Page

5 More Discussions You Might Find Interesting

1. UNIX for Advanced & Expert Users

core dump

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)
Discussion started by: sudhir patnaik
6 Replies

2. Programming

Debugging Pro C Programs

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)
Discussion started by: rameshvmenon
5 Replies

3. UNIX for Dummies Questions & Answers

No core dump

my progrme complaints 'Segmentation fault'. How to let it print 'Segmentation fault(core dumped)' and generate core dump file? $ulimit unlimited (22 Replies)
Discussion started by: vistastar
22 Replies

4. Shell Programming and Scripting

Script to find the top 100 most popular pages

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)
Discussion started by: jontjioe
3 Replies

5. Red Hat

Gdb error while debugging core file

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)
Discussion started by: sanzee007
2 Replies