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)
Check Out this Related Man Page
CLASP(1) General Commands Manual CLASP(1)NAME
clasp - a conflict-driven nogood learning answer set solver
SYNOPSIS
clasp [number][options]
DESCRIPTION
This manual page documents briefly the clasp command.
clasp is an answer set solver for (extended) normal logic programs. It combines the high-level modeling capacities of answer set program-
ming (ASP) with state-of-the-art techniques from the area of Boolean constraint solving. The primary clasp algorithm relies on conflict-
driven nogood learning, a technique that proved very successful for satisfiability checking (SAT). Unlike other learning ASP solvers, clasp
does not rely on legacy software, such as a SAT solver or any other existing ASP solver. Rather, clasp has been genuinely developed for
answer set solving based on conflict-driven nogood learning. clasp can be applied as an ASP solver (on LPARSE output format), as a SAT
solver (on simplified DIMACS/CNF format), or as a PB solver (on OPB format).
OPTIONS
These programs follow the usual GNU command line syntax, with long options starting with two dashes (`-'). A summary of options is
included below. For a complete description, see <http://www.cs.uni-potsdam.de/clasp/>.
-h, --help
Show summary of options.
-v, --version
Show version of program.
SEE ALSO gringo(1).
AUTHOR
clasp was written by Benjamin Kaufmann <kaufmann@cs.uni-potsdam.de>.
This manual page was written by Thomas Krennwallner <tkren@kr.tuwien.ac.at>, for the Debian project (and may be used by others).
March 4, 2010 CLASP(1)
For people who want to pull a number of lines from a long file using a specific formula
n (number of iterations in a loop)
a (offset number)
b (stretch factor)
example with n {1..100}
for (( n=1; n<101; n++ )); do awk -v n=$n 'NR==a+(b*n)' a=0 b=1 inputfile >>outputfile (2 Replies)
Hello,
Im trying to work on a small script for a formula converting temperatures, Celsius to fahrenheit.
I have a formula, and it works.... it works every way I try it. But it keeps giving me the wrong results every time with expr.
The formula for C to F would be:
divide by 5, multiply by... (12 Replies)
Hi, I was wondering if someone could help with what is probably a fairly easy problem. I have two variables, i is between 1-5, j is between 11-15
I'd like to produce this:
1_11
2_12
3_13
4_14
5_15
Each number goes up incrementally with the other.
But my shoddy code is not... (5 Replies)
Dear Masters,
Kindly need your helps for this issue..
I face a formula as a picture...
the input file is
A DEPT Vp Vs rho VPperVS
------------------------ ------------ ------------ ------------
700 151.9218 121.9269 ... (11 Replies)